313   SMTExprRef newExprRef(const SMTExpr &Exp) {  in newExprRef()  function in __anona2cc94240111::Z3Solver
349     return newExprRef(  in mkBVNeg()
354     return newExprRef(  in mkBVNot()
359     return newExprRef(  in mkNot()
364     return newExprRef(  in mkBVAdd()
370     return newExprRef(  in mkBVSub()
376     return newExprRef(  in mkBVMul()
382     return newExprRef(  in mkBVSRem()
388     return newExprRef(  in mkBVURem()
394     return newExprRef(  in mkBVSDiv()
400     return newExprRef(  in mkBVUDiv()
406     return newExprRef(  in mkBVShl()
412     return newExprRef(  in mkBVAshr()
418     return newExprRef(  in mkBVLshr()
424     return newExprRef(  in mkBVXor()
430     return newExprRef(  in mkBVOr()
436     return newExprRef(  in mkBVAnd()
442     return newExprRef(  in mkBVUlt()
448     return newExprRef(  in mkBVSlt()
454     return newExprRef(  in mkBVUgt()
460     return newExprRef(  in mkBVSgt()
466     return newExprRef(  in mkBVUle()
472     return newExprRef(  in mkBVSle()
478     return newExprRef(  in mkBVUge()
484     return newExprRef(  in mkBVSge()
491     return newExprRef(Z3Expr(Context, Z3_mk_and(Context.Context, 2, Args)));  in mkAnd()
496     return newExprRef(Z3Expr(Context, Z3_mk_or(Context.Context, 2, Args)));  in mkOr()
500     return newExprRef(  in mkEqual()
506     return newExprRef(  in mkFPNeg()
511     return newExprRef(Z3Expr(  in mkFPIsInfinite()
516     return newExprRef(  in mkFPIsNaN()
521     return newExprRef(Z3Expr(  in mkFPIsNormal()
526     return newExprRef(Z3Expr(  in mkFPIsZero()
532     return newExprRef(  in mkFPMul()
540     return newExprRef(  in mkFPDiv()
547     return newExprRef(  in mkFPRem()
554     return newExprRef(  in mkFPAdd()
562     return newExprRef(  in mkFPSub()
569     return newExprRef(  in mkFPLt()
575     return newExprRef(  in mkFPGt()
581     return newExprRef(  in mkFPLe()
587     return newExprRef(  in mkFPGe()
593     return newExprRef(  in mkFPEqual()
600     return newExprRef(  in mkIte()
606     return newExprRef(Z3Expr(  in mkBVSignExt()
611     return newExprRef(Z3Expr(  in mkBVZeroExt()
617     return newExprRef(Z3Expr(Context, Z3_mk_extract(Context.Context, High, Low,  in mkBVExtract()
625     return newExprRef(Z3Expr(  in mkBVAddNoOverflow()
634     return newExprRef(Z3Expr(  in mkBVAddNoUnderflow()
643     return newExprRef(Z3Expr(  in mkBVSubNoOverflow()
652     return newExprRef(Z3Expr(  in mkBVSubNoUnderflow()
661     return newExprRef(Z3Expr(  in mkBVSDivNoOverflow()
669     return newExprRef(Z3Expr(  in mkBVNegNoOverflow()
677     return newExprRef(Z3Expr(  in mkBVMulNoOverflow()
686     return newExprRef(Z3Expr(  in mkBVMulNoUnderflow()
692     return newExprRef(  in mkBVConcat()
699     return newExprRef(Z3Expr(  in mkFPtoFP()
707     return newExprRef(Z3Expr(  in mkSBVtoFP()
715     return newExprRef(Z3Expr(  in mkUBVtoFP()
723     return newExprRef(Z3Expr(  in mkFPtoSBV()
730     return newExprRef(Z3Expr(  in mkFPtoUBV()
736     return newExprRef(Z3Expr(Context, b ? Z3_mk_true(Context.Context)  in mkBoolean()
747       return newExprRef(Z3Expr(  in mkBitvector()
759     return newExprRef(Z3Expr(Context, Literal));  in mkBitvector()
768     return newExprRef(Z3Expr(  in mkFloat()
774     return newExprRef(  in mkSymbol()
795     return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context)));  in getFloatRoundingMode()
864     SMTExprRef Assign = newExprRef(  in getInterpretation()
878     SMTExprRef Assign = newExprRef(  in getInterpretation()