diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp
index 1984581ee..f5e7cbaf9 100644
--- 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";