Merge pull request diffblue#1465 from mgudemann/feature/string-solver-performance

Feature/string solver performance

Author: Matthias Güdemann

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