From b2191cab020718362d544bad6e7624cf30948c97 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 21 Oct 2017 18:46:35 -0400 Subject: [PATCH] disable eager clear of check-sat-result to fix #1318 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 9615e86ce..77dce80c8 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -774,7 +774,6 @@ bool cmd_context::is_func_decl(symbol const & s) const { } void cmd_context::insert(symbol const & s, func_decl * f) { - m_check_sat_result = 0; if (!m_check_logic(f)) { throw cmd_exception(m_check_logic.get_last_error()); } @@ -805,7 +804,6 @@ void cmd_context::insert(symbol const & s, func_decl * f) { } void cmd_context::insert(symbol const & s, psort_decl * p) { - m_check_sat_result = 0; if (m_psort_decls.contains(s)) { throw cmd_exception("sort already defined ", s); } @@ -819,7 +817,6 @@ void cmd_context::insert(symbol const & s, psort_decl * p) { void cmd_context::insert(symbol const & s, unsigned arity, sort *const* domain, expr * t) { expr_ref _t(t, m()); - m_check_sat_result = 0; if (m_builtin_decls.contains(s)) { throw cmd_exception("invalid macro/named expression, builtin symbol ", s); }