jbmc THOROUGH regression tests: fix spec files

Several tests spuriously failed as they were lacking the Java models
library. Some of them also do not need to be marked as "THOROUGH" for
they terminate in under 1 second. One test moved from THOROUGH to
KNOWNBUG as the assertions are (unexpectedly) deemed unreachable.

Author: tautschnig

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

@@ -1,7 +1,6 @@
 THOROUGH
 Test
---function Test.check --max-nondet-string-length 50 --unwind 50 --java-assume-inputs-non-null
-^EXIT=10$
+--function Test.check --max-nondet-string-length 50 --unwind 50 --java-assume-inputs-non-null  --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
+VERIFICATION SUCCESSFUL
+^EXIT=0$
 ^SIGNAL=0$
-assertion at file Test.java line 32 .* SUCCESS$
-assertion at file Test.java line 34 .* FAILURE$

jbmc/regression/strings-smoke-tests/java_format5/test.desc

@@ -1,6 +1,6 @@
-THOROUGH
+CORE
 test
---max-nondet-string-length 20
+--function test.main --max-nondet-string-length 20  --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 7.* SUCCESS$

jbmc/regression/strings-smoke-tests/java_long_to_string/test2.desc

@@ -1,6 +1,6 @@
-THOROUGH
+CORE
 Test2
---max-nondet-string-length 1000 --function Test2.main
+--max-nondet-string-length 1000 --function Test2.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_long_to_string/test3.desc

@@ -1,6 +1,6 @@
-THOROUGH
+CORE
 Test3
---max-nondet-string-length 1000 --function Test3.main
+--max-nondet-string-length 1000 --function Test3.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_long_to_string/test4.desc

@@ -1,6 +1,6 @@
-THOROUGH
+CORE
 Test4
---max-nondet-string-length 1000 --function Test4.main
+--max-nondet-string-length 1000 --function Test4.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary1.desc

@@ -1,6 +1,6 @@
-THOROUGH
+CORE
 Test_binary1
---max-nondet-string-length 1000 --function Test_binary1.main
+--max-nondet-string-length 1000 --function Test_binary1.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary2.desc

@@ -1,6 +1,6 @@
-THOROUGH
+CORE
 Test_binary2
---max-nondet-string-length 1000 --function Test_binary2.main
+--max-nondet-string-length 1000 --function Test_binary2.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary3.desc

@@ -1,6 +1,6 @@
-THOROUGH
+CORE
 Test_binary3
---max-nondet-string-length 1000 --function Test_binary3.main
+--max-nondet-string-length 1000 --function Test_binary3.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_value_of_float_4/test.desc

@@ -1,6 +1,6 @@
 THOROUGH
 test
---max-nondet-string-length 1000 --function test.check
+--max-nondet-string-length 1000 --function test.check --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* test.java line 8 .* SUCCESS$

jbmc/regression/strings-smoke-tests/java_value_of_float_5/test.desc

@@ -1,6 +1,6 @@
-THOROUGH
+KNOWNBUG
 test
---max-nondet-string-length 1000 --function test.check
+--max-nondet-string-length 1000 --function test.check --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test.java line 6 .* SUCCESS$