From 32e23b3b6cddc233dddbd5201a6ec9d22693a986 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 1 Feb 2024 12:39:37 -0800 Subject: [PATCH] remove unsound simplification Signed-off-by: Nikolaj Bjorner --- src/sat/smt/polysat/constraints.cpp | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/sat/smt/polysat/constraints.cpp b/src/sat/smt/polysat/constraints.cpp index 73fe5d85d..8c1e3f703 100644 --- a/src/sat/smt/polysat/constraints.cpp +++ b/src/sat/smt/polysat/constraints.cpp @@ -34,10 +34,6 @@ namespace polysat { } signed_constraint constraints::umul_ovfl(pdd const& p, pdd const& q) { - if (p == q) { - unsigned N = p.manager().power_of_2(); - return ule(rational::power_of_two(N - 1), p); - } auto* cnstr = alloc(umul_ovfl_constraint, p, q); c.trail().push(new_obj_trail(cnstr)); return signed_constraint(ckind_t::umul_ovfl_t, cnstr);