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

fixed pop issue and interpolation proof mode issue

Browse source
This commit is contained in:
Ken McMillan 2014-08-26 13:46:53 -07:00
parent 97c5d09de1
commit 51aa10821e
2 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/cmd_context/interpolant_cmds.cpp
View file

@ -33,6 +33,7 @@ Notes:
#include"iz3checker.h" #include"iz3checker.h"
#include"iz3profiling.h" #include"iz3profiling.h"
#include"interp_params.hpp" #include"interp_params.hpp"
#include"scoped_proof.h"
static void show_interpolant_and_maybe_check(cmd_context & ctx, static void show_interpolant_and_maybe_check(cmd_context & ctx,
ptr_vector<ast> &cnsts, ptr_vector<ast> &cnsts,
@ -153,7 +154,7 @@ static void compute_interpolant_and_maybe_check(cmd_context & ctx, expr * t, par
ast_manager &_m = ctx.m(); ast_manager &_m = ctx.m();
// TODO: the following is a HACK to enable proofs in the old smt solver // 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 // When we stop using that solver, this hack can be removed
_m.toggle_proof_mode(PGM_FINE); scoped_proof_mode spm(_m,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); 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());

2
src/solver/solver_na2as.cpp
View file

@ -82,7 +82,7 @@ void solver_na2as::pop(unsigned n) {
} }
void solver_na2as::restore_assumptions(unsigned old_sz) { void solver_na2as::restore_assumptions(unsigned old_sz) {
SASSERT(old_sz == 0); // SASSERT(old_sz == 0);
for (unsigned i = old_sz; i < m_assumptions.size(); i++) { for (unsigned i = old_sz; i < m_assumptions.size(); i++) {
m_manager.dec_ref(m_assumptions[i]); m_manager.dec_ref(m_assumptions[i]);
} }