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 c0e8476fe..102082cd5 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -159,6 +159,7 @@ template void bit_blaster_tpl::mk_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) { SASSERT(sz > 0); numeral n_a, n_b; + out_bits.reset(); if (is_numeral(sz, a_bits, n_b)) std::swap(a_bits, b_bits); if (is_minus_one(sz, b_bits)) {