diff --git a/jbmc/lib/java-models-library b/jbmc/lib/java-models-library
index 3163b09a9f4..1068a992642 160000
--- a/jbmc/lib/java-models-library
+++ b/jbmc/lib/java-models-library
@@ -1 +1 @@
-Subproject commit 3163b09a9f43ebe637caf508427b52e41e1993f2
+Subproject commit 1068a992642ab6adbe1d4aab2c868cf81445ca25
diff --git a/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc
index b1a75f2563d..386cc37503d 100644
--- a/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc
+++ b/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$
diff --git a/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test2.desc b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test2.desc
index a262228e038..c39ba088b5b 100644
--- a/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test2.desc
+++ b/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$
diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test.desc
index 500630ed419..124afa21ae7 100644
--- a/jbmc/regression/jbmc-concurrency/get-current-thread/test.desc
+++ b/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
diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test2.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test2.desc
index eb912a30fe3..4b2552572ad 100644
--- a/jbmc/regression/jbmc-concurrency/get-current-thread/test2.desc
+++ b/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
diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test3.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test3.desc
index ddf8a72a449..39c37fdf824 100644
--- a/jbmc/regression/jbmc-concurrency/get-current-thread/test3.desc
+++ b/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
diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test4.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test4.desc
index 3ea7924ede3..8ceb063f4f9 100644
--- a/jbmc/regression/jbmc-concurrency/get-current-thread/test4.desc
+++ b/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
diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test5.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test5.desc
index 9deba6c12de..6522d6f95a2 100644
--- a/jbmc/regression/jbmc-concurrency/get-current-thread/test5.desc
+++ b/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
diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test6.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test6.desc
index a939961f4a4..6bb22f0f8f9 100644
--- a/jbmc/regression/jbmc-concurrency/get-current-thread/test6.desc
+++ b/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
diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test_bug.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test_bug.desc
index 09ba6a5fcb0..5baecbc64b1 100644
--- a/jbmc/regression/jbmc-concurrency/get-current-thread/test_bug.desc
+++ b/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
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test.desc
index c58629abd8d..60b60587f48 100644
--- a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test.desc
+++ b/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
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test2.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test2.desc
index 6d75ed56e19..02c95662b4b 100644
--- a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test2.desc
+++ b/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
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test3.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test3.desc
index 5efe6550efd..3b9c0e1421f 100644
--- a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test3.desc
+++ b/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
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test4.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test4.desc
index 5ae79f1f394..eb5d686f26a 100644
--- a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test4.desc
+++ b/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
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/test.desc b/jbmc/regression/jbmc-concurrency/java-lang-thread/test.desc
index 3076c2d7519..8eec4067339 100644
--- a/jbmc/regression/jbmc-concurrency/java-lang-thread/test.desc
+++ b/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
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/test2.desc b/jbmc/regression/jbmc-concurrency/java-lang-thread/test2.desc
index 9f2b09a20a9..dbde3635d9f 100644
--- a/jbmc/regression/jbmc-concurrency/java-lang-thread/test2.desc
+++ b/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$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/test3.desc b/jbmc/regression/jbmc-concurrency/java-lang-thread/test3.desc
index 5c9593f210a..a4e55bfa5ec 100644
--- a/jbmc/regression/jbmc-concurrency/java-lang-thread/test3.desc
+++ b/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$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/test4.desc b/jbmc/regression/jbmc-concurrency/java-lang-thread/test4.desc
index 82910e4f4cf..0fc102be1da 100644
--- a/jbmc/regression/jbmc-concurrency/java-lang-thread/test4.desc
+++ b/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$
diff --git a/jbmc/regression/jbmc-concurrency/several-threads/test.desc b/jbmc/regression/jbmc-concurrency/several-threads/test.desc
index 599838f0a5e..cfd4860376d 100644
--- a/jbmc/regression/jbmc-concurrency/several-threads/test.desc
+++ b/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
diff --git a/jbmc/regression/jbmc-concurrency/several-threads/test2.desc b/jbmc/regression/jbmc-concurrency/several-threads/test2.desc
index a6dcc84f557..acfc61c48c6 100644
--- a/jbmc/regression/jbmc-concurrency/several-threads/test2.desc
+++ b/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$
diff --git a/jbmc/regression/jbmc-concurrency/several-threads/test3.desc b/jbmc/regression/jbmc-concurrency/several-threads/test3.desc
index f9e1cd58abe..cbcd840a1e0 100644
--- a/jbmc/regression/jbmc-concurrency/several-threads/test3.desc
+++ b/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$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/test.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/test.desc
index 47a4a6772fa..56746bc721c 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/test.desc
+++ b/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$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test.desc
index d5774c48850..21891800efb 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test.desc
+++ b/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
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc
index f430244ad39..2a4878a4737 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc
+++ b/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
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc
index 9232ded906f..f284db38cf3 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc
+++ b/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
 --
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc
index 74628ecb54d..ec805ab619a 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc
+++ b/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$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc
index 74628ecb54d..ec805ab619a 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc
+++ b/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$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync.desc
index 534e87da451..824bc5b0d11 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync.desc
+++ b/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$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync_baseline.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync_baseline.desc
index 3d50a965b8c..550429547e4 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync_baseline.desc
+++ b/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$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/test.desc b/jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/test.desc
index 0dfad82a676..22eaef591e3 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/test.desc
+++ b/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$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test1.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test1.desc
index 08f6afeac48..32be2704a71 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-methods/test1.desc
+++ b/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
 --
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test2.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test2.desc
index f77d63f540a..4420b0af9f2 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-methods/test2.desc
+++ b/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
 --
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test3.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test3.desc
index bad4684aeb4..e79944afd03 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-methods/test3.desc
+++ b/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
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync.desc
index 131f69beaee..3d6edf4b922 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync.desc
+++ b/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$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_baseline.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_baseline.desc
index 534e87da451..824bc5b0d11 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_baseline.desc
+++ b/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$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_static.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_static.desc
index 19a3619ea42..771bdd9ba32 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_static.desc
+++ b/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$
diff --git a/jbmc/regression/jbmc/synchronized/Sync.class b/jbmc/regression/jbmc-concurrency/synchronized/Sync.class
similarity index 100%
rename from jbmc/regression/jbmc/synchronized/Sync.class
rename to jbmc/regression/jbmc-concurrency/synchronized/Sync.class
diff --git a/jbmc/regression/jbmc/synchronized/Sync.java b/jbmc/regression/jbmc-concurrency/synchronized/Sync.java
similarity index 100%
rename from jbmc/regression/jbmc/synchronized/Sync.java
rename to jbmc/regression/jbmc-concurrency/synchronized/Sync.java
diff --git a/jbmc/regression/jbmc-concurrency/synchronized/test.desc b/jbmc/regression/jbmc-concurrency/synchronized/test.desc
new file mode 100644
index 00000000000..5921af6c569
--- /dev/null
+++ b/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
+--
diff --git a/jbmc/regression/jbmc-generics/type_erasure/test.desc b/jbmc/regression/jbmc-generics/type_erasure/test.desc
index 117f6e0a8a2..0665b549d34 100644
--- a/jbmc/regression/jbmc-generics/type_erasure/test.desc
+++ b/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
diff --git a/jbmc/regression/jbmc/NondetEnumArg/test_some_constant.desc b/jbmc/regression/jbmc/NondetEnumArg/test_some_constant.desc
index 2e88221ea60..27ebc3bcf16 100644
--- a/jbmc/regression/jbmc/NondetEnumArg/test_some_constant.desc
+++ b/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$
diff --git a/jbmc/regression/jbmc/NondetEnumArg/test_specific_constant1.desc b/jbmc/regression/jbmc/NondetEnumArg/test_specific_constant1.desc
index 4f4d5c34208..b4304eb8ba6 100644
--- a/jbmc/regression/jbmc/NondetEnumArg/test_specific_constant1.desc
+++ b/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$
 --
 --
diff --git a/jbmc/regression/jbmc/NondetEnumArg/test_specific_constant2.desc b/jbmc/regression/jbmc/NondetEnumArg/test_specific_constant2.desc
index 52b06d65b1c..4e477d932ae 100644
--- a/jbmc/regression/jbmc/NondetEnumArg/test_specific_constant2.desc
+++ b/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$
 --
 --
diff --git a/jbmc/regression/jbmc/NondetEnumArg/test_specific_constant3.desc b/jbmc/regression/jbmc/NondetEnumArg/test_specific_constant3.desc
index 3913535c8c4..f7a50aa07c0 100644
--- a/jbmc/regression/jbmc/NondetEnumArg/test_specific_constant3.desc
+++ b/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$
 --
 --
diff --git a/jbmc/regression/jbmc/NondetEnumArgField/test.desc b/jbmc/regression/jbmc/NondetEnumArgField/test.desc
index f5b4de914db..48937ec19ce 100644
--- a/jbmc/regression/jbmc/NondetEnumArgField/test.desc
+++ b/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$
 --
 --
diff --git a/jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_some_constant.desc b/jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_some_constant.desc
index 4628904c706..802ee8f24d3 100644
--- a/jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_some_constant.desc
+++ b/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$
diff --git a/jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant1.desc b/jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant1.desc
index 52ab297e335..42d534d40b9 100644
--- a/jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant1.desc
+++ b/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$
 --
 --
diff --git a/jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant2.desc b/jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant2.desc
index 22e146eaba5..656e2dafee7 100644
--- a/jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant2.desc
+++ b/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$
 --
 --
diff --git a/jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant3.desc b/jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant3.desc
index e347386333e..425b27ce549 100644
--- a/jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant3.desc
+++ b/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$
 --
 --
diff --git a/jbmc/regression/jbmc/coreModels/test.desc b/jbmc/regression/jbmc/coreModels/test.desc
index 9390687e25c..66aec4a4d28 100644
--- a/jbmc/regression/jbmc/coreModels/test.desc
+++ b/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$
diff --git a/jbmc/regression/jbmc/enum_values_clone/test.desc b/jbmc/regression/jbmc/enum_values_clone/test.desc
index 3d6fc869747..b9df8aece96 100644
--- a/jbmc/regression/jbmc/enum_values_clone/test.desc
+++ b/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$
 --
diff --git a/jbmc/regression/jbmc/enum_values_clone_name/test.desc b/jbmc/regression/jbmc/enum_values_clone_name/test.desc
index 3d6fc869747..b9df8aece96 100644
--- a/jbmc/regression/jbmc/enum_values_clone_name/test.desc
+++ b/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$
 --
diff --git a/jbmc/regression/jbmc/nondet-static/test.desc b/jbmc/regression/jbmc/nondet-static/test.desc
index f401d5bfe06..fd4d2a8b78f 100644
--- a/jbmc/regression/jbmc/nondet-static/test.desc
+++ b/jbmc/regression/jbmc/nondet-static/test.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 My.class
---function "My.<init>" --nondet-static --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function "My.<init>" --nondet-static --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 file My\.java line 104 function java::My\.\<init\>:\(I\)V.*FAILURE$
diff --git a/jbmc/regression/jbmc/string_field_aliasing/test.desc b/jbmc/regression/jbmc/string_field_aliasing/test.desc
index 62e5918320d..a152589bfed 100644
--- a/jbmc/regression/jbmc/string_field_aliasing/test.desc
+++ b/jbmc/regression/jbmc/string_field_aliasing/test.desc
@@ -1,6 +1,6 @@
 CORE
 Cart.class
---cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --trace --java-max-vla-length 96 --java-unwind-enum-static --max-nondet-string-length 200 --unwind 4 Cart.class --function Cart.checkTax4 --string-printable
+--cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --trace --java-max-vla-length 96 --java-unwind-enum-static --max-nondet-string-length 200 --unwind 4 Cart.class --function Cart.checkTax4 --string-printable
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/jbmc/regression/jbmc/synchronized/test.desc b/jbmc/regression/jbmc/synchronized/test.desc
deleted file mode 100644
index 7155ff81375..00000000000
--- a/jbmc/regression/jbmc/synchronized/test.desc
+++ /dev/null
@@ -1,10 +0,0 @@
-KNOWNBUG
-Sync.class
-
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
---
-See #1236 for details of this test.