From 53aded3198738e64f2e8f1cf3db44d0bb4db5535 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 25 Jul 2019 18:55:44 -0700
Subject: [PATCH] fix #2416 exposed bugs: unsat-core extraction in combination
 with chronological backracking, equivalence elimination in combination with
 PB constraints

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/maxres.cpp       |  2 +-
 src/sat/ba_solver.cpp    |  4 +---
 src/sat/sat_elim_eqs.cpp |  3 ++-
 src/sat/sat_solver.cpp   | 24 ++++++++++--------------
 4 files changed, 14 insertions(+), 19 deletions(-)

diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 483db7e70..edfb043ac 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -133,7 +133,7 @@ public:
         m_max_core_size(3),
         m_maximize_assignment(false),
         m_max_correction_set_size(3),
-        m_pivot_on_cs(true)
+        m_pivot_on_cs(true)       
     {
         switch(st) {
         case s_primal:
diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index 99dab4ecf..2de772b55 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -2085,7 +2085,6 @@ namespace sat {
       \brief return true to keep watching literal.
     */
     bool ba_solver::propagate(literal l, ext_constraint_idx idx) {
-        TRACE("ba", tout << l << "\n";);
         SASSERT(value(l) == l_true);
         constraint& c = index2constraint(idx);
         if (c.lit() != null_literal && l.var() == c.lit().var()) {
@@ -2813,7 +2812,7 @@ namespace sat {
         // literal is assigned to false.        
         unsigned sz = c.size();
         unsigned bound = c.k();
-        TRACE("ba", tout << "assign: " << c.lit() << ": " << ~alit << "@" << lvl(~alit) << "\n";);
+        TRACE("ba", tout << "assign: " << c.lit() << ": " << ~alit << "@" << lvl(~alit) << " " << c << "\n";);
 
         SASSERT(0 < bound && bound <= sz);
         if (bound == sz) {
@@ -3242,7 +3241,6 @@ namespace sat {
 
         // pre-condition is that the literals, except c.lit(), in c are unwatched.
         if (c.id() == _bad_id) std::cout << "recompile: " << c << "\n";
-        // IF_VERBOSE(0, verbose_stream() << c << "\n";);
         m_weights.resize(2*s().num_vars(), 0);
         for (literal l : c) {
             ++m_weights[l.index()];
diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp
index 0054c8d65..e577846e0 100644
--- a/src/sat/sat_elim_eqs.cpp
+++ b/src/sat/sat_elim_eqs.cpp
@@ -230,7 +230,8 @@ namespace sat {
             literal  l(v, false);
             literal r  = roots[v];
             SASSERT(v != r.var());
-            bool root_ok = !m_solver.is_external(v) || m_solver.set_root(l, r);
+            bool set_root = m_solver.set_root(l, r);
+            bool root_ok = !m_solver.is_external(v) || set_root;
             if (m_solver.is_assumption(v) || (m_solver.is_external(v) && (m_solver.is_incremental() || !root_ok))) {
                 // cannot really eliminate v, since we have to notify extension of future assignments
                 m_solver.mk_bin_clause(~l, r, false);
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index d89ab74fd..8787e70eb 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -301,8 +301,10 @@ namespace sat {
     clause* solver::mk_clause(unsigned num_lits, literal * lits, bool learned) {
         m_model_is_current = false;
         DEBUG_CODE({
-            for (unsigned i = 0; i < num_lits; i++)
-                SASSERT(m_eliminated[lits[i].var()] == false);
+                for (unsigned i = 0; i < num_lits; i++) {
+                    CTRACE("sat", m_eliminated[lits[i].var()], tout << lits[i] << " was eliminated\n";);
+                    SASSERT(m_eliminated[lits[i].var()] == false);
+                }
         });
 
         if (m_user_scope_literals.empty()) {
@@ -2908,26 +2910,20 @@ namespace sat {
 
         justification js = m_conflict;
 
+        int init_sz = init_trail_size();
         while (true) {
             process_consequent_for_unsat_core(consequent, js);
-            while (idx >= 0) {
-                literal l = m_trail[idx];
-                if (is_marked(l.var()))
+            while (idx >= init_sz) {
+                consequent = m_trail[idx];
+                if (is_marked(consequent.var()) && lvl(consequent) == m_conflict_lvl)
                     break;
                 idx--;
             }
-
-            if (idx < 0) {
+            if (idx < init_sz) {
                 break;
             }
-            consequent     = m_trail[idx];
-            if (lvl(consequent) < m_conflict_lvl) {
-                TRACE("sat", tout << consequent << " at level " << lvl(consequent) << "\n";);
-                break;
-            }
-            bool_var c_var = consequent.var();
             SASSERT(lvl(consequent) == m_conflict_lvl);
-            js             = m_justification[c_var];
+            js = m_justification[consequent.var()];
             idx--;
         }
         reset_unmark(old_size);