From 0a22f1e0f555324ab83b9a8f42946bceb87bcb6f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sun, 8 Feb 2015 18:07:10 +0000 Subject: [PATCH] array simplifier fix for a fix... Signed-off-by: Christoph M. Wintersteiger --- src/ast/simplifier/array_simplifier_plugin.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/simplifier/array_simplifier_plugin.cpp b/src/ast/simplifier/array_simplifier_plugin.cpp index 3f056df8e..c75766b25 100644 --- a/src/ast/simplifier/array_simplifier_plugin.cpp +++ b/src/ast/simplifier/array_simplifier_plugin.cpp @@ -413,7 +413,7 @@ bool array_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & resul 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)) { + if (arity1 == arity2 && 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) {