From 762ade2a798e127a96f939eb08052853f7f8ff1c Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Fri, 15 Sep 2023 06:15:22 -0700
Subject: [PATCH] check m_unassigned_bounds in bound_is_interesting

---
 src/smt/theory_lra.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 1a022e087..d88d54a69 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2239,6 +2239,9 @@ public:
         if (v == null_theory_var) 
             return false;
 
+        if (m_unassigned_bounds[v] == 0) 
+            return false;
+
         if (should_refine_bounds()) 
             return true;