Merge pull request #3423 from peterschrammel/enable-monitor-exceptions

Update jbmc/lib/java-models-library to #11 (enable-monitor-exceptions)

jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test2.desc

@@ -1,5 +1,5 @@
 CORE
 A.class
---function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-concurrency/get-current-thread/test.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

jbmc/regression/jbmc-concurrency/get-current-thread/test2.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 A.class
---function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

jbmc/regression/jbmc-concurrency/get-current-thread/test3.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 A.class
---function 'A.me3:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me3:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

jbmc/regression/jbmc-concurrency/get-current-thread/test4.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me4:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me4:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

jbmc/regression/jbmc-concurrency/get-current-thread/test5.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me5:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me5:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

jbmc/regression/jbmc-concurrency/get-current-thread/test6.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me6:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me6:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

jbmc/regression/jbmc-concurrency/get-current-thread/test_bug.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 A.class
---function 'A.me_bug:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me_bug:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

jbmc/regression/jbmc-concurrency/java-lang-runnable/test.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

jbmc/regression/jbmc-concurrency/java-lang-runnable/test2.desc

@@ -1,5 +1,5 @@
 CORE
 A.class
---function 'A.me2:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function 'A.me2:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^SIGNAL=0$
 ^VERIFICATION FAILED

jbmc/regression/jbmc-concurrency/java-lang-runnable/test3.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me4:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function 'A.me4:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

jbmc/regression/jbmc-concurrency/java-lang-runnable/test4.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me3:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function 'A.me3:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

jbmc/regression/jbmc-concurrency/java-lang-thread/test.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me:()V'  --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function 'A.me:()V'  --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

jbmc/regression/jbmc-concurrency/java-lang-thread/test2.desc

@@ -1,5 +1,5 @@
 CORE
 A.class
---function 'A.me2:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function 'A.me2:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-concurrency/java-lang-thread/test3.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me4:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function 'A.me4:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/jbmc-concurrency/java-lang-thread/test4.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me3:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function 'A.me3:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/jbmc-concurrency/several-threads/test.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function A.me --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function A.me --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

jbmc/regression/jbmc-concurrency/several-threads/test2.desc

@@ -1,5 +1,5 @@
 CORE
 A.class
---function A.me2 --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function A.me2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc-concurrency/several-threads/test3.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function A.me3 --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading --unwind 3
+--function A.me3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading --unwind 3
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 Sync.class
---cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 Sync.class
---cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 Sync.class
---cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions --java-threading
+--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-goto-functions --java-threading
 ATOMIC_BEGIN
 ATOMIC_END
 --

jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
+--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync_baseline.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/test.desc

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

jbmc/regression/jbmc-concurrency/synchronized-methods/test1.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions
+--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-goto-functions
 ATOMIC_BEGIN
 ATOMIC_END
 --

jbmc/regression/jbmc-concurrency/synchronized-methods/test2.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions
+--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-goto-functions
 ATOMIC_BEGIN
 ATOMIC_END
 --

jbmc/regression/jbmc-concurrency/synchronized-methods/test3.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me3:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me3:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_baseline.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_static.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 A.class
---function 'A.me4:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me4:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-concurrency/synchronized/test.desc

@@ -0,0 +1,9 @@
+CORE
+Sync.class
+--java-threading --throw-runtime-exceptions --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--

jbmc/regression/jbmc-generics/type_erasure/test.desc

@@ -1,6 +1,6 @@
 CORE
 TestClass.class
---function TestClass.testFunction --classpath `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function TestClass.testFunction --classpath `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 EXIT=0
 SIGNAL=0
 VERIFICATION SUCCESSFUL

jbmc/regression/jbmc/NondetEnumArg/test_some_constant.desc

@@ -1,6 +1,6 @@
 CORE
 NondetEnumArg.class
---function NondetEnumArg.canChooseSomeConstant --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function NondetEnumArg.canChooseSomeConstant --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/jbmc/NondetEnumArg/test_specific_constant1.desc

@@ -1,6 +1,6 @@
 CORE
 NondetEnumArg.class
---function NondetEnumArg.canChooseRed --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function NondetEnumArg.canChooseRed --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^VERIFICATION FAILED$
 --
 --

jbmc/regression/jbmc/NondetEnumArg/test_specific_constant2.desc

@@ -1,6 +1,6 @@
 CORE
 NondetEnumArg.class
---function NondetEnumArg.canChooseGreen --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function NondetEnumArg.canChooseGreen --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^VERIFICATION FAILED$
 --
 --

jbmc/regression/jbmc/NondetEnumArg/test_specific_constant3.desc

@@ -1,6 +1,6 @@
 CORE
 NondetEnumArg.class
---function NondetEnumArg.canChooseBlue --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function NondetEnumArg.canChooseBlue --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^VERIFICATION FAILED$
 --
 --

jbmc/regression/jbmc/NondetEnumArgField/test.desc

@@ -1,6 +1,6 @@
 CORE
 NondetEnumArgField.class
---function NondetEnumArgField.test --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function NondetEnumArgField.test --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^VERIFICATION FAILED$
 --
 --

jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_some_constant.desc

@@ -1,6 +1,6 @@
 CORE
 NondetEnumOpaqueReturn.class
---function NondetEnumOpaqueReturn.canChooseSomeConstant --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function NondetEnumOpaqueReturn.canChooseSomeConstant --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant1.desc

@@ -1,6 +1,6 @@
 CORE
 NondetEnumOpaqueReturn.class
---function NondetEnumOpaqueReturn.canChooseRed --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function NondetEnumOpaqueReturn.canChooseRed --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^VERIFICATION FAILED$
 --
 --

jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant2.desc

@@ -1,6 +1,6 @@
 CORE
 NondetEnumOpaqueReturn.class
---function NondetEnumOpaqueReturn.canChooseGreen --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function NondetEnumOpaqueReturn.canChooseGreen --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^VERIFICATION FAILED$
 --
 --

jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant3.desc

@@ -1,6 +1,6 @@
 CORE
 NondetEnumOpaqueReturn.class
---function NondetEnumOpaqueReturn.canChooseBlue --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function NondetEnumOpaqueReturn.canChooseBlue --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^VERIFICATION FAILED$
 --
 --

jbmc/regression/jbmc/coreModels/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
---no-lazy-methods --no-refine-strings --show-symbol-table --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--no-lazy-methods --no-refine-strings --show-symbol-table --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^Symbol\s*\.*\: java\:\:org\.cprover\.CProver\.\<init\>\:\(\)V$

jbmc/regression/jbmc/enum_values_clone/test.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 com/diffblue/regression/EnumIter.class
---java-max-vla-length 16 --max-nondet-string-length 20 --string-printable --unwind 2 --function "com.diffblue.regression.EnumIter.f" --java-unwind-enum-static --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--java-max-vla-length 16 --max-nondet-string-length 20 --string-printable --unwind 2 --function "com.diffblue.regression.EnumIter.f" --java-unwind-enum-static --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 --

jbmc/regression/jbmc/enum_values_clone_name/test.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 com/diffblue/regression/EnumIter.class
---java-max-vla-length 16 --max-nondet-string-length 20 --string-printable --unwind 2 --function "com.diffblue.regression.EnumIter.f" --java-unwind-enum-static --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--java-max-vla-length 16 --max-nondet-string-length 20 --string-printable --unwind 2 --function "com.diffblue.regression.EnumIter.f" --java-unwind-enum-static --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 --