From e8163b1769f6fd7578b066fa257205a6bc868f6a Mon Sep 17 00:00:00 2001 From: Clemens Eisenhofer Date: Fri, 27 Jan 2023 08:32:44 +0100 Subject: [PATCH] Removed wrong assertion --- src/math/polysat/op_constraint.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/math/polysat/op_constraint.cpp b/src/math/polysat/op_constraint.cpp index 7f5ebd86c..b8b5384fc 100644 --- a/src/math/polysat/op_constraint.cpp +++ b/src/math/polysat/op_constraint.cpp @@ -662,8 +662,6 @@ namespace polysat { rational prodv = (pv * rv).val(); if (prodv != rational::power_of_two(parity_pv)) verbose_stream() << prodv << " " << rational::power_of_two(parity_pv) << " " << parity_pv << " " << pv << " " << rv << "\n"; - SASSERT(prodv != rational::power_of_two(parity_pv)); // Why did it evaluate to false in this case? - VERIFY(prodv != rational::power_of_two(parity_pv)); // Why did it evaluate to false in this case? unsigned lower = 0, upper = m.power_of_2(); // binary search for the parity (otw. we would have justifications like "parity_at_most(k) && parity_at_least(k)" for at most "k" widths while (lower + 1 < upper) { @@ -688,6 +686,7 @@ namespace polysat { if (rv.val() > max_rv) return s.mk_clause(~invc, s.parity_at_least(p(), middle), s.ule(r(), max_rv), false); } + // Why did it evaluate to false in this case? UNREACHABLE(); return {}; }