From 0a6b03808cdfbad3057d9e2402584bae4e405f9d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 Jul 2016 12:35:54 -0700 Subject: [PATCH] fix core extraction for QF_BV theory/inc_sat_solver based on regressions pointed out by Matthias Heizmann and Tjark Weber Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 14 +------------- 1 file changed, 1 insertion(+), 13 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index d773a3066..5f9de116d 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1473,19 +1473,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions scoped_timer timer(timeout, &eh); scoped_rlimit _rlimit(m().limit(), rlimit); try { - if (produce_unsat_cores()) { - expr_ref_vector asms(m()); - asms.append(num_assumptions, assumptions); - for (unsigned i = 0; false && i < m_assertion_names.size(); ++i) { - if (m_assertion_names[i]) { - asms.push_back(m_assertion_names[i]); - } - } - r = m_solver->check_sat(asms); - } - else { - r = m_solver->check_sat(num_assumptions, assumptions); - } + r = m_solver->check_sat(num_assumptions, assumptions); } catch (z3_error & ex) { throw ex;