301   SMTExprRef newExprRef(const SMTExpr &Exp) {  in newExprRef()  function in __anon13641eda0111::Z3Solver
337     return newExprRef(  in mkBVNeg()
342     return newExprRef(  in mkBVNot()
347     return newExprRef(  in mkNot()
352     return newExprRef(  in mkBVAdd()
358     return newExprRef(  in mkBVSub()
364     return newExprRef(  in mkBVMul()
370     return newExprRef(  in mkBVSRem()
376     return newExprRef(  in mkBVURem()
382     return newExprRef(  in mkBVSDiv()
388     return newExprRef(  in mkBVUDiv()
394     return newExprRef(  in mkBVShl()
400     return newExprRef(  in mkBVAshr()
406     return newExprRef(  in mkBVLshr()
412     return newExprRef(  in mkBVXor()
418     return newExprRef(  in mkBVOr()
424     return newExprRef(  in mkBVAnd()
430     return newExprRef(  in mkBVUlt()
436     return newExprRef(  in mkBVSlt()
442     return newExprRef(  in mkBVUgt()
448     return newExprRef(  in mkBVSgt()
454     return newExprRef(  in mkBVUle()
460     return newExprRef(  in mkBVSle()
466     return newExprRef(  in mkBVUge()
472     return newExprRef(  in mkBVSge()
479     return newExprRef(Z3Expr(Context, Z3_mk_and(Context.Context, 2, Args)));  in mkAnd()
484     return newExprRef(Z3Expr(Context, Z3_mk_or(Context.Context, 2, Args)));  in mkOr()
488     return newExprRef(  in mkEqual()
494     return newExprRef(  in mkFPNeg()
499     return newExprRef(Z3Expr(  in mkFPIsInfinite()
504     return newExprRef(  in mkFPIsNaN()
509     return newExprRef(Z3Expr(  in mkFPIsNormal()
514     return newExprRef(Z3Expr(  in mkFPIsZero()
520     return newExprRef(  in mkFPMul()
528     return newExprRef(  in mkFPDiv()
535     return newExprRef(  in mkFPRem()
542     return newExprRef(  in mkFPAdd()
550     return newExprRef(  in mkFPSub()
557     return newExprRef(  in mkFPLt()
563     return newExprRef(  in mkFPGt()
569     return newExprRef(  in mkFPLe()
575     return newExprRef(  in mkFPGe()
581     return newExprRef(  in mkFPEqual()
588     return newExprRef(  in mkIte()
594     return newExprRef(Z3Expr(  in mkBVSignExt()
599     return newExprRef(Z3Expr(  in mkBVZeroExt()
605     return newExprRef(Z3Expr(Context, Z3_mk_extract(Context.Context, High, Low,  in mkBVExtract()
613     return newExprRef(Z3Expr(  in mkBVAddNoOverflow()
622     return newExprRef(Z3Expr(  in mkBVAddNoUnderflow()
631     return newExprRef(Z3Expr(  in mkBVSubNoOverflow()
640     return newExprRef(Z3Expr(  in mkBVSubNoUnderflow()
649     return newExprRef(Z3Expr(  in mkBVSDivNoOverflow()
657     return newExprRef(Z3Expr(  in mkBVNegNoOverflow()
665     return newExprRef(Z3Expr(  in mkBVMulNoOverflow()
674     return newExprRef(Z3Expr(  in mkBVMulNoUnderflow()
680     return newExprRef(  in mkBVConcat()
687     return newExprRef(Z3Expr(  in mkFPtoFP()
695     return newExprRef(Z3Expr(  in mkSBVtoFP()
703     return newExprRef(Z3Expr(  in mkUBVtoFP()
711     return newExprRef(Z3Expr(  in mkFPtoSBV()
718     return newExprRef(Z3Expr(  in mkFPtoUBV()
724     return newExprRef(Z3Expr(Context, b ? Z3_mk_true(Context.Context)  in mkBoolean()
735       return newExprRef(Z3Expr(  in mkBitvector()
747     return newExprRef(Z3Expr(Context, Literal));  in mkBitvector()
756     return newExprRef(Z3Expr(  in mkFloat()
762     return newExprRef(  in mkSymbol()
783     return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context)));  in getFloatRoundingMode()
852     SMTExprRef Assign = newExprRef(  in getInterpretation()
866     SMTExprRef Assign = newExprRef(  in getInterpretation()