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);