mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 05:13:39 +00:00
Code Activity

fixed so produce-interpolants option is not needed for compute-interpolant

Browse source
This commit is contained in:
Ken McMillan 2013-04-15 12:22:04 -07:00
parent e651f45bc0
commit 6495d7b88c
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/cmd_context/interpolant_cmds.cpp
View file

@ -124,15 +124,15 @@ static void get_and_check_interpolant(cmd_context & ctx, expr * t) {
static void compute_interpolant_and_maybe_check(cmd_context & ctx, expr * t, bool check){ static void compute_interpolant_and_maybe_check(cmd_context & ctx, expr * t, bool check){
// get the proof, if there is one
check_can_interpolate(ctx);
// create a fresh solver suitable for interpolation // create a fresh solver suitable for interpolation
bool proofs_enabled, models_enabled, unsat_core_enabled; bool proofs_enabled, models_enabled, unsat_core_enabled;
params_ref p; params_ref p;
ast_manager &_m = ctx.m(); ast_manager &_m = ctx.m();
// TODO: the following is a HACK to enable proofs in the old smt solver
// When we stop using that solver, this hack can be removed
_m.toggle_proof_mode(PGM_FINE);
ctx.params().get_solver_params(_m, p, proofs_enabled, models_enabled, unsat_core_enabled); ctx.params().get_solver_params(_m, p, proofs_enabled, models_enabled, unsat_core_enabled);
p.set_bool("proof", true);
scoped_ptr<solver> sp = (ctx.get_interpolating_solver_factory())(_m, p, true, models_enabled, false, ctx.get_logic()); scoped_ptr<solver> sp = (ctx.get_interpolating_solver_factory())(_m, p, true, models_enabled, false, ctx.get_logic());
ptr_vector<ast> cnsts; ptr_vector<ast> cnsts;