mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 04:43:39 +00:00
Code Activity

check bits for next_val

Browse source
This commit is contained in:
Jakob Rath 2023-11-24 17:13:48 +01:00
parent 2a3c8d2b82
commit 3740e766f7
1 changed files with 8 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1628,6 +1628,14 @@ namespace polysat {
if (distance(val, n, mod_value) < distance(val, next_val, mod_value)) if (distance(val, n, mod_value) < distance(val, next_val, mod_value))
next_val = n; next_val = n;
} }
if (entry* e = refine_bits<false>(v, next_val, w, fbi)) {
refine_todo.push_back(e);
rational const& n = e->interval.lo_val();
SASSERT(distance(val, n, mod_value) < distance(val, next_val, mod_value));
next_val = n;
}
SASSERT(!refine_bits<true>(v, val, w, fbi));
SASSERT(val != next_val);
unsigned const lower_w = widths[w_idx - 1]; unsigned const lower_w = widths[w_idx - 1];
rational const lower_mod_value = rational::power_of_two(lower_w); rational const lower_mod_value = rational::power_of_two(lower_w);