mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix #6426

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-10-26 12:20:55 -07:00
parent 2258b9b9b6
commit 5352a0106d
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/ast/rewriter/bv_rewriter.cpp
View file

@ -2270,11 +2270,13 @@ br_status bv_rewriter::mk_bv_mul(unsigned num_args, expr * const * args, expr_re
// ~x = -1 - x // ~x = -1 - x
unsigned sz = m_util.get_bv_size(x); unsigned sz = m_util.get_bv_size(x);
if (m_util.is_bv_not(x, z)) { 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; return BR_REWRITE3;
} }
if (m_util.is_bv_not(y, z)) { 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; return BR_REWRITE3;
} }
// shl(z, u) * x = shl(x * z, u) // shl(z, u) * x = shl(x * z, u)