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;