mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

update progress

Browse source
This commit is contained in:
Jakob Rath 2023-11-29 13:31:36 +01:00
parent 179da49379
commit 5d3a5a94e8
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1732,7 +1732,9 @@ namespace polysat {
return l_false; // conflict return l_false; // conflict
// replace lower bits of 'val' by 'a' // replace lower bits of 'val' by 'a'
val = val + distance(lower_cover_lo, a, lower_mod_value); rational const dist = distance(lower_cover_lo, a, lower_mod_value);
val += dist;
progress += dist;
LOG("distance(val, cover_hi) = " << distance(val, to_cover_hi, mod_value)); LOG("distance(val, cover_hi) = " << distance(val, to_cover_hi, mod_value));
LOG("distance(next_val, cover_hi) = " << distance(next_val, to_cover_hi, mod_value)); LOG("distance(next_val, cover_hi) = " << distance(next_val, to_cover_hi, mod_value));
SASSERT(distance(val, to_cover_hi, mod_value) >= distance(next_val, to_cover_hi, mod_value)); SASSERT(distance(val, to_cover_hi, mod_value) >= distance(next_val, to_cover_hi, mod_value));