From 17131983fe945f8ebcdf2dfec6d02dcf5ee2f88e Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Tue, 2 Apr 2024 16:31:16 +0200
Subject: [PATCH] use loop instead of goto

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

diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp
index ddda463ba..de9cd6100 100644
--- a/src/sat/smt/polysat/viable.cpp
+++ b/src/sat/smt/polysat/viable.cpp
@@ -174,19 +174,16 @@ namespace polysat {
         // 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;
-                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;
+                while (entry* e = find_overlap(w, layer, val)) {
+                    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;
+                    }
                 }
-                goto again;
             }
         }
         return last;