From 9dfcaaa01dbfd3892400bc6831539d589fcd99c1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 Jan 2016 10:07:44 -0800 Subject: [PATCH] reset out_bits when blasting multiplication of bit-vectors Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h index 25bc72add..c0e8476fe 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -163,23 +163,25 @@ void bit_blaster_tpl::mk_multiplier(unsigned sz, expr * const * a_bits, exp std::swap(a_bits, b_bits); if (is_minus_one(sz, b_bits)) { mk_neg(sz, a_bits, out_bits); + SASSERT(sz == out_bits.size()); return; } if (is_numeral(sz, a_bits, n_a)) { n_a *= n_b; num2bits(n_a, sz, out_bits); + SASSERT(sz == out_bits.size()); return; } -#if 1 if (mk_const_multiplier(sz, a_bits, b_bits, out_bits)) { + SASSERT(sz == out_bits.size()); return; } if (mk_const_multiplier(sz, b_bits, a_bits, out_bits)) { + SASSERT(sz == out_bits.size()); return; } -#endif - + out_bits.reset(); if (!m_use_wtm) { #if 0 static unsigned counter = 0; @@ -1230,10 +1232,11 @@ bool bit_blaster_tpl::mk_const_multiplier(unsigned sz, expr * const * a_bit } 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()); return true; } + out_bits.reset(); if (!m_use_bcm) { return false; }