Merge pull request #2588 from ZGoriely/zgoriely/string-equals

romainbrenguier · web-flow · commit 46cd50b01662 · 2018-10-01T17:37:37.000+01:00
Implement model for String.equals
diff --git a/jbmc/lib/java-models-library b/jbmc/lib/java-models-library
@@ -1 +1 @@
-Subproject commit c86885cfd2e8cf98947132de15bcfa3835ae3ebc
+Subproject commit c9d9226d34649c21f30bb99f92e0a3d6e5fb8977
diff --git a/jbmc/regression/jbmc-strings/StringBuilderInsert/test.desc b/jbmc/regression/jbmc-strings/StringBuilderInsert/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.check
+--function Test.check --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 13 .*: SUCCESS
diff --git a/jbmc/regression/jbmc-strings/StringConcat_StringII/test.desc b/jbmc/regression/jbmc-strings/StringConcat_StringII/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---max-nondet-string-length 4 --verbosity 10 --unwind 5 --function Test.testSuccess
+--max-nondet-string-length 4 --verbosity 10 --unwind 5 --function Test.testSuccess --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 assertion at file Test.java line 23 .*: SUCCESS
diff --git a/jbmc/regression/jbmc-strings/StringConcatenation01/test.desc b/jbmc/regression/jbmc-strings/StringConcatenation01/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringConcatenation01.class
---max-nondet-string-length 1000
+--max-nondet-string-length 1000 --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/StringEquals/test.desc b/jbmc/regression/jbmc-strings/StringEquals/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---max-nondet-string-length 40 --function Test.check
+--max-nondet-string-length 40 --function Test.check --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 9 .* SUCCESS
diff --git a/jbmc/regression/jbmc-strings/StringEquals/test_verify_non_null.desc b/jbmc/regression/jbmc-strings/StringEquals/test_verify_non_null.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---max-nondet-string-length 20 --unwind 30 --function Test.verifyNonNull
+--max-nondet-string-length 20 --unwind 30 --function Test.verifyNonNull --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 assertion at file Test.java line 48 .* SUCCESS
diff --git a/jbmc/regression/jbmc-strings/StringMiscellaneous04/test.desc b/jbmc/regression/jbmc-strings/StringMiscellaneous04/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringMiscellaneous04.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/StringSubstring/test.desc b/jbmc/regression/jbmc-strings/StringSubstring/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---unwind 10 --max-nondet-string-length 6  --function Test.testSuccess
+--unwind 10 --max-nondet-string-length 6  --function Test.testSuccess --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 assertion at file Test.java line 21.*: SUCCESS
diff --git a/jbmc/regression/jbmc-strings/SubString01/test.desc b/jbmc/regression/jbmc-strings/SubString01/test.desc
@@ -1,6 +1,6 @@
 CORE
 SubString01.class
---max-nondet-string-length 1000
+--max-nondet-string-length 1000 --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/bug-test-gen-119-2/test.desc b/jbmc/regression/jbmc-strings/bug-test-gen-119-2/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringValueOfLong.class
---max-nondet-string-length 1000 --function StringValueOfLong.main
+--max-nondet-string-length 1000 --function StringValueOfLong.main --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/bug-test-gen-119/test.desc b/jbmc/regression/jbmc-strings/bug-test-gen-119/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringValueOfBool.class
---max-nondet-string-length 1000 --function StringValueOfBool.main
+--max-nondet-string-length 1000 --function StringValueOfBool.main --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/char_escape/test.desc b/jbmc/regression/jbmc-strings/char_escape/test.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.test --trace --json-ui
+--function Test.test --trace --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --json-ui
 ^EXIT=10$
 ^SIGNAL=0$
 "reason": "assertion at file Test.java line 14
diff --git a/jbmc/regression/jbmc-strings/java_append_char/test.desc b/jbmc/regression/jbmc-strings/java_append_char/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_append_char.class
---max-nondet-string-length 1000 --function test_append_char.main
+--max-nondet-string-length 1000 --function test_append_char.main --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/java_char_array_init/test.desc b/jbmc/regression/jbmc-strings/java_char_array_init/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_init.class
---max-nondet-string-length 1000 --function test_init.main
+--max-nondet-string-length 1000 --function test_init.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test_init.java line 31 .* SUCCESS$
diff --git a/jbmc/regression/jbmc-strings/java_insert_char/test.desc b/jbmc/regression/jbmc-strings/java_insert_char/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_char.class
---max-nondet-string-length 1000 --function test_insert_char.main
+--max-nondet-string-length 1000 --function test_insert_char.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 8.* FAILURE$
diff --git a/jbmc/regression/strings-smoke-tests/java_append_char/test.desc b/jbmc/regression/strings-smoke-tests/java_append_char/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_append_char.class
---verbosity 10 --max-nondet-string-length 1000
+--verbosity 10 --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test_append_char.java line 23 .* SUCCESS
diff --git a/jbmc/regression/strings-smoke-tests/java_append_string/test.desc b/jbmc/regression/strings-smoke-tests/java_append_string/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_append_string.class
---verbosity 10 --max-nondet-string-length 1000 --function test_append_string.main
+--verbosity 10 --max-nondet-string-length 1000 --function test_append_string.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/strings-smoke-tests/java_case/test.desc b/jbmc/regression/strings-smoke-tests/java_case/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_case.class
---verbosity 10 --max-nondet-string-length 1000 --function test_case.main
+--verbosity 10 --max-nondet-string-length 1000 --function test_case.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test_case.java line 10 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_delete_char_at/test.desc b/jbmc/regression/strings-smoke-tests/java_delete_char_at/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_delete_char_at.class
---verbosity 10 --max-nondet-string-length 1000 --function test_delete_char_at.main
+--verbosity 10 --max-nondet-string-length 1000 --function test_delete_char_at.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/strings-smoke-tests/java_equal/test.desc b/jbmc/regression/strings-smoke-tests/java_equal/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_equal.class
---verbosity 10 --max-nondet-string-length 100
+--verbosity 10 --max-nondet-string-length 100 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* FAILURE$
diff --git a/jbmc/regression/strings-smoke-tests/java_format/test.desc b/jbmc/regression/strings-smoke-tests/java_format/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---verbosity 10 --max-nondet-string-length 20 --function test.main
+--verbosity 10 --max-nondet-string-length 20 --function test.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 6.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_format2/test.desc b/jbmc/regression/strings-smoke-tests/java_format2/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---verbosity 10 --max-nondet-string-length 20 --function test.main
+--verbosity 10 --max-nondet-string-length 20 --function test.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 6.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_format3/test.desc b/jbmc/regression/strings-smoke-tests/java_format3/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---verbosity 10 --max-nondet-string-length 20 --function test.main
+--verbosity 10 --max-nondet-string-length 20 --function test.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 7.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_if/test.desc b/jbmc/regression/strings-smoke-tests/java_if/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---verbosity 10 --max-nondet-string-length 100 --function test.main
+--verbosity 10 --max-nondet-string-length 100 --function test.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 11.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_insert_char/test.desc b/jbmc/regression/strings-smoke-tests/java_insert_char/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_char.class
---verbosity 10  --max-nondet-string-length 1000 --function test_insert_char.main
+--verbosity 10  --max-nondet-string-length 1000 --function test_insert_char.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/strings-smoke-tests/java_insert_char_array/test.desc b/jbmc/regression/strings-smoke-tests/java_insert_char_array/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_char_array.class
---verbosity 10 --max-nondet-string-length 1000 --function test_insert_char_array.main
+--verbosity 10 --max-nondet-string-length 1000 --function test_insert_char_array.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test_insert_char_array.java line 20 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_insert_multiple/test.desc b/jbmc/regression/strings-smoke-tests/java_insert_multiple/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_multiple.class
---verbosity 10 --max-nondet-string-length 1000 --function test_insert_multiple.main
+--verbosity 10 --max-nondet-string-length 1000 --function test_insert_multiple.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/strings-smoke-tests/java_insert_string/test.desc b/jbmc/regression/strings-smoke-tests/java_insert_string/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_string.class
---verbosity 10 --max-nondet-string-length 1000 --function test_insert_string.main
+--verbosity 10 --max-nondet-string-length 1000 --function test_insert_string.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string/test1.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string/test1.desc
@@ -1,6 +1,6 @@
 CORE
 Test1.class
---verbosity 10 --max-nondet-string-length 1000 --function Test1.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test1.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string/test2.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string/test2.desc
@@ -1,6 +1,6 @@
 CORE
 Test2.class
---verbosity 10 --max-nondet-string-length 1000 --function Test2.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test2.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string/test3.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string/test3.desc
@@ -1,6 +1,6 @@
 CORE
 Test3.class
---verbosity 10 --max-nondet-string-length 1000 --function Test3.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test3.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string/test4.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string/test4.desc
@@ -1,6 +1,6 @@
 CORE
 Test4.class
---verbosity 10 --max-nondet-string-length 1000 --function Test4.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test4.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string/test5.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string/test5.desc
@@ -1,6 +1,6 @@
 CORE
 Test5.class
---verbosity 10 --max-nondet-string-length 1000 --function Test5.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test5.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary1.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary1.desc
@@ -1,6 +1,6 @@
 CORE
 Test_binary1.class
---verbosity 10 --max-nondet-string-length 1000 --function Test_binary1.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test_binary1.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary2.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary2.desc
@@ -1,6 +1,6 @@
 CORE
 Test_binary2.class
---verbosity 10 --max-nondet-string-length 1000 --function Test_binary2.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test_binary2.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary3.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary3.desc
@@ -1,6 +1,6 @@
 CORE
 Test_binary3.class
---verbosity 10 --max-nondet-string-length 1000 --function Test_binary3.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test_binary3.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_decimal.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_decimal.desc
@@ -1,6 +1,6 @@
 CORE
 Test_decimal.class
---verbosity 10 --max-nondet-string-length 1000 --function Test_decimal.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test_decimal.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex1.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex1.desc
@@ -1,6 +1,6 @@
 CORE
 Test_hex1.class
---verbosity 10 --max-nondet-string-length 1000 --function Test_hex1.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test_hex1.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex2.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex2.desc
@@ -1,6 +1,6 @@
 CORE
 Test_hex2.class
---verbosity 10 --max-nondet-string-length 1000 --function Test_hex2.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test_hex2.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex3.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex3.desc
@@ -1,6 +1,6 @@
 CORE
 Test_hex3.class
---verbosity 10 --max-nondet-string-length 100 --function Test_hex3.main
+--verbosity 10 --max-nondet-string-length 100 --function Test_hex3.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal1.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal1.desc
@@ -1,6 +1,6 @@
 CORE
 Test_octal1.class
---verbosity 10 --max-nondet-string-length 1000 --function Test_octal1.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test_octal1.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal2.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal2.desc
@@ -1,6 +1,6 @@
 CORE
 Test_octal2.class
---verbosity 10 --max-nondet-string-length 1000 --function Test_octal2.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test_octal2.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal3.desc b/jbmc/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal3.desc
@@ -1,6 +1,6 @@
 CORE
 Test_octal3.class
---verbosity 10 --max-nondet-string-length 1000 --function Test_octal3.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test_octal3.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_long_to_string/test1.desc b/jbmc/regression/strings-smoke-tests/java_long_to_string/test1.desc
@@ -1,6 +1,6 @@
 CORE
 Test1.class
---verbosity 10 --max-nondet-string-length 1000 --function Test1.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test1.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_long_to_string/test5.desc b/jbmc/regression/strings-smoke-tests/java_long_to_string/test5.desc
@@ -1,6 +1,6 @@
 CORE
 Test5.class
---verbosity 10 --max-nondet-string-length 1000 --function Test5.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test5.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_decimal.desc b/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_decimal.desc
@@ -1,6 +1,6 @@
 CORE
 Test_decimal.class
---verbosity 10 --max-nondet-string-length 1000 --function Test_decimal.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test_decimal.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex1.desc b/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex1.desc
@@ -1,6 +1,6 @@
 CORE
 Test_hex1.class
---verbosity 10 --max-nondet-string-length 1000 --function Test_hex1.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test_hex1.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex2.desc b/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex2.desc
@@ -1,6 +1,6 @@
 CORE
 Test_hex2.class
---verbosity 10 --max-nondet-string-length 1000 --function Test_hex2.main
+--verbosity 10 --max-nondet-string-length 1000 --function Test_hex2.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex3.desc b/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex3.desc
@@ -1,6 +1,6 @@
 CORE
 Test_hex3.class
---verbosity 10 --max-nondet-string-length 100 --function Test_hex3.main
+--verbosity 10 --max-nondet-string-length 100 --function Test_hex3.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal1.desc b/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal1.desc
@@ -1,6 +1,6 @@
 CORE
 Test_octal1.class
---verbosity 10 --max-nondet-string-length 100 --function Test_octal1.main
+--verbosity 10 --max-nondet-string-length 100 --function Test_octal1.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal2.desc b/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal2.desc
diff --git a/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal3.desc b/jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal3.desc
diff --git a/jbmc/regression/strings-smoke-tests/java_replace_char/test.desc b/jbmc/regression/strings-smoke-tests/java_replace_char/test.desc
diff --git a/jbmc/regression/strings-smoke-tests/java_set_char_at/test.desc b/jbmc/regression/strings-smoke-tests/java_set_char_at/test.desc
diff --git a/jbmc/regression/strings-smoke-tests/java_string_printable/test.desc b/jbmc/regression/strings-smoke-tests/java_string_printable/test.desc
diff --git a/jbmc/regression/strings-smoke-tests/java_value_of_float/test.desc b/jbmc/regression/strings-smoke-tests/java_value_of_float/test.desc
diff --git a/jbmc/regression/strings-smoke-tests/java_value_of_long/test.desc b/jbmc/regression/strings-smoke-tests/java_value_of_long/test.desc
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.h b/jbmc/src/java_bytecode/java_string_library_preprocess.h
diff --git a/src/solvers/flattening/boolbv_array.cpp b/src/solvers/flattening/boolbv_array.cpp
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
