mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

Fix is_infty_level to treat 2^16-1 as infinity

Browse source
This commit is contained in:
Arie Gurfinkel 2018-09-04 21:48:07 -04:00
parent 5d2f682f7a
commit f67346d16e
2 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/muz/spacer/spacer_prop_solver.cpp
View file

@ -94,6 +94,7 @@ void prop_solver::add_level()
void prop_solver::ensure_level(unsigned lvl)
{
if (is_infty_level(lvl)) return;
while (lvl >= level_cnt()) {
add_level();
}

3
src/muz/spacer/spacer_util.h
View file

@ -48,7 +48,8 @@ namespace spacer {
}
inline bool is_infty_level(unsigned lvl) {
return lvl == infty_level ();
// XXX: level is 16 bits in class pob
return lvl >= 65535;
}
inline unsigned next_level(unsigned lvl) {