From ee157e47e4752b241a22fb1637dfda047cf7df2d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 Jan 2016 09:19:21 -0800 Subject: [PATCH] fix crash caused by recycling variable names. Stackoverflow segfault-in-bv-rewritermk-mul-eq Signed-off-by: Nikolaj Bjorner --- 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)) {