From b808dece1529bf4635f4dc2545b80178b22bc3a6 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 3 Apr 2024 17:38:43 +0200
Subject: [PATCH] always restart find_overlap at smallest size

---
 src/sat/smt/polysat/viable.cpp | 21 +++++++++++++--------
 1 file changed, 13 insertions(+), 8 deletions(-)

diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp
index c71e827d1..c3a596f93 100644
--- a/src/sat/smt/polysat/viable.cpp
+++ b/src/sat/smt/polysat/viable.cpp
@@ -172,18 +172,23 @@ 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.
+next:
         for (auto const& [w, offset] : m_suffixes) {
             for (auto& layer : m_units[w].get_layers()) {
-                while (entry* e = find_overlap(w, layer, val)) {
-                    last = e;
-                    if (e->interval.is_proper())
+                entry* e = find_overlap(w, layer, val);
+                if (!e)
+                    continue;
+                last = e;
+                if (e->interval.is_proper())
                     update_value_to_high(val, e);
-                    m_explain.push_back({ e, val });
-                    if (is_conflict()) {
-                        m_explain_kind = explain_t::conflict;
-                        return nullptr;
-                    }
+                // display_explain(verbose_stream() << "found: ", {e,val}) << "\n";
+                m_explain.push_back({ e, val });
+                if (is_conflict()) {
+                    verbose_stream() << "find_overlap conflict\n";
+                    m_explain_kind = explain_t::conflict;
+                    return nullptr;
                 }
+                goto next;
             }
         }
         return last;