From 5e81c1220c959fe74f5b4af7ab7b340b4a9d1845 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Jan 2022 12:48:15 -0800 Subject: [PATCH] #5797 probably still wrong wrt underflow. --- src/ast/rewriter/bv_rewriter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index f1b0afd45..4d15011d6 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -2829,7 +2829,7 @@ br_status bv_rewriter::mk_bvsmul_no_overflow(unsigned num, expr * const * args, bool sign1 = m_util.has_sign_bit(a1_val, bv_sz); if (sign0) a0_val = rational::power_of_two(bv_sz) - a0_val; if (sign1) a1_val = rational::power_of_two(bv_sz) - a1_val; - rational lim = rational::power_of_two(bv_sz); + rational lim = rational::power_of_two(bv_sz-1); rational r = a0_val * a1_val; result = m().mk_bool_val((sign0 != sign1) || r < lim); return BR_DONE;