From 22103c03228954b667f1a0261bcbb9fb0040076a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 12 Jan 2024 14:00:33 -0800
Subject: [PATCH] bugfix

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/smt/polysat/fixed_bits.cpp |  2 --
 src/sat/smt/polysat/viable.cpp     | 21 +++++++++++++++------
 2 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/src/sat/smt/polysat/fixed_bits.cpp b/src/sat/smt/polysat/fixed_bits.cpp
index 761c0fabd..4fce10ad4 100644
--- a/src/sat/smt/polysat/fixed_bits.cpp
+++ b/src/sat/smt/polysat/fixed_bits.cpp
@@ -34,11 +34,9 @@ namespace polysat {
     bool fixed_bits::check(rational const& val, fi_record& fi) {
         unsigned sz = c.size(m_var);
         rational bw = rational::power_of_two(sz);
-        // verbose_stream() << "check for fixed bits v" << m_var << "[" << sz << "] := " << val << "\n";
         for (auto const& s : m_fixed_slices) {
             rational sbw = rational::power_of_two(s.length);
             // slice is properly contained in bit-vector variable
-            // verbose_stream() << "  slice " << s.value << "[" << s.length << "]@" << s.offset << "\n";
             if (s.length <= sz && s.value != mod(machine_div2k(val, s.offset), sbw)) {
                 SASSERT(s.offset + s.length <= sz);
                 rational hi_val = s.value;
diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp
index 31dbfa81f..075852fba 100644
--- a/src/sat/smt/polysat/viable.cpp
+++ b/src/sat/smt/polysat/viable.cpp
@@ -638,20 +638,27 @@ namespace polysat {
         if (ebw < bw || aw != bw) {
             auto const& p2b = rational::power_of_two(bw);
             auto const& p2eb = rational::power_of_two(bw - ebw);
+            // let coeff = 2^{bw - ebw}
+            // let assume coeff * x \not\in [lo, t[
+            // Then value is chosen, min x . coeff * x >= t.
+            // In other words:
+            //
+            // coeff * (value - 1) <= t < coeff*value + 1
+            //
+            auto vlo = c.value(mod((e.value - 1) * p2eb, p2b), bw);
             auto vhi = c.value(mod(e.value * p2eb + 1, p2b), bw);
-            auto vlo = c.value(mod((e.value - 1) * p2eb - 1, p2b), bw);
-            // t in ] (value - 1) * 2^{bw - ebw} ; value * 2^{bw - ebw} ]
-            // t in [ (value - 1) * 2^{bw - ebw} - 1 ; value * 2^{bw - ebw} + 1 [
 
 #if 0
-            verbose_stream() << e.value << " " << t << "\n";
-            if (t.is_val()) verbose_stream() << "tval " << t.val() << "\n";
+            verbose_stream() << "value " << e.value << "\n";
+            verbose_stream() << "t " << t << "\n";
             verbose_stream() << "[" << vlo << " " << vhi << "[\n";
-            verbose_stream() << "bw " << ebw << " " << bw << " " << e.e->interval << " bw " << abw << " " << aw << " " << after.e->coeff << " " << after.e->interval << "\n";
+            verbose_stream() << "before bw " << ebw << " " << bw << " " << *e.e << "\nafter  bw " << abw << " " << aw << " " << *after.e << "\n";
             if (!t.is_val())
                 IF_VERBOSE(0, verbose_stream() << "symbolic t : " << t << "\n");
 #endif
             auto sc = cs.ult(t - vlo, vhi - vlo);
+            CTRACE("bv", sc.is_always_false(), c.display(tout));
+                
             VERIFY(!sc.is_always_false());
             if (!sc.is_always_true())
                 deps.push_back(c.propagate(sc, c.explain_weak_eval(sc)));
@@ -1011,6 +1018,8 @@ namespace polysat {
             out << e->coeff << " * v" << v << " " << e->interval << " ";
         else
             out << e->interval << " ";
+        for (auto const& d : e->deps)
+            out << d << " ";
         if (e->side_cond.size() <= 5)
             out << e->side_cond << " ";
         else