From 5352a0106dfc8a432f1835fc241523879d8cd9d5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 26 Oct 2022 12:20:55 -0700
Subject: [PATCH] fix #6426
---
src/ast/rewriter/bv_rewriter.cpp | 6 ++++--
1 file changed, 4 insertions(+), 2 deletions(-)
diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index 4740a954c..b677b2197 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -2270,11 +2270,13 @@ br_status bv_rewriter::mk_bv_mul(unsigned num_args, expr * const * args, expr_re
// ~x = -1 - x
unsigned sz = m_util.get_bv_size(x);
if (m_util.is_bv_not(x, z)) {
- result = m_util.mk_bv_mul(m_util.mk_bv_sub(mk_numeral(-1, sz), z), y);
+ numeral p = rational(2).expt(sz) - 1;
+ result = m_util.mk_bv_mul(m_util.mk_bv_sub(mk_numeral(p, sz), z), y);
return BR_REWRITE3;
}
if (m_util.is_bv_not(y, z)) {
- result = m_util.mk_bv_mul(m_util.mk_bv_sub(mk_numeral(-1, sz), z), x);
+ numeral p = rational(2).expt(sz) - 1;
+ result = m_util.mk_bv_mul(m_util.mk_bv_sub(mk_numeral(p, sz), z), x);
return BR_REWRITE3;
}
// shl(z, u) * x = shl(x * z, u)