Fix bug with lastIndexOf TG-592

regression/jbmc-strings/VerifStringLastIndexOf/Test.java

@@ -0,0 +1,27 @@
+public class Test {
+  // This compares the model of indexOf to an implementation
+  // using loops
+
+  public int math_min(int i, int j) {
+    if (i < j)
+      return i;
+    else
+      return j;
+  }
+
+  public int referenceLastIndexOf(String s, char ch, int fromIndex) {
+    for (int i = math_min(fromIndex, s.length() - 1); i >= 0; i--) {
+      if (s.charAt(i) == ch) {
+        return i;
+      }
+    }
+    return -1;
+  }
+
+  public int check(String s, char ch, int fromIndex) {
+    int reference = referenceLastIndexOf(s, ch, fromIndex);
+    int jbmc_result = s.lastIndexOf(ch, fromIndex);
+    assert(reference == jbmc_result);
+    return jbmc_result;
+  }
+}

regression/jbmc-strings/VerifStringLastIndexOf/test.desc

@@ -0,0 +1,7 @@
+THOROUGH
+Test.class
+--function Test.check --refine-strings --string-max-length 50 --unwind 50 --java-assume-inputs-non-null
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 32 .* SUCCESS$
+assertion at file Test.java line 34 .* FAILURE$

src/solvers/refinement/string_constraint_generator_indexof.cpp

@@ -348,7 +348,8 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of(
   axioms.push_back(a3);
 
   const exprt index1 = from_integer(1, index_type);
-  const plus_exprt from_index_plus_one(from_index, index1);
+  const exprt from_index_plus_one =
+    plus_exprt_with_overflow_check(from_index, index1);
   const if_exprt end_index(
     binary_relation_exprt(from_index_plus_one, ID_le, str.length()),
     from_index_plus_one,