fix prefix constraint

Z3Prover · May 14, 2024 · a4f14fa · a4f14fa
1 parent 1f68612
commit a4f14fa
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp
@@ -974,9 +974,11 @@ v0[19] := 0 v0 [-131062 ; 0[ := [-131062;0[  src ~4 <= 43691*v0;
 #endif
             // for simplicity, we fix the evaluation of the stored upper bits
             // (alternative would be to track sub-ranges of extracted symbolic bounds)
-            auto sc = cs.fixed(t, ebw - 1, abw, store_val);
+            unsigned const k = bw - ebw;
+            auto const sc = cs.fixed(t, ebw - 1 + k, abw + k, store_val);
 #if DEBUG_EXPLAIN
-            verbose_stream() << "    t[" << (ebw - 1) << ":" << abw << "] = " << store_val << "\n";
+            verbose_stream() << "    t     " << t << "\n";
+            verbose_stream() << "    t[" << (ebw - 1 + k) << ":" << (abw + k) << "] = " << store_val << "\n";
             verbose_stream() << "    fixed prefix constraint " << sc << "\n";
             verbose_stream() << "        eval " << sc.eval() << "\n";
             verbose_stream() << "        weval " << sc.weak_eval(c.get_assignment()) << "\n";