mirror of
https://github.com/Z3Prover/z3
synced 2025-04-13 12:28:44 +00:00
fix #4868
This commit is contained in:
parent
6c9bdc949e
commit
982da8db05
|
@ -171,7 +171,6 @@ namespace sat {
|
||||||
for (unsigned i = 0; i < sz; ++i) {
|
for (unsigned i = 0; i < sz; ++i) {
|
||||||
watch_list& wlist = s.get_wlist(~l);
|
watch_list& wlist = s.get_wlist(~l);
|
||||||
watched & w = wlist[i];
|
watched & w = wlist[i];
|
||||||
sz = wlist.size();
|
|
||||||
if (!w.is_binary_clause())
|
if (!w.is_binary_clause())
|
||||||
continue;
|
continue;
|
||||||
literal l2 = w.get_literal();
|
literal l2 = w.get_literal();
|
||||||
|
@ -185,6 +184,7 @@ namespace sat {
|
||||||
return;
|
return;
|
||||||
if (s.inconsistent())
|
if (s.inconsistent())
|
||||||
return;
|
return;
|
||||||
|
sz = wlist.size();
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in a new issue