mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

reset out_bits when blasting multiplication of bit-vectors

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-01-05 10:07:44 -08:00
parent ee157e47e4
commit 9dfcaaa01d
1 changed files with 7 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
View file

@ -163,23 +163,25 @@ void bit_blaster_tpl<Cfg>::mk_multiplier(unsigned sz, expr * const * a_bits, exp
std::swap(a_bits, b_bits); std::swap(a_bits, b_bits);
if (is_minus_one(sz, b_bits)) { if (is_minus_one(sz, b_bits)) {
mk_neg(sz, a_bits, out_bits); mk_neg(sz, a_bits, out_bits);
SASSERT(sz == out_bits.size());
return; return;
} }
if (is_numeral(sz, a_bits, n_a)) { if (is_numeral(sz, a_bits, n_a)) {
n_a *= n_b; n_a *= n_b;
num2bits(n_a, sz, out_bits); num2bits(n_a, sz, out_bits);
SASSERT(sz == out_bits.size());
return; return;
} }
#if 1
if (mk_const_multiplier(sz, a_bits, b_bits, out_bits)) { if (mk_const_multiplier(sz, a_bits, b_bits, out_bits)) {
SASSERT(sz == out_bits.size());
return; return;
} }
if (mk_const_multiplier(sz, b_bits, a_bits, out_bits)) { if (mk_const_multiplier(sz, b_bits, a_bits, out_bits)) {
SASSERT(sz == out_bits.size());
return; return;
} }
#endif out_bits.reset();
if (!m_use_wtm) { if (!m_use_wtm) {
#if 0 #if 0
static unsigned counter = 0; static unsigned counter = 0;
@ -1230,10 +1232,11 @@ bool bit_blaster_tpl<Cfg>::mk_const_multiplier(unsigned sz, expr * const * a_bit
} }
SASSERT(out_bits.empty()); SASSERT(out_bits.empty());
if (false && mk_const_case_multiplier(sz, a_bits, b_bits, out_bits)) { if (mk_const_case_multiplier(sz, a_bits, b_bits, out_bits)) {
SASSERT(sz == out_bits.size()); SASSERT(sz == out_bits.size());
return true; return true;
} }
out_bits.reset();
if (!m_use_bcm) { if (!m_use_bcm) {
return false; return false;
} }