Disable string indices assertion

This checked that no universally-quantified expression referred to the same string with
two different indices, but this is definitely possible (and always has been, e.g. the
StartsWith regression test asks for s.startsWtih(s, 1), which essentially asks if s is
its own prefix, and produces the expression "forall x, s[x] == s[x+1]".

The previous commit's improvement to pointer tracking means symex now exposes that situation
more directly, but it would always have happened in reality, just not getting caught by this
assertion.

Author: smowton

src/solvers/refinement/string_refinement.cpp

@@ -2152,6 +2152,13 @@ static bool is_valid_string_constraint(
   {
     // Condition 1: All indices of the same string must be the of the same form
     const exprt rep=pair.second.back();
+
+    // This test is disabled because Java like "s.startsWith(s, 1)" produces
+    // a constraint like "forall x, s[x] == s[x+1]", which does not meet this
+    // constraint as s is indexed with both 'x' and 'x+1' under the same
+    // universal quantifier. We should either indirect to avoid the double
+    // reference, or establish that this conditon wasn't needed to begin with.
+    /*
     for(size_t j=0; j<pair.second.size()-1; j++)
     {
       const exprt i=pair.second[j];
@@ -2164,6 +2171,7 @@ static bool is_valid_string_constraint(
         return false;
       }
     }
+    */
 
     // Condition 2: f must be linear in the quantified variable
     if(!is_linear_arithmetic_expr(rep, constraint.univ_var))