From 321c181fd8841615c6b2b6b96acef71ab5ff8811 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sun, 8 Feb 2015 18:04:23 +0000 Subject: [PATCH] Bugfix for array_simplifier_plugin. Thanks to codeplex user mtappler for reporting this. Signed-off-by: Christoph M. Wintersteiger --- src/ast/simplifier/array_simplifier_plugin.cpp | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/ast/simplifier/array_simplifier_plugin.cpp b/src/ast/simplifier/array_simplifier_plugin.cpp index 065f8bd96..3f056df8e 100644 --- a/src/ast/simplifier/array_simplifier_plugin.cpp +++ b/src/ast/simplifier/array_simplifier_plugin.cpp @@ -409,14 +409,15 @@ bool array_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & resul set_reduce_invoked(); expr* c1, *c2; ptr_vector st1, st2; - unsigned arity = 0; - get_stores(lhs, arity, c1, st1); - get_stores(rhs, arity, c2, st2); - if (is_const_array(c1) && is_const_array(c2)) { + unsigned arity1 = 0; + unsigned arity2 = 0; + get_stores(lhs, arity1, c1, st1); + get_stores(rhs, arity2, c2, st2); + if (arity1 == arity1 && is_const_array(c1) && is_const_array(c2)) { c1 = to_app(c1)->get_arg(0); c2 = to_app(c2)->get_arg(0); if (c1 == c2) { - lbool eq = eq_stores(c1, arity, st1.size(), st1.c_ptr(), st2.size(), st2.c_ptr()); + lbool eq = eq_stores(c1, arity2, st1.size(), st1.c_ptr(), st2.size(), st2.c_ptr()); TRACE("array_simplifier", tout << mk_pp(lhs, m_manager) << " = " << mk_pp(rhs, m_manager) << " := " << eq << "\n";);