From b8f59d15c6d71658784de298590f7327cf6b303e Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Thu, 14 Dec 2023 14:29:46 +0100
Subject: [PATCH] Fix propagation

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

diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index b8eddb457..b9d41cec9 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -866,12 +866,9 @@ namespace polysat {
             m_free_pvars.unassign_var_eh(v);
             return;
         case find_t::singleton:
-            // Any propagations should have been discovered by viable::intersect.
-            // The fallback solver currently does not detect propagations, because we would need to handle justifications differently.
-            // However, this case may still occur if during viable::intersect, we run into the refinement budget,
-            // but here, we continue refinement and actually succeed until propagation.
-            // ???
-            UNREACHABLE();
+            // Propagations are intended to be discovered by viable::intersect.
+            // However, changes in the slicing structure currently don't trigger a check for interval-propagated values,
+            // which means this call to find_viable may have had more intervals ot work with than the previous viable::intersect.
             SASSERT(m_justification[v].is_propagation_by_viable());
             return;
         case find_t::multiple:
@@ -892,8 +889,10 @@ namespace polysat {
     }
 
     void solver::assign_propagate_by_viable(pvar v, rational const& val) {
+        LOG("Propagation by viable: " << assignment_pp(*this, v, val));
         unsigned lvl = 0;
         for (sat::literal const lit : m_viable.get_propagation_reason(v)) {
+            LOG("    due to " << lit_pp(*this, lit));
             VERIFY(m_bvars.is_assigned(lit));
             lvl = std::max(lvl, m_bvars.level(lit));
         }
diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index 9d93cb0c0..cff1458d6 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -204,6 +204,8 @@ namespace polysat {
         unsigned const begin = m_propagation_reason_storage.size();
 
         auto add_reason = [this](signed_constraint c) {
+            if (c.is_always_true())
+                return;
             s.try_assign_eval(c);
             m_propagation_reason_storage.push_back(c.blit());
         };