From 7925ef731fb6f181c843695cd80609a0d464d321 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 6 May 2024 15:24:00 +0200 Subject: [PATCH] relax eq_resolve conditions fixes Example 1 --- src/sat/smt/polysat/saturation.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/polysat/saturation.cpp b/src/sat/smt/polysat/saturation.cpp index eaea9c04d..6b28c5e60 100644 --- a/src/sat/smt/polysat/saturation.cpp +++ b/src/sat/smt/polysat/saturation.cpp @@ -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);