mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-03 22:43:56 +00:00
Code Activity

check for full intervals

Browse source
This commit is contained in:
Jakob Rath 2023-12-01 15:14:16 +01:00
parent a3bf994aa4
commit 7987ac4475
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/polysat/viable.cpp
View file

@ -1659,6 +1659,9 @@ namespace polysat {
if (!e) if (!e)
break; break;
if (e->interval.is_full())
return l_false;
SASSERT(e->interval.currently_contains(val)); SASSERT(e->interval.currently_contains(val));
rational const& new_val = e->interval.hi_val(); rational const& new_val = e->interval.hi_val();
rational const dist = distance(val, new_val, mod_value); rational const dist = distance(val, new_val, mod_value);