From fafdbfaf0ec0e1bbf59d47526f7e8cffd833b4b4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 5 Jan 2016 10:16:02 -0800
Subject: [PATCH] reset out_bits when blasting multiplication of bit-vectors

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h | 1 +
 1 file changed, 1 insertion(+)

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<typename Cfg>
 void bit_blaster_tpl<Cfg>::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)) {