From 8f862f8fedab42a79d424707b9159fd577bcc9f3 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 9 Jul 2016 12:35:11 -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 <nbjorner@microsoft.com>
---
 src/cmd_context/cmd_context.cpp       |  2 +-
 src/sat/sat_solver/inc_sat_solver.cpp | 15 ++++++++++++---
 2 files changed, 13 insertions(+), 4 deletions(-)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index d4c7a1a54..d773a3066 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1476,7 +1476,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * 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) {
+                for (unsigned i = 0; false && i < m_assertion_names.size(); ++i) {
                     if (m_assertion_names[i]) {
                         asms.push_back(m_assertion_names[i]);
                     }
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 65f62ec0e..766ed52be 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -135,7 +135,6 @@ public:
         lbool r = internalize_formulas();
         if (r != l_true) return r;
         r = internalize_assumptions(sz, assumptions, dep2asm);
-        SASSERT(sz == m_asms.size());
         if (r != l_true) return r;
 
         r = m_solver.check(m_asms.size(), m_asms.c_ptr(), m_weights.c_ptr(), max_weight);
@@ -147,7 +146,7 @@ public:
             break;
         case l_false:
             // TBD: expr_dependency core is not accounted for.
-            if (sz > 0) {
+            if (!m_asms.empty()) {
                 extract_core(dep2asm);
             }
             break;
@@ -314,7 +313,7 @@ private:
     }
 
     lbool internalize_assumptions(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) {
-        if (sz == 0) {
+        if (sz == 0 && get_num_assumptions() == 0) {
             m_asms.shrink(0);
             return l_true;
         }
@@ -322,6 +321,9 @@ private:
         for (unsigned i = 0; i < sz; ++i) {
             g->assert_expr(asms[i], m.mk_leaf(asms[i]));
         }
+        for (unsigned i = 0; i < get_num_assumptions(); ++i) {
+            g->assert_expr(get_assumption(i), m.mk_leaf(get_assumption(i)));
+        }
         lbool res = internalize_goal(g, dep2asm);
         if (res == l_true) {
             extract_assumptions(sz, asms, dep2asm);
@@ -355,6 +357,13 @@ private:
                 ++j;
             }
         }
+        for (unsigned i = 0; i < get_num_assumptions(); ++i) {
+            if (dep2asm.find(get_assumption(i), lit)) {
+                SASSERT(lit.var() <= m_solver.num_vars());
+                m_asms.push_back(lit);
+            }
+        }
+
         SASSERT(dep2asm.size() == m_asms.size());
     }