From 66469bb678c20ef98c1f78e3818e6a6e22ad245e Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 12 Oct 2022 13:20:34 +0200
Subject: [PATCH] Don't leave propagation loop too early (cause of unsoundness
 in bench0)

---
 src/math/polysat/solver.cpp | 9 ++++++---
 src/math/polysat/viable.cpp | 1 +
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index eb765dd92..590d3f08b 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -293,7 +293,7 @@ namespace polysat {
     * Propagate assignment to a pvar
     */
     void solver::propagate(pvar v) {
-        LOG_H2("Propagate v" << v);
+        LOG_H2("Propagate " << assignment_pp(*this, v, get_value(v)));
         SASSERT(!m_locked_wlist);
         DEBUG_CODE(m_locked_wlist = v;);
         auto& wlist = m_pwatch[v];
@@ -749,8 +749,11 @@ namespace polysat {
                 LOG(bool_justification_pp(m_bvars, lit));
                 LOG("Literal " << lit << " is " << lit2cnstr(lit));
                 LOG("Conflict: " << m_conflict);
-                if (m_bvars.level(var) <= base_level())
-                    break;
+                if (m_bvars.level(var) <= base_level()) {
+                    // NOTE: the levels of boolean literals on the stack aren't always ordered by level (cf. replay functionality in pop_levels).
+                    //       Thus we can only skip base level literals here, instead of aborting the loop.
+                    continue;
+                }
                 SASSERT(!m_bvars.is_assumption(var));
                 if (m_bvars.is_decision(var)) {
                     revert_bool_decision(lit);
diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index 8daabb31e..3f659328b 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -633,6 +633,7 @@ namespace polysat {
     }
 
     bool viable::resolve(pvar v, conflict& core) {
+        DEBUG_CODE( log(v); );
         if (has_viable(v))
             return false;
         entry const* e = m_units[v];