From 65de39f403bdd36893c98319c31c56bb3348b41a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 5 Jan 2016 08:45:10 -0800
Subject: [PATCH 1/2] disabling mk_const_case_multiplier until debugged

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h | 9 +++++++--
 1 file changed, 7 insertions(+), 2 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 942f97e93..25bc72add 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
@@ -171,12 +171,14 @@ void bit_blaster_tpl<Cfg>::mk_multiplier(unsigned sz, expr * const * a_bits, exp
         return;
     }
     
+#if 1
     if (mk_const_multiplier(sz, a_bits, b_bits, out_bits)) {
         return;
     }
     if (mk_const_multiplier(sz, b_bits, a_bits, out_bits)) {
         return;
     }
+#endif
 
     if (!m_use_wtm) {
 #if 0
@@ -1217,6 +1219,7 @@ void bit_blaster_tpl<Cfg>::mk_const_case_multiplier(bool is_a, unsigned i, unsig
         n_a *= n_b;
         num2bits(n_a, sz, out_bits);
     }
+    SASSERT(out_bits.size() == sz);
 }
 
 template<typename Cfg>
@@ -1227,7 +1230,8 @@ bool bit_blaster_tpl<Cfg>::mk_const_multiplier(unsigned sz, expr * const * a_bit
     }
     SASSERT(out_bits.empty());
     
-    if (mk_const_case_multiplier(sz, a_bits, b_bits, out_bits)) {
+    if (false && mk_const_case_multiplier(sz, a_bits, b_bits, out_bits)) {
+        SASSERT(sz == out_bits.size());
         return true;
     }    
     if (!m_use_bcm) {
@@ -1239,7 +1243,7 @@ bool bit_blaster_tpl<Cfg>::mk_const_multiplier(unsigned sz, expr * const * a_bit
     out_bits.resize(sz, m().mk_false());
     
 #if 1
-    bool last=false, now;
+    bool last = false, now;
     for (unsigned i = 0; i < sz; i++) {
         now = m().is_true(a_bits[i]);
         SASSERT(now || m().is_false(a_bits[i]));
@@ -1311,5 +1315,6 @@ bool bit_blaster_tpl<Cfg>::mk_const_multiplier(unsigned sz, expr * const * a_bit
     TRACE("bit_blaster_tpl_booth", for (unsigned i=0; i<out_bits.size(); i++)
                                      tout << "Booth encoding: " << mk_pp(out_bits[i].get(), m()) << "\n"; );
 
+    SASSERT(out_bits.size() == sz);
     return true;
 }

From ee157e47e4752b241a22fb1637dfda047cf7df2d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 5 Jan 2016 09:19:21 -0800
Subject: [PATCH 2/2] fix crash caused by recycling variable names.
 Stackoverflow segfault-in-bv-rewritermk-mul-eq

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/bv_rewriter.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index c571a5c56..2f1fe3c90 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -2064,12 +2064,12 @@ br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) {
         }
     }
     if (m_util.is_numeral(lhs, c_val, sz) && is_add_mul_const(rhs)) {
-        unsigned sz = to_app(rhs)->get_num_args();
+        unsigned num_args = to_app(rhs)->get_num_args();
         unsigned i = 0;
         expr* c2, *x2;
         numeral c2_val, c2_inv_val;
         bool found = false;
-        for (; !found && i < sz; ++i) {
+        for (; !found && i < num_args; ++i) {
             expr* arg = to_app(rhs)->get_arg(i);
             if (m_util.is_bv_mul(arg, c2, x2) && m_util.is_numeral(c2, c2_val, sz) &&
                 m_util.mult_inverse(c2_val, sz, c2_inv_val)) {