From 111dee91433936c3a31aa7abf5691ea2468ed580 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 1 Feb 2024 09:37:41 -0800 Subject: [PATCH] simplify overflow check up front Signed-off-by: Nikolaj Bjorner --- src/sat/smt/polysat/constraints.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/sat/smt/polysat/constraints.cpp b/src/sat/smt/polysat/constraints.cpp index 9d7e02c6f..73fe5d85d 100644 --- a/src/sat/smt/polysat/constraints.cpp +++ b/src/sat/smt/polysat/constraints.cpp @@ -33,7 +33,11 @@ namespace polysat { return is_positive ? sc : ~sc; } - signed_constraint constraints::umul_ovfl(pdd const& p, pdd const& q) { + 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);