From 3d73fe55c71e1a875f3e0691fa8e7f205bcf548f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 Jul 2016 05:31:49 -0700 Subject: [PATCH] track assumptions when calling check-sat. regression detected by Tjark Weber running core extraction Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 5f9de116d..d4c7a1a54 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1473,7 +1473,19 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions scoped_timer timer(timeout, &eh); scoped_rlimit _rlimit(m().limit(), rlimit); try { - r = m_solver->check_sat(num_assumptions, assumptions); + if (produce_unsat_cores()) { + expr_ref_vector asms(m()); + asms.append(num_assumptions, assumptions); + for (unsigned i = 0; 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); + } } catch (z3_error & ex) { throw ex;