diff --git a/jbmc/lib/java-models-library b/jbmc/lib/java-models-library
index 766ac7a2c87..d92026cd8dd 160000
--- a/jbmc/lib/java-models-library
+++ b/jbmc/lib/java-models-library
@@ -1 +1 @@
-Subproject commit 766ac7a2c87dadfc7286ea0aab0a6eabdf3e4cdc
+Subproject commit d92026cd8dd8f1e769f5b11831e831fefdc4c080
diff --git a/jbmc/regression/jbmc-strings/StringBuilderChars04/test.desc b/jbmc/regression/jbmc-strings/StringBuilderChars04/test.desc
index 0923359deef..8df4c46ffc9 100644
--- a/jbmc/regression/jbmc-strings/StringBuilderChars04/test.desc
+++ b/jbmc/regression/jbmc-strings/StringBuilderChars04/test.desc
@@ -1,6 +1,6 @@
-FUTURE
+CORE
 StringBuilderChars04.class
---max-nondet-string-length 1000 --unwind 100
+--max-nondet-string-length 1000 --unwind 100 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/jbmc/regression/jbmc-strings/StringMiscellaneous01/test.desc b/jbmc/regression/jbmc-strings/StringMiscellaneous01/test.desc
index b6fc0921c0c..5166387582c 100644
--- a/jbmc/regression/jbmc-strings/StringMiscellaneous01/test.desc
+++ b/jbmc/regression/jbmc-strings/StringMiscellaneous01/test.desc
@@ -1,6 +1,6 @@
-FUTURE
+CORE
 StringMiscellaneous01.class
---max-nondet-string-length 1000 --unwind 30
+--max-nondet-string-length 1000 --unwind 30 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-strings/TokenTest01/test.desc b/jbmc/regression/jbmc-strings/TokenTest01/test.desc
index 2de78f35997..210c573d3f0 100644
--- a/jbmc/regression/jbmc-strings/TokenTest01/test.desc
+++ b/jbmc/regression/jbmc-strings/TokenTest01/test.desc
@@ -1,6 +1,6 @@
-FUTURE
+CORE
 TokenTest01.class
---max-nondet-string-length 1000 --unwind 30
+--max-nondet-string-length 1000 --unwind 6  --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-strings/TokenTest02/test.desc b/jbmc/regression/jbmc-strings/TokenTest02/test.desc
index b065ddf0d67..a22c7f272a4 100644
--- a/jbmc/regression/jbmc-strings/TokenTest02/test.desc
+++ b/jbmc/regression/jbmc-strings/TokenTest02/test.desc
@@ -1,8 +1,9 @@
-FUTURE
+CORE
 TokenTest02.class
---max-nondet-string-length 1000 --unwind 15
+--max-nondet-string-length 1000 --unwind 6 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
+line 13 assertion at file TokenTest02\.java .*: FAILURE
 --
 ^warning: ignoring