fix #4955

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Jan 20, 2021 · dc43826 · dc43826
1 parent 3bc18ab
commit dc43826
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 1 deletion.
diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp
@@ -54,8 +54,13 @@ namespace sat {
                     literal r2 = norm(roots, l2);
                     if (r1 == r2) {
                         m_solver.assign_unit(r1);
-                        if (m_solver.inconsistent())
+                        if (m_solver.inconsistent()) {
+                            ++it;
+                            for (; it != end; ++it, ++itprev)
+                                *itprev = *it;
+                            wlist.set_end(itprev);
                             return;
+                        }
                         // consume unit
                         continue;
                     }
@@ -97,6 +102,7 @@ namespace sat {
         for (; it != end; ++it) {
             clause & c     = *(*it);
             TRACE("sats", tout << "processing: " << c << "\n";);
+            TRACE("scc_details", m_solver.display_watches(tout););
             unsigned sz    = c.size();
             unsigned i;
             for (i = 0; i < sz; i++) {

diff --git a/src/sat/sat_scc.cpp b/src/sat/sat_scc.cpp
@@ -220,6 +220,7 @@ namespace sat {
                 frames.pop_back();
             }
         }
+        TRACE("scc_details", m_solver.display_watches(tout););
         for (unsigned i = 0; i < m_solver.num_vars(); ++i) {
             if (roots[i] == null_literal) {
                 roots[i] = literal(i, false);