From c3ffbf05db03c1a09b6ca8fe596b1c017b537f78 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Sat, 11 May 2024 14:16:18 +0200
Subject: [PATCH] fix bv type error in projection check

---
 src/sat/smt/polysat/project_interval.cpp | 16 ++++++++++++----
 src/sat/smt/polysat/project_interval.h   |  2 +-
 2 files changed, 13 insertions(+), 5 deletions(-)

diff --git a/src/sat/smt/polysat/project_interval.cpp b/src/sat/smt/polysat/project_interval.cpp
index e3b5cc6ff..15a03fa5c 100644
--- a/src/sat/smt/polysat/project_interval.cpp
+++ b/src/sat/smt/polysat/project_interval.cpp
@@ -170,14 +170,14 @@ namespace polysat {
         });
     }
 
-    lbool project_interval::try_project(pvar const w, unsigned const w_off, unsigned const w_sz, rational const& value, unsigned const max_level) {
+    lbool project_interval::try_project(pvar const w, unsigned const w_off, unsigned const w_sz, rational const& w_value, unsigned const max_level) {
         SASSERT(w != null_var);
         SASSERT_EQ(c.size(w), w_sz);
         SASSERT(w != m_var);
         if (w == m_var)
             return l_undef;
 
-        // verbose_stream() << "v" << m_var << " size " << c.size(m_var) << " -> v" << w << " size " << w_sz << " offset " << w_off << " level " << w_level << "\n";
+        // verbose_stream() << "v" << m_var << " size " << c.size(m_var) << " -> v" << w << " size " << w_sz << " offset " << w_off << " max_level " << max_level << "\n";
 
         // Let:
         // v = m_var[m_width-1:0]
@@ -244,15 +244,23 @@ namespace polysat {
         SASSERT(ivl.is_proper() && !ivl.is_empty());
 
         // interval propagation worked but it doesn't conflict the currently assigned value
-        if (!ivl.contains(value))
+        rational const& y_value = mod2k(w_value, y_sz);
+        // verbose_stream() << "interval: " << ivl << "\n";
+        // verbose_stream() << "w_value: " << w_value << "  contained: " << ivl.contains(w_value) << "\n";
+        // verbose_stream() << "y_value: " << y_value << "  contained: " << ivl.contains(y_value) << "\n";
+        if (!ivl.contains(y_value))
             return l_undef;
 
         // now: m_deps implies 2^w_shift * w is not in ivl
         signed_constraint sc = ~cs().ult(w_shift * (c.var(w) - ivl.lo()), w_shift * (ivl.hi() - ivl.lo()));
+        // verbose_stream() << "propagate sc: " << sc << "    weak-eval: " << c.weak_eval(sc) << "\n";
+        VERIFY(c.weak_eval(sc) != l_true);
         dependency d = c.propagate(sc, m_deps, "propagate from containing slice");
+        // verbose_stream() << "     sc is dep " << d << "\n";
+        // TODO: add as axiom instead???
 
         m_explain.push_back(d);
-        m_explain.push_back(dep_target_fixed(w, value));  // w ~ value
+        m_explain.push_back(dep_target_fixed(w, w_value));  // w ~ w_value
 
         IF_VERBOSE(3, {
             verbose_stream() << "=>  v" << w << "[" << y_sz << "] not in " << ivl << "\n";
diff --git a/src/sat/smt/polysat/project_interval.h b/src/sat/smt/polysat/project_interval.h
index 5af6088a9..94320d983 100644
--- a/src/sat/smt/polysat/project_interval.h
+++ b/src/sat/smt/polysat/project_interval.h
@@ -83,7 +83,7 @@ namespace polysat {
          */
         static r_interval chop_off_lower(r_interval const& i, unsigned Ny, unsigned Nz, rational const* z_fixed_value = nullptr);
 
-        lbool try_project(pvar const w, unsigned const w_off, unsigned const w_sz, rational const& value, unsigned const max_level);
+        lbool try_project(pvar const w, unsigned const w_off, unsigned const w_sz, rational const& w_value, unsigned const max_level);
         r_interval chop_off_upper(r_interval ivl, unsigned max_level, unsigned x_sz, unsigned y_sz, unsigned z_sz);
         r_interval chop_off_lower(r_interval ivl, unsigned max_level, unsigned y_sz, unsigned z_sz);