From 734609889552e733c141bacff2e5d8f3b4f567df Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 30 Jul 2016 11:22:34 -0700
Subject: [PATCH] fix unsat core extraction code in smt_context

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_conflict_resolution.cpp | 23 ++++++++++++++---------
 src/smt/smt_context.cpp             |  9 ++++-----
 src/solver/solver.cpp               |  1 +
 3 files changed, 19 insertions(+), 14 deletions(-)

diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp
index e3c2be123..6c7c71602 100644
--- a/src/smt/smt_conflict_resolution.cpp
+++ b/src/smt/smt_conflict_resolution.cpp
@@ -1334,8 +1334,9 @@ namespace smt {
         if (!m_ctx.is_marked(var)) {
             m_ctx.set_mark(var);
             m_unmark.push_back(var);
-            if (m_ctx.is_assumption(var)) 
-                m_assumptions.push_back(antecedent);
+        }
+        if (m_ctx.is_assumption(var)) {
+            m_assumptions.push_back(antecedent);
         }
     }
     
@@ -1373,7 +1374,7 @@ namespace smt {
         }
         
         while (true) {
-            TRACE("unsat_core_bug", tout << "js.get_kind(): " << js.get_kind() << ", idx: " << idx << "\n";);
+            TRACE("unsat_core_bug", tout << consequent << " js.get_kind(): " << js.get_kind() << ", idx: " << idx << "\n";);
             switch (js.get_kind()) {
             case b_justification::CLAUSE: {
                 clause * cls = js.get_clause();
@@ -1410,18 +1411,22 @@ namespace smt {
             default:
                 UNREACHABLE();
             }
-            
-            while (true) {
-                if (idx < 0) 
-                    goto end_unsat_core;
+
+            if (m_ctx.is_assumption(consequent.var())) {
+                m_assumptions.push_back(consequent);
+            }            
+            while (idx >= 0) {
                 literal l = m_assigned_literals[idx];
                 TRACE("unsat_core_bug", tout << "l: " << l << ", get_assign_level(l): " << m_ctx.get_assign_level(l) << ", is_marked(l): " << m_ctx.is_marked(l.var()) << "\n";);
-                if (m_ctx.get_assign_level(l) < search_lvl || idx == 0) 
-                    goto end_unsat_core;
+                if (m_ctx.get_assign_level(l) < search_lvl) 
+                    goto end_unsat_core;                
                 if (m_ctx.is_marked(l.var())) 
                     break;
                 idx--;
             }
+            if (idx < 0) { 
+                goto end_unsat_core;
+            }
 
             SASSERT(idx >= 0);
             consequent     = m_assigned_literals[idx];
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 3aeb623f9..88d0c8aff 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3044,7 +3044,7 @@ namespace smt {
             SASSERT(m_assumptions.empty());
             return; 
         }
-        obj_hashtable<expr> already_found_assumptions;
+        uint_set already_found_assumptions;
         literal_vector::const_iterator it  = m_conflict_resolution->begin_unsat_core();
         literal_vector::const_iterator end = m_conflict_resolution->end_unsat_core();
         for (; it != end; ++it) {
@@ -3053,10 +3053,9 @@ namespace smt {
             SASSERT(get_bdata(l.var()).m_assumption);
             if (!m_literal2assumption.contains(l.index())) l.neg();
             SASSERT(m_literal2assumption.contains(l.index()));
-            expr * a = m_literal2assumption[l.index()];
-            if (!already_found_assumptions.contains(a)) {
-                already_found_assumptions.insert(a);
-                m_unsat_core.push_back(a);
+            if (!already_found_assumptions.contains(l.index())) {
+                already_found_assumptions.insert(l.index());
+                m_unsat_core.push_back(m_literal2assumption[l.index()]);
             }
         }
         reset_assumptions();
diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp
index 7b11317d1..b0ae6a540 100644
--- a/src/solver/solver.cpp
+++ b/src/solver/solver.cpp
@@ -19,6 +19,7 @@ Notes:
 #include"solver.h"
 #include"model_evaluator.h"
 #include"ast_util.h"
+#include"ast_pp.h"
 
 unsigned solver::get_num_assertions() const {
     NOT_IMPLEMENTED_YET();