Avoid generating redundant constraints by iterating over n^2/2 rather than n^2 pairs.

Ackermann constaints are symmetric so we don't need to consider every pair of indexes,
only every ordered pair.  This can halve the number of constraints generated which can
be a significant saving in terms of problem size but also saves significant time when
used in the string solver.

Author: martin

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)