From f1d9228b943e40188720083ecb9bae7206722343 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 20 Jan 2015 16:30:46 -0800 Subject: [PATCH] fix bug in context push/pop for sat solver Signed-off-by: Nikolaj Bjorner --- src/opt/maxres.cpp | 2 +- src/sat/sat_solver.cpp | 5 ++++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 209601c78..6bc0cfa9b 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -925,7 +925,7 @@ public: } void verify_assignment() { - IF_VERBOSE(0, verbose_stream() << "verify assignment\n";); + IF_VERBOSE(1, verbose_stream() << "verify assignment\n";); ref smt_solver = mk_smt_solver(m, m_params, symbol()); for (unsigned i = 0; i < s().get_num_assertions(); ++i) { smt_solver->assert_expr(s().get_assertion(i)); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index a2d39d3ea..817fb2c23 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -930,8 +930,11 @@ namespace sat { void solver::reinit_assumptions() { if (tracking_assumptions() && scope_lvl() == 0) { - TRACE("sat", tout << m_assumptions.size() << "\n";); + TRACE("sat", tout << m_assumptions << "\n";); push(); + for (unsigned i = 0; !inconsistent() && i < m_user_scope_literals.size(); ++i) { + assign(~m_user_scope_literals[i], justification()); + } for (unsigned i = 0; !inconsistent() && i < m_assumptions.size(); ++i) { assign(m_assumptions[i], justification()); }