From 3740e766f7b78f4d2042c6c1fed19d0046e5c144 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Fri, 24 Nov 2023 17:13:48 +0100
Subject: [PATCH] check bits for next_val

---
 src/math/polysat/viable.cpp | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index bb1ee238c..fb57e3d22 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -1628,6 +1628,14 @@ namespace polysat {
             if (distance(val, n, mod_value) < distance(val, next_val, mod_value))
                 next_val = n;
         }
+        if (entry* e = refine_bits<false>(v, next_val, w, fbi)) {
+            refine_todo.push_back(e);
+            rational const& n = e->interval.lo_val();
+            SASSERT(distance(val, n, mod_value) < distance(val, next_val, mod_value));
+            next_val = n;
+        }
+        SASSERT(!refine_bits<true>(v, val, w, fbi));
+        SASSERT(val != next_val);
 
         unsigned const lower_w = widths[w_idx - 1];
         rational const lower_mod_value = rational::power_of_two(lower_w);