From 47f28c6857f8a29daf70a9a72a115d4a9b44c4ea Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Tue, 2 Apr 2024 16:27:29 +0200
Subject: [PATCH] find_overlap should stay on lower bit-width to find conflicts

---
 src/sat/smt/polysat/viable.cpp | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp
index c1e4dca0e..187c2b330 100644
--- a/src/sat/smt/polysat/viable.cpp
+++ b/src/sat/smt/polysat/viable.cpp
@@ -170,10 +170,11 @@ namespace polysat {
     // 
 
     viable::entry* viable::find_overlap(rational& val) {
-
         entry* last = nullptr;
+        // TODO: this doesn't always make sure we prefer smaller sizes... different suffixes would have to be interleaved.
         for (auto const& [w, offset] : m_overlaps) {
             for (auto& layer : m_units[w].get_layers()) {
+again:
                 entry* e = find_overlap(w, layer, val);
                 if (!e)
                     continue;
@@ -185,12 +186,13 @@ namespace polysat {
                     m_explain_kind = explain_t::conflict;
                     return nullptr;
                 }
+                goto again;
             }
         }
         return last;
     }
 
-    viable::entry* viable::find_overlap(pvar w, layer& l, rational const& val) {
+    viable::entry* viable::find_overlap(pvar /* w */, layer& l, rational const& val) {
         if (!l.entries)
             return nullptr;
         unsigned v_width = m_num_bits;