diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation1/Main.class b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation01-String/Main.class
similarity index 83%
rename from jbmc/regression/jbmc-strings/IndexOfConstantEvaluation1/Main.class
rename to jbmc/regression/jbmc-strings/IndexOfConstantEvaluation01-String/Main.class
index c77429885c0..5ddeaceabcd 100644
Binary files a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation1/Main.class and b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation01-String/Main.class differ
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation01-String/Main.java b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation01-String/Main.java
new file mode 100644
index 00000000000..5310a7c59e3
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation01-String/Main.java
@@ -0,0 +1,14 @@
+public class Main {
+
+  public void constantIndexOf() {
+    String s1 = "abcabc";
+    String s2 = "bc";
+    assert s1.indexOf(s2) == 1;
+    assert s1.indexOf(s2, -10) == 1;
+    assert s1.indexOf("") == 0;
+    assert s1.indexOf(s2, 3) == 4;
+    assert s1.indexOf("cd") == -1;
+    assert s1.indexOf(s2, 10) == -1;
+    assert s1.indexOf("", 10) == -1;
+  }
+}
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation01-String/test-models-library.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation01-String/test-models-library.desc
new file mode 100644
index 00000000000..6bccaef4ef9
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation01-String/test-models-library.desc
@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.constantIndexOf --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation1/test.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation01-String/test.desc
similarity index 100%
rename from jbmc/regression/jbmc-strings/IndexOfConstantEvaluation1/test.desc
rename to jbmc/regression/jbmc-strings/IndexOfConstantEvaluation01-String/test.desc
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation2/Main.class b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation02-char/Main.class
similarity index 79%
rename from jbmc/regression/jbmc-strings/IndexOfConstantEvaluation2/Main.class
rename to jbmc/regression/jbmc-strings/IndexOfConstantEvaluation02-char/Main.class
index 896933de6ff..43990372412 100644
Binary files a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation2/Main.class and b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation02-char/Main.class differ
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation02-char/Main.java b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation02-char/Main.java
new file mode 100644
index 00000000000..9cd8b92095c
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation02-char/Main.java
@@ -0,0 +1,11 @@
+public class Main {
+
+  public void constantIndexOf() {
+    String s1 = "abcabc";
+    assert s1.indexOf('b') == 1;
+    assert s1.indexOf('b', -10) == 1;
+    assert s1.indexOf('b', 3) == 4;
+    assert s1.indexOf('d') == -1;
+    assert s1.indexOf('b', 10) == -1;
+  }
+}
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation2/test.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation02-char/test.desc
similarity index 100%
rename from jbmc/regression/jbmc-strings/IndexOfConstantEvaluation2/test.desc
rename to jbmc/regression/jbmc-strings/IndexOfConstantEvaluation02-char/test.desc
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation3/Main.class b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation03-IndexOutOfRange/Main.class
similarity index 89%
rename from jbmc/regression/jbmc-strings/IndexOfConstantEvaluation3/Main.class
rename to jbmc/regression/jbmc-strings/IndexOfConstantEvaluation03-IndexOutOfRange/Main.class
index fed19bbf5b4..7095e9016ba 100644
Binary files a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation3/Main.class and b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation03-IndexOutOfRange/Main.class differ
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation03-IndexOutOfRange/Main.java b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation03-IndexOutOfRange/Main.java
new file mode 100644
index 00000000000..83cbaf8a928
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation03-IndexOutOfRange/Main.java
@@ -0,0 +1,7 @@
+public class Main {
+
+  public void constantIndexOf(String arg) {
+    String s1 = "abcabc";
+    assert s1.indexOf(arg, 10) == -1;
+  }
+}
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation3/test.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation03-IndexOutOfRange/test.desc
similarity index 100%
rename from jbmc/regression/jbmc-strings/IndexOfConstantEvaluation3/test.desc
rename to jbmc/regression/jbmc-strings/IndexOfConstantEvaluation03-IndexOutOfRange/test.desc
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/Main.class b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/Main.class
similarity index 79%
rename from jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/Main.class
rename to jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/Main.class
index 6400d17f6f7..99b39467ebc 100644
Binary files a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/Main.class and b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/Main.class differ
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/Main.java b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/Main.java
new file mode 100644
index 00000000000..e532e475034
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/Main.java
@@ -0,0 +1,24 @@
+public class Main {
+
+  public void constantIndexOf(String s, char c, int i) {
+
+    String s1 = "abcabc";
+    String s2 = "bc";
+
+    assert s1.indexOf(c) == 1;
+    assert s1.indexOf(s) == 1;
+    assert s1.indexOf(c, 1) == 1;
+    assert s1.indexOf(s, 1) == 1;
+
+    assert s.indexOf('a') == 1;
+    assert s.indexOf(s1) == 1;
+    assert s.indexOf('a', 1) == 1;
+    assert s.indexOf(s1, 1) == 1;
+
+    assert s1.indexOf(s, -10) == 1;
+    assert s1.indexOf(c, -10) == 1;
+
+    assert s1.indexOf(s2, i) == 1;
+    assert s1.indexOf('a', i) == 1;
+  }
+}
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test1.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test1.desc
similarity index 100%
rename from jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test1.desc
rename to jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test1.desc
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test10.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test10.desc
similarity index 100%
rename from jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test10.desc
rename to jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test10.desc
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test11.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test11.desc
similarity index 100%
rename from jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test11.desc
rename to jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test11.desc
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test12.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test12.desc
similarity index 100%
rename from jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test12.desc
rename to jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test12.desc
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test2.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test2.desc
similarity index 100%
rename from jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test2.desc
rename to jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test2.desc
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test3.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test3.desc
similarity index 100%
rename from jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test3.desc
rename to jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test3.desc
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test4.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test4.desc
similarity index 100%
rename from jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test4.desc
rename to jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test4.desc
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test5.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test5.desc
similarity index 100%
rename from jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test5.desc
rename to jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test5.desc
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test6.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test6.desc
similarity index 100%
rename from jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test6.desc
rename to jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test6.desc
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test7.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test7.desc
similarity index 100%
rename from jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test7.desc
rename to jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test7.desc
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test8.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test8.desc
similarity index 100%
rename from jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test8.desc
rename to jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test8.desc
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test9.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test9.desc
similarity index 100%
rename from jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test9.desc
rename to jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test9.desc
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation05-Character/Main.class b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation05-Character/Main.class
new file mode 100644
index 00000000000..7734ec2dd56
Binary files /dev/null and b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation05-Character/Main.class differ
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation05-Character/Main.java b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation05-Character/Main.java
new file mode 100644
index 00000000000..49ee0852a80
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation05-Character/Main.java
@@ -0,0 +1,11 @@
+public class Main {
+
+  public void constantIndexOf() {
+    String s1 = "abcabc";
+    Character b = 'b';
+    assert s1.indexOf(b) == 1;
+    assert s1.indexOf(b, -10) == 1;
+    assert s1.indexOf(b, 3) == 4;
+    assert s1.indexOf(b, 10) == -1;
+  }
+}
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation05-Character/test-models-library.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation05-Character/test-models-library.desc
new file mode 100644
index 00000000000..6bccaef4ef9
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation05-Character/test-models-library.desc
@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.constantIndexOf --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation06-AssertionFailure/Main.class b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation06-AssertionFailure/Main.class
new file mode 100644
index 00000000000..38845f9cd17
Binary files /dev/null and b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation06-AssertionFailure/Main.class differ
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation06-AssertionFailure/Main.java b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation06-AssertionFailure/Main.java
new file mode 100644
index 00000000000..e64b4b108e8
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation06-AssertionFailure/Main.java
@@ -0,0 +1,7 @@
+public class Main {
+
+  public void constantIndexOf() {
+    String s1 = "abcabc";
+    assert s1.indexOf("") == -1;
+  }
+}
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation06-AssertionFailure/test.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation06-AssertionFailure/test.desc
new file mode 100644
index 00000000000..9705cb829fb
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation06-AssertionFailure/test.desc
@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.constantIndexOf --property "java::Main.constantIndexOf:()V.assertion.1"
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation1/Main.java b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation1/Main.java
deleted file mode 100644
index 5d67144292d..00000000000
--- a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation1/Main.java
+++ /dev/null
@@ -1,13 +0,0 @@
-public class Main {
-    public void constantIndexOf() {
-        String s1 = "abcabc";
-        String s2 = "bc";
-        assert s1.indexOf(s2) == 1;
-        assert s1.indexOf(s2, -10) == 1;
-        assert s1.indexOf("") == 0;
-        assert s1.indexOf(s2, 3) == 4;
-        assert s1.indexOf("cd") == -1;
-        assert s1.indexOf(s2, 10) == -1;
-        assert s1.indexOf("", 10) == -1;
-    }
-}
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation2/Main.java b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation2/Main.java
deleted file mode 100644
index ef5449e91b2..00000000000
--- a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation2/Main.java
+++ /dev/null
@@ -1,10 +0,0 @@
-public class Main {
-    public void constantIndexOf() {
-        String s1 = "abcabc";
-        assert s1.indexOf('b') == 1;
-        assert s1.indexOf('b', -10) == 1;
-        assert s1.indexOf('b', 3) == 4;
-        assert s1.indexOf('d') == -1;
-        assert s1.indexOf('b', 10) == -1;
-    }
-}
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation3/Main.java b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation3/Main.java
deleted file mode 100644
index 953a9180bc8..00000000000
--- a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation3/Main.java
+++ /dev/null
@@ -1,6 +0,0 @@
-public class Main {
-    public void constantIndexOf(String arg) {
-        String s1 = "abcabc";
-        assert s1.indexOf(arg, 10) == -1;
-    }
-}
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/Main.java b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/Main.java
deleted file mode 100644
index f371e36713d..00000000000
--- a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/Main.java
+++ /dev/null
@@ -1,23 +0,0 @@
-public class Main {
-    public void constantIndexOf(String s, char c, int i) {
-
-        String s1 = "abcabc";
-        String s2 = "bc";
-
-        assert s1.indexOf(c) == 1;
-        assert s1.indexOf(s) == 1;
-        assert s1.indexOf(c, 1) == 1;
-        assert s1.indexOf(s, 1) == 1;
-
-        assert s.indexOf('a') == 1;
-        assert s.indexOf(s1) == 1;
-        assert s.indexOf('a', 1) == 1;
-        assert s.indexOf(s1, 1) == 1;
-
-        assert s1.indexOf(s, -10) == 1;
-        assert s1.indexOf(c, -10) == 1;
-
-        assert s1.indexOf(s2, i) == 1;
-        assert s1.indexOf('a', i) == 1;
-    }
-}