diff --git a/jbmc/lib/java-models-library b/jbmc/lib/java-models-library index 766ac7a2c87..1f41012e0cd 160000 --- a/jbmc/lib/java-models-library +++ b/jbmc/lib/java-models-library @@ -1 +1 @@ -Subproject commit 766ac7a2c87dadfc7286ea0aab0a6eabdf3e4cdc +Subproject commit 1f41012e0cdb10371fe1e37348dfeabc8205bdf4 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$