From e4cc6e29ca8af5ae71f7a0c48799e80050b9a553 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 15 Mar 2024 08:55:07 -0700
Subject: [PATCH] fix case when interval is full

---
 src/sat/smt/polysat/viable.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp
index b21a203a2..cd309fa8f 100644
--- a/src/sat/smt/polysat/viable.cpp
+++ b/src/sat/smt/polysat/viable.cpp
@@ -174,7 +174,8 @@ namespace polysat {
                 if (!e)
                     continue;
                 last = e;
-                update_value_to_high(val, 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;