mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-03 11:25:40 +00:00
Code Activity

fix

Browse source
This commit is contained in:
Jakob Rath 2021-09-09 11:00:01 +02:00
parent ec882d10da
commit 6e9e8999dc
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/explain.cpp
View file

@ -33,7 +33,7 @@ namespace polysat {
return {}; return {};
// Only keep result if the degree in c2 was reduced. // Only keep result if the degree in c2 was reduced.
// (this condition might be too strict, but we use it for now to prevent looping) // (this condition might be too strict, but we use it for now to prevent looping)
if (b.degree(v) >= r.degree(v)) if (b.degree(v) <= r.degree(v))
return {}; return {};
unsigned const lvl = std::max(c1->level(), c2->level()); unsigned const lvl = std::max(c1->level(), c2->level());
signed_constraint c = cm().eq(lvl, r); signed_constraint c = cm().eq(lvl, r);