265   Z3_solver Solver;  member in __anon13641eda0111::Z3Solver
274   Z3Solver() : Solver(Z3_mk_simple_solver(Context.Context)) {  in Z3Solver()
275     Z3_solver_inc_ref(Context.Context, Solver);  in Z3Solver()
284     if (Solver)  in ~Z3Solver()
285       Z3_solver_dec_ref(Context.Context, Solver);  in ~Z3Solver()
289     Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST);  in addConstraint()
846     Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));  in getInterpretation()
860     Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));  in getInterpretation()
874     Z3_lbool res = Z3_solver_check(Context.Context, Solver);  in check()
884   void push() override { return Z3_solver_push(Context.Context, Solver); }  in push()
887     assert(Z3_solver_get_num_scopes(Context.Context, Solver) >= NumStates);  in pop()
888     return Z3_solver_pop(Context.Context, Solver, NumStates);  in pop()
894   void reset() override { Z3_solver_reset(Context.Context, Solver); }  in reset()
897     OS << Z3_solver_to_string(Context.Context, Solver);  in print()