288   void addConstraint(const SMTExprRef &Exp) const override {  in addConstraint()
289     Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST);  in addConstraint()
301   SMTExprRef newExprRef(const SMTExpr &Exp) {  in newExprRef()  argument
302     auto It = CachedExprs.insert(toZ3Expr(Exp));  in newExprRef()
315   SMTSortRef getSort(const SMTExprRef &Exp) override {  in getSort()  argument
317         Z3Sort(Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST)));  in getSort()
336   SMTExprRef mkBVNeg(const SMTExprRef &Exp) override {  in mkBVNeg()  argument
338         Z3Expr(Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST)));  in mkBVNeg()
341   SMTExprRef mkBVNot(const SMTExprRef &Exp) override {  in mkBVNot()  argument
343         Z3Expr(Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST)));  in mkBVNot()
346   SMTExprRef mkNot(const SMTExprRef &Exp) override {  in mkNot()  argument
348         Z3Expr(Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST)));  in mkNot()
493   SMTExprRef mkFPNeg(const SMTExprRef &Exp) override {  in mkFPNeg()  argument
495         Z3Expr(Context, Z3_mk_fpa_neg(Context.Context, toZ3Expr(*Exp).AST)));  in mkFPNeg()
498   SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) override {  in mkFPIsInfinite()  argument
500         Context, Z3_mk_fpa_is_infinite(Context.Context, toZ3Expr(*Exp).AST)));  in mkFPIsInfinite()
503   SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) override {  in mkFPIsNaN()  argument
505         Z3Expr(Context, Z3_mk_fpa_is_nan(Context.Context, toZ3Expr(*Exp).AST)));  in mkFPIsNaN()
508   SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) override {  in mkFPIsNormal()  argument
510         Context, Z3_mk_fpa_is_normal(Context.Context, toZ3Expr(*Exp).AST)));  in mkFPIsNormal()
513   SMTExprRef mkFPIsZero(const SMTExprRef &Exp) override {  in mkFPIsZero()  argument
515         Context, Z3_mk_fpa_is_zero(Context.Context, toZ3Expr(*Exp).AST)));  in mkFPIsZero()
593   SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) override {  in mkBVSignExt()  argument
595         Context, Z3_mk_sign_ext(Context.Context, i, toZ3Expr(*Exp).AST)));  in mkBVSignExt()
598   SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) override {  in mkBVZeroExt()  argument
600         Context, Z3_mk_zero_ext(Context.Context, i, toZ3Expr(*Exp).AST)));  in mkBVZeroExt()
604                          const SMTExprRef &Exp) override {  in mkBVExtract()  argument
606                                                     toZ3Expr(*Exp).AST)));  in mkBVExtract()
656   SMTExprRef mkBVNegNoOverflow(const SMTExprRef &Exp) override {  in mkBVNegNoOverflow()  argument
658         Context, Z3_mk_bvneg_no_overflow(Context.Context, toZ3Expr(*Exp).AST)));  in mkBVNegNoOverflow()
768   llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth,  in getBitvector()  argument
772                     Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST),  in getBitvector()
777   bool getBoolean(const SMTExprRef &Exp) override {  in getBoolean()  argument
778     return Z3_get_bool_value(Context.Context, toZ3Expr(*Exp).AST) == Z3_L_TRUE;  in getBoolean()
845   bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) override {  in getInterpretation()  argument
848         Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));  in getInterpretation()
859   bool getInterpretation(const SMTExprRef &Exp, llvm::APFloat &Float) override {  in getInterpretation()  argument
862         Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));  in getInterpretation()