From d1ef8029a934a5699201895bbdb996707e16b57e Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Thu, 19 Jan 2023 13:43:50 +0100
Subject: [PATCH] simpler condition

---
 src/math/polysat/viable.cpp | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index 62458db29..907d1250d 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -910,9 +910,8 @@ namespace {
                 entry const* n1 = n->next();
                 if (n1 == e)
                     break;
-                if (!e->interval.currently_contains(n1->interval.lo_val()))
-                    if (e->interval.hi_val() != n1->interval.lo_val())
-                        break;
+                if (!n1->interval.currently_contains(e->interval.hi_val()))
+                    break;
                 n = n1;
             }
             // display_one(verbose_stream() << "e is ", v, e) << "\n";
@@ -1278,9 +1277,8 @@ namespace {
                 //      n1:        [----[
                 if (n1 == e)
                     break;
-                if (!e->interval.currently_contains(n1->interval.lo_val()))
-                    if (e->interval.hi_val() != n1->interval.lo_val())
-                        break;
+                if (!n1->interval.currently_contains(e->interval.hi_val()))
+                    break;
                 n = n1;
             }