From aeb6138c258d47af0618c6af0c0e8f3705236e37 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Thu, 5 Jan 2023 17:21:25 +0100
Subject: [PATCH] No result if there is no other interval

---
 src/math/polysat/viable.cpp | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index e88db7d27..96b468d10 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -755,6 +755,11 @@ namespace polysat {
                         break;
                 n = n1;
             }
+            if (e == n) {
+                SASSERT_EQ(e, e0);
+                // VERIFY(false);
+                return false;
+            }
 
             if (e == e0) {
                 out_lo = n->interval.lo_val();