fixup! Implement model for String.equals

Author: romainbrenguier

jbmc/regression/jbmc-strings/StringBuilderInsert/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.check --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--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

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 --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--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

jbmc/regression/jbmc-strings/StringConcatenation01/test.desc

@@ -1,6 +1,6 @@
 CORE
 StringConcatenation01.class
---max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-strings/StringEquals/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---max-nondet-string-length 40 --function Test.check --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--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

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 --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--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

jbmc/regression/jbmc-strings/StringMiscellaneous04/test.desc

@@ -1,6 +1,6 @@
 CORE
 StringMiscellaneous04.class
---max-nondet-string-length 1000 --unwind 30 --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--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$

jbmc/regression/jbmc-strings/StringSubstring/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---unwind 10 --max-nondet-string-length 6  --function Test.testSuccess --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--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

jbmc/regression/jbmc-strings/SubString01/test.desc

@@ -1,6 +1,6 @@
 CORE
 SubString01.class
---max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

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 --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--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$

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 --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--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$

jbmc/regression/jbmc-strings/char_escape/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.test --cover location --trace --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function Test.test --cover location --trace --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 file Test.java line 14 .*: SATISFIED

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 --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--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$

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 --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--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$

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 --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--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$