286   void addConstraint(const SMTExprRef &Exp) const override {  in addConstraint()
287     Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST);  in addConstraint()
299   SMTExprRef newExprRef(const SMTExpr &Exp) {  in newExprRef()  argument
300     auto It = CachedExprs.insert(toZ3Expr(Exp));  in newExprRef()
313   SMTSortRef getSort(const SMTExprRef &Exp) override {  in getSort()  argument
315         Z3Sort(Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST)));  in getSort()
334   SMTExprRef mkBVNeg(const SMTExprRef &Exp) override {  in mkBVNeg()  argument
336         Z3Expr(Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST)));  in mkBVNeg()
339   SMTExprRef mkBVNot(const SMTExprRef &Exp) override {  in mkBVNot()  argument
341         Z3Expr(Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST)));  in mkBVNot()
344   SMTExprRef mkNot(const SMTExprRef &Exp) override {  in mkNot()  argument
346         Z3Expr(Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST)));  in mkNot()
491   SMTExprRef mkFPNeg(const SMTExprRef &Exp) override {  in mkFPNeg()  argument
493         Z3Expr(Context, Z3_mk_fpa_neg(Context.Context, toZ3Expr(*Exp).AST)));  in mkFPNeg()
496   SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) override {  in mkFPIsInfinite()  argument
498         Context, Z3_mk_fpa_is_infinite(Context.Context, toZ3Expr(*Exp).AST)));  in mkFPIsInfinite()
501   SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) override {  in mkFPIsNaN()  argument
503         Z3Expr(Context, Z3_mk_fpa_is_nan(Context.Context, toZ3Expr(*Exp).AST)));  in mkFPIsNaN()
506   SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) override {  in mkFPIsNormal()  argument
508         Context, Z3_mk_fpa_is_normal(Context.Context, toZ3Expr(*Exp).AST)));  in mkFPIsNormal()
511   SMTExprRef mkFPIsZero(const SMTExprRef &Exp) override {  in mkFPIsZero()  argument
513         Context, Z3_mk_fpa_is_zero(Context.Context, toZ3Expr(*Exp).AST)));  in mkFPIsZero()
591   SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) override {  in mkBVSignExt()  argument
593         Context, Z3_mk_sign_ext(Context.Context, i, toZ3Expr(*Exp).AST)));  in mkBVSignExt()
596   SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) override {  in mkBVZeroExt()  argument
598         Context, Z3_mk_zero_ext(Context.Context, i, toZ3Expr(*Exp).AST)));  in mkBVZeroExt()
602                          const SMTExprRef &Exp) override {  in mkBVExtract()  argument
604                                                     toZ3Expr(*Exp).AST)));  in mkBVExtract()
654   SMTExprRef mkBVNegNoOverflow(const SMTExprRef &Exp) override {  in mkBVNegNoOverflow()  argument
656         Context, Z3_mk_bvneg_no_overflow(Context.Context, toZ3Expr(*Exp).AST)));  in mkBVNegNoOverflow()
766   llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth,  in getBitvector()  argument
770                     Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST),  in getBitvector()
775   bool getBoolean(const SMTExprRef &Exp) override {  in getBoolean()  argument
776     return Z3_get_bool_value(Context.Context, toZ3Expr(*Exp).AST) == Z3_L_TRUE;  in getBoolean()
843   bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) override {  in getInterpretation()  argument
846         Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));  in getInterpretation()
857   bool getInterpretation(const SMTExprRef &Exp, llvm::APFloat &Float) override {  in getInterpretation()  argument
860         Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));  in getInterpretation()