From 811843cf4508e60afc83c9308c0b7c0bab3878fe Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 3 Oct 2022 15:22:00 +0200
Subject: [PATCH] Fix interval check

---
 src/math/polysat/viable.cpp | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index 7be0fa72b..78e52f020 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -644,7 +644,6 @@ namespace polysat {
             // using the equivalence:  t \in [l;h[  <=>  t-l < h-l
             entry* n = e->next();
 
-#if 0
             // Choose the next interval which furthest extends the covered region.
             // Example:
             //      covered:   [-------]
@@ -668,11 +667,21 @@ namespace polysat {
             // The interval 'first' is always part of the lemma. If we reach first again here, we have covered the complete domain.
             while (n != first) {
                 entry* n1 = n->next();
-                if (!e->interval.currently_contains(n1->interval.lo_val()))
+                // Check if n1 is eligible; if yes, then n1 is better than n.
+                //
+                // Case 1, n1 overlaps e (unless n1 == e):
+                //      e:  [------[
+                //      n1:      [----[
+                // Case 2, n1 connects to e:
+                //      e:  [------[
+                //      n1:        [----[
+                if (n1 == e)
                     break;
+                if (!e->interval.currently_contains(n1->interval.lo_val()))
+                    if (e->interval.hi_val() != n1->interval.lo_val())
+                        break;
                 n = n1;
             }
-#endif
 
             if (!e->interval.is_full()) {
                 auto const& hi = e->interval.hi();