299   SMTExprRef newExprRef(const SMTExpr &Exp) {  in newExprRef()  function in __anonca7d1dd80111::Z3Solver
335     return newExprRef(  in mkBVNeg()
340     return newExprRef(  in mkBVNot()
345     return newExprRef(  in mkNot()
350     return newExprRef(  in mkBVAdd()
356     return newExprRef(  in mkBVSub()
362     return newExprRef(  in mkBVMul()
368     return newExprRef(  in mkBVSRem()
374     return newExprRef(  in mkBVURem()
380     return newExprRef(  in mkBVSDiv()
386     return newExprRef(  in mkBVUDiv()
392     return newExprRef(  in mkBVShl()
398     return newExprRef(  in mkBVAshr()
404     return newExprRef(  in mkBVLshr()
410     return newExprRef(  in mkBVXor()
416     return newExprRef(  in mkBVOr()
422     return newExprRef(  in mkBVAnd()
428     return newExprRef(  in mkBVUlt()
434     return newExprRef(  in mkBVSlt()
440     return newExprRef(  in mkBVUgt()
446     return newExprRef(  in mkBVSgt()
452     return newExprRef(  in mkBVUle()
458     return newExprRef(  in mkBVSle()
464     return newExprRef(  in mkBVUge()
470     return newExprRef(  in mkBVSge()
477     return newExprRef(Z3Expr(Context, Z3_mk_and(Context.Context, 2, Args)));  in mkAnd()
482     return newExprRef(Z3Expr(Context, Z3_mk_or(Context.Context, 2, Args)));  in mkOr()
486     return newExprRef(  in mkEqual()
492     return newExprRef(  in mkFPNeg()
497     return newExprRef(Z3Expr(  in mkFPIsInfinite()
502     return newExprRef(  in mkFPIsNaN()
507     return newExprRef(Z3Expr(  in mkFPIsNormal()
512     return newExprRef(Z3Expr(  in mkFPIsZero()
518     return newExprRef(  in mkFPMul()
526     return newExprRef(  in mkFPDiv()
533     return newExprRef(  in mkFPRem()
540     return newExprRef(  in mkFPAdd()
548     return newExprRef(  in mkFPSub()
555     return newExprRef(  in mkFPLt()
561     return newExprRef(  in mkFPGt()
567     return newExprRef(  in mkFPLe()
573     return newExprRef(  in mkFPGe()
579     return newExprRef(  in mkFPEqual()
586     return newExprRef(  in mkIte()
592     return newExprRef(Z3Expr(  in mkBVSignExt()
597     return newExprRef(Z3Expr(  in mkBVZeroExt()
603     return newExprRef(Z3Expr(Context, Z3_mk_extract(Context.Context, High, Low,  in mkBVExtract()
611     return newExprRef(Z3Expr(  in mkBVAddNoOverflow()
620     return newExprRef(Z3Expr(  in mkBVAddNoUnderflow()
629     return newExprRef(Z3Expr(  in mkBVSubNoOverflow()
638     return newExprRef(Z3Expr(  in mkBVSubNoUnderflow()
647     return newExprRef(Z3Expr(  in mkBVSDivNoOverflow()
655     return newExprRef(Z3Expr(  in mkBVNegNoOverflow()
663     return newExprRef(Z3Expr(  in mkBVMulNoOverflow()
672     return newExprRef(Z3Expr(  in mkBVMulNoUnderflow()
678     return newExprRef(  in mkBVConcat()
685     return newExprRef(Z3Expr(  in mkFPtoFP()
693     return newExprRef(Z3Expr(  in mkSBVtoFP()
701     return newExprRef(Z3Expr(  in mkUBVtoFP()
709     return newExprRef(Z3Expr(  in mkFPtoSBV()
716     return newExprRef(Z3Expr(  in mkFPtoUBV()
722     return newExprRef(Z3Expr(Context, b ? Z3_mk_true(Context.Context)  in mkBoolean()
733       return newExprRef(Z3Expr(  in mkBitvector()
745     return newExprRef(Z3Expr(Context, Literal));  in mkBitvector()
754     return newExprRef(Z3Expr(  in mkFloat()
760     return newExprRef(  in mkSymbol()
781     return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context)));  in getFloatRoundingMode()
850     SMTExprRef Assign = newExprRef(  in getInterpretation()
864     SMTExprRef Assign = newExprRef(  in getInterpretation()