mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

array simplifier fix for a fix...

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2015-02-08 18:07:10 +00:00
parent 321c181fd8
commit 0a22f1e0f5
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/simplifier/array_simplifier_plugin.cpp
View file

@ -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) {