From 7987ac447543170ac65345265b72950bfaa87b17 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Fri, 1 Dec 2023 15:14:16 +0100
Subject: [PATCH] check for full intervals

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

diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index 2de8315bf..5aad7100f 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -1659,6 +1659,9 @@ namespace polysat {
                 if (!e)
                     break;
 
+                if (e->interval.is_full())
+                    return l_false;
+
                 SASSERT(e->interval.currently_contains(val));
                 rational const& new_val = e->interval.hi_val();
                 rational const dist = distance(val, new_val, mod_value);