From 8d6a091083fdf7a40fe6c906bb8a39c0a813f909 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 7 Nov 2012 07:36:40 -0800 Subject: [PATCH] fixed bugs found in regression tests Signed-off-by: Leonardo de Moura --- src/cmd_context/cmd_context.cpp | 6 ++++++ src/cmd_context/pdecl.cpp | 1 + src/solver/solver_na2as.cpp | 23 ++++++++++++++--------- 3 files changed, 21 insertions(+), 9 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 2d0d349d7..1be6fe395 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1235,6 +1235,12 @@ static void restore(ast_manager & m, ptr_vector & c, unsigned old_sz) { } void cmd_context::restore_assertions(unsigned old_sz) { + if (!has_manager()) { + // restore_assertions invokes m(), so if cmd_context does not have a manager, it will try to create one. + SASSERT(old_sz == m_assertions.size()); + SASSERT(m_assertions.empty()); + return; + } SASSERT(old_sz <= m_assertions.size()); SASSERT(!m_interactive_mode || m_assertions.size() == m_assertion_strings.size()); restore(m(), m_assertions, old_sz); diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp index 9d06cb115..6b55d4072 100644 --- a/src/cmd_context/pdecl.cpp +++ b/src/cmd_context/pdecl.cpp @@ -785,6 +785,7 @@ psort * pdecl_manager::mk_psort_cnst(sort * s) { } psort * pdecl_manager::register_psort(psort * n) { + TRACE("register_psort", tout << "registering psort...\n"; n->display(tout); tout << "\n";); psort * r = m_table.insert_if_not_there(n); if (r != n) { del_decl_core(n); diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp index f6d7414a5..e71a9873b 100644 --- a/src/solver/solver_na2as.cpp +++ b/src/solver/solver_na2as.cpp @@ -31,15 +31,20 @@ solver_na2as::~solver_na2as() { } void solver_na2as::assert_expr(expr * t, expr * a) { - SASSERT(m_manager != 0); - SASSERT(is_uninterp_const(a)); - SASSERT(m_manager->is_bool(a)); - TRACE("solver_na2as", tout << "asserting\n" << mk_ismt2_pp(t, *m_manager) << "\n" << mk_ismt2_pp(a, *m_manager) << "\n";); - m_manager->inc_ref(a); - m_assumptions.push_back(a); - expr_ref new_t(*m_manager); - new_t = m_manager->mk_implies(a, t); - assert_expr(new_t); + if (a == 0) { + assert_expr(t); + } + else { + SASSERT(m_manager != 0); + SASSERT(is_uninterp_const(a)); + SASSERT(m_manager->is_bool(a)); + TRACE("solver_na2as", tout << "asserting\n" << mk_ismt2_pp(t, *m_manager) << "\n" << mk_ismt2_pp(a, *m_manager) << "\n";); + m_manager->inc_ref(a); + m_assumptions.push_back(a); + expr_ref new_t(*m_manager); + new_t = m_manager->mk_implies(a, t); + assert_expr(new_t); + } } void solver_na2as::init(ast_manager & m, symbol const & logic) {