diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp
index 854ca4156b1..8a1fcfc328c 100644
--- a/src/solvers/flattening/arrays.cpp
+++ b/src/solvers/flattening/arrays.cpp
@@ -316,7 +316,7 @@ void arrayst::add_array_Ackermann_constraints()
         i1!=index_set.end();
         i1++)
       for(index_sett::const_iterator
-          i2=index_set.begin();
+          i2=i1;
           i2!=index_set.end();
           i2++)
         if(i1!=i2)
@@ -348,7 +348,7 @@ void arrayst::add_array_Ackermann_constraints()
 
             // add constraint
             lazy_constraintt lazy(lazy_typet::ARRAY_ACKERMANN,
-              or_exprt(literal_exprt(!indices_equal_lit), values_equal));
+              implies_exprt(literal_exprt(indices_equal_lit), values_equal));
             add_array_constraint(lazy, true); // added lazily
 
 #if 0 // old code for adding, not significantly faster