mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-31 08:23:17 +00:00
Code Activity

fix

Browse source
This commit is contained in:
Jakob Rath 2023-11-29 13:23:51 +01:00
parent 0b98a76177
commit 179da49379
1 changed files with 1 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1732,7 +1732,7 @@ 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 - lower_cover_lo + a; val = val + distance(lower_cover_lo, a, lower_mod_value);
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));
@ -1743,9 +1743,6 @@ namespace polysat {
SASSERT(result == l_undef); SASSERT(result == l_undef);
// TODO: continue with intervals at current level // TODO: continue with intervals at current level
// TODO: refinement and fallback solver -- can we refine without throwing out all the entry_cursors we have set up?
// we only have to chase intervals from the beginning if ec.cur has become inactive
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
return l_undef; return l_undef;
} }