diff --git a/regression/jbmc-strings/StringIndexOf/Test.class b/regression/jbmc-strings/StringIndexOf/Test.class
index 73660394203..095327fb14f 100644
Binary files a/regression/jbmc-strings/StringIndexOf/Test.class and b/regression/jbmc-strings/StringIndexOf/Test.class differ
diff --git a/regression/jbmc-strings/StringIndexOf/Test.java b/regression/jbmc-strings/StringIndexOf/Test.java
index 6732eba723a..87f3d1ee3c8 100644
--- a/regression/jbmc-strings/StringIndexOf/Test.java
+++ b/regression/jbmc-strings/StringIndexOf/Test.java
@@ -1,3 +1,6 @@
+// This test uses CProverString so should be compiled with
+// javac Test.java ../cprover/CProverString.java
+
 public class Test {
 
     public boolean check(String input_String, char input_char, int input_int) {
@@ -14,13 +17,13 @@ public boolean check(String input_String, char input_char, int input_int) {
 
         if (i == -1) {
             for (int j = lower_bound; j < input_String.length(); j++)
-                assert input_String.charAt(j) != input_char;
+                assert org.cprover.CProverString.charAt(input_String, j) != input_char;
         } else {
             assert i >= lower_bound;
-            assert input_String.charAt(i) == input_char;
+            assert org.cprover.CProverString.charAt(input_String, i) == input_char;
 
             for (int j = lower_bound; j < i; j++)
-                assert input_String.charAt(j) != input_char;
+                assert org.cprover.CProverString.charAt(input_String, j) != input_char;
         }
         return true;
     }
diff --git a/regression/jbmc-strings/StringIndexOf/test.desc b/regression/jbmc-strings/StringIndexOf/test.desc
index 9c17878eb94..8b52eaea4dd 100644
--- a/regression/jbmc-strings/StringIndexOf/test.desc
+++ b/regression/jbmc-strings/StringIndexOf/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---refine-strings --function Test.check --unwind 4 --string-max-length 3 --java-assume-inputs-non-null
+--refine-strings --function Test.check --unwind 4 --string-max-input-length 3 --java-assume-inputs-non-null
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/jbmc-strings/StringIndexOf/test2.desc b/regression/jbmc-strings/StringIndexOf/test2.desc
index 6fdbcd101f0..3bb7fe6b973 100644
--- a/regression/jbmc-strings/StringIndexOf/test2.desc
+++ b/regression/jbmc-strings/StringIndexOf/test2.desc
@@ -3,12 +3,12 @@ Test.class
 --refine-strings --function Test.check2 --unwind 10 --string-max-length 10 --java-assume-inputs-non-null
 ^EXIT=10$
 ^SIGNAL=0$
-assertion at file Test.java line 32 .* SUCCESS
-assertion at file Test.java line 34 .* SUCCESS
-assertion at file Test.java line 36 .* SUCCESS
-assertion at file Test.java line 38 .* SUCCESS
-assertion at file Test.java line 40 .* SUCCESS
-assertion at file Test.java line 42 .* SUCCESS
-assertion at file Test.java line 43 .* FAILURE
+assertion at file Test.java line 35 .* SUCCESS
+assertion at file Test.java line 37 .* SUCCESS
+assertion at file Test.java line 39 .* SUCCESS
+assertion at file Test.java line 41 .* SUCCESS
+assertion at file Test.java line 43 .* SUCCESS
+assertion at file Test.java line 45 .* SUCCESS
+assertion at file Test.java line 46 .* FAILURE
 ^VERIFICATION FAILED$
 --