mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

relax eq_resolve conditions

Browse source 
fixes Example 1
This commit is contained in:
Jakob Rath 2024-05-06 15:24:00 +02:00
parent 0a8879b505
commit 7925ef731f
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/sat/smt/polysat/saturation.cpp
View file

@ -316,6 +316,8 @@ namespace polysat {
SASSERT(i.rhs().is_zero() && j.rhs().is_zero() && !i.is_strict() && !j.is_strict());
pdd a = i.lhs();
pdd b = j.lhs();
if (a == b)
return;
unsigned degree_a = a.degree();
unsigned degree_b = b.degree();
pdd r = a;
@ -326,9 +328,9 @@ namespace polysat {
return;
// 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)
if (b.degree(v) <= r.degree(v))
if (b.degree(v) < r.degree(v))
return;
if (a.degree(v) <= r.degree(v))
if (a.degree(v) < r.degree(v))
return;
add_clause("ax + b = 0 & cx + d = 0 ==> cb - da = 0", { i.dep(), j.dep(), C.eq(r) }, true);