From 82f1e81ac24fe34d718a237fbc9df74ea847ba05 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 19 Jan 2015 00:50:08 +0000 Subject: [PATCH 1/2] fix build errors on gcc Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_aux.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index ffc8314e0..37cbf7bc0 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -417,7 +417,7 @@ namespace smt { template void theory_arith::atom::display(theory_arith const& th, std::ostream& out) const { literal l(get_bool_var(), !m_is_true); - out << "v" << get_var() << " " << get_bound_kind() << " " << get_k() << " "; + out << "v" << bound::get_var() << " " << bound::get_bound_kind() << " " << get_k() << " "; out << l << ":"; th.get_context().display_detailed_literal(out, l); } @@ -747,7 +747,7 @@ namespace smt { template void theory_arith::derived_bound::display(theory_arith const& th, std::ostream& out) const { - out << "v" << m_var << " " << get_bound_kind() << " " << get_value(); + out << "v" << bound::get_var() << " " << bound::get_bound_kind() << " " << bound::get_value(); ast_manager& m = th.get_manager(); for (unsigned i = 0; i < m_eqs.size(); ++i) { From f1d9228b943e40188720083ecb9bae7206722343 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 20 Jan 2015 16:30:46 -0800 Subject: [PATCH 2/2] 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()); }