mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
check m_unassigned_bounds in bound_is_interesting
This commit is contained in:
parent
a55aa1a648
commit
762ade2a79
|
@ -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;
|
||||
|
||||
|
|
Loading…
Reference in a new issue