From 913b90f7aac8a585a40a0c74d7837be8dc2cb807 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 30 Jan 2022 10:42:34 -0800 Subject: [PATCH] fix #5802 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bv_rewriter.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 2c0d6abfb..d7ba4d604 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -2828,7 +2828,10 @@ br_status bv_rewriter::mk_bvsmul_no_overflow(unsigned num, expr * const * args, if (sign1) a1_val = rational::power_of_two(bv_sz) - a1_val; rational lim = rational::power_of_two(bv_sz-1); rational r = a0_val * a1_val; - result = m().mk_bool_val((is_overflow == (sign0 != sign1)) || r < lim); + if (is_overflow) + result = m().mk_bool_val(sign0 != sign1 || r < lim); + else + result = m().mk_bool_val(sign0 == sign1 || r <= lim); return BR_DONE; }