diff --git a/jbmc/regression/jbmc/classpath-class-incorrect-package/src/Test.class b/jbmc/regression/jbmc/classpath-class-incorrect-package/src/Test.class
new file mode 100644
index 00000000000..27e5f9e511c
Binary files /dev/null and b/jbmc/regression/jbmc/classpath-class-incorrect-package/src/Test.class differ
diff --git a/jbmc/regression/jbmc/classpath-class-incorrect-package/src/Test.java b/jbmc/regression/jbmc/classpath-class-incorrect-package/src/Test.java
new file mode 100644
index 00000000000..0054455a672
--- /dev/null
+++ b/jbmc/regression/jbmc/classpath-class-incorrect-package/src/Test.java
@@ -0,0 +1,9 @@
+package com.diffblue;
+
+class Test
+{
+  public static void main(String[] args)
+  {
+    assert true;
+  }
+}
diff --git a/jbmc/regression/jbmc/classpath-class-incorrect-package/test.desc b/jbmc/regression/jbmc/classpath-class-incorrect-package/test.desc
new file mode 100644
index 00000000000..80c7ebf54e1
--- /dev/null
+++ b/jbmc/regression/jbmc/classpath-class-incorrect-package/test.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+Test.class
+--classpath src
+^EXIT=6$
+--
+Java main class: Test
+failed to open input file `Test.class'
+--
+Test.class is not in the right directory corresponding to its package.
+Issue: 2864
diff --git a/jbmc/regression/jbmc/classpath-class-with-jar/Test.class b/jbmc/regression/jbmc/classpath-class-with-jar/Test.class
new file mode 100644
index 00000000000..bf4867ab5c6
Binary files /dev/null and b/jbmc/regression/jbmc/classpath-class-with-jar/Test.class differ
diff --git a/jbmc/regression/jbmc/classpath-class-with-jar/Test.java b/jbmc/regression/jbmc/classpath-class-with-jar/Test.java
new file mode 100644
index 00000000000..cb017abd1cd
--- /dev/null
+++ b/jbmc/regression/jbmc/classpath-class-with-jar/Test.java
@@ -0,0 +1,7 @@
+class Test
+{
+  public static void main(String[] args)
+  {
+    TestJar.foo();
+  }
+}
diff --git a/jbmc/regression/jbmc/classpath-class-with-jar/src.jar b/jbmc/regression/jbmc/classpath-class-with-jar/src.jar
new file mode 100644
index 00000000000..8976dd278fb
Binary files /dev/null and b/jbmc/regression/jbmc/classpath-class-with-jar/src.jar differ
diff --git a/jbmc/regression/jbmc/classpath-class-with-jar/src/TestJar.java b/jbmc/regression/jbmc/classpath-class-with-jar/src/TestJar.java
new file mode 100644
index 00000000000..f7c15870e2f
--- /dev/null
+++ b/jbmc/regression/jbmc/classpath-class-with-jar/src/TestJar.java
@@ -0,0 +1,7 @@
+class TestJar
+{
+  public static void foo()
+  {
+    assert false;
+  }
+}
diff --git a/jbmc/regression/jbmc/classpath-class-with-jar/test.desc b/jbmc/regression/jbmc/classpath-class-with-jar/test.desc
new file mode 100644
index 00000000000..32571dc6baf
--- /dev/null
+++ b/jbmc/regression/jbmc/classpath-class-with-jar/test.desc
@@ -0,0 +1,8 @@
+CORE
+Test.class
+--classpath `../../../../scripts/format_classpath.sh src.jar .`
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/jbmc/regression/jbmc/classpath-class-with-one-dir/Test.class b/jbmc/regression/jbmc/classpath-class-with-one-dir/Test.class
new file mode 100644
index 00000000000..2801e8c0610
Binary files /dev/null and b/jbmc/regression/jbmc/classpath-class-with-one-dir/Test.class differ
diff --git a/jbmc/regression/jbmc/classpath-class-with-one-dir/Test.java b/jbmc/regression/jbmc/classpath-class-with-one-dir/Test.java
new file mode 100644
index 00000000000..29a4d8a5ecf
--- /dev/null
+++ b/jbmc/regression/jbmc/classpath-class-with-one-dir/Test.java
@@ -0,0 +1,7 @@
+class Test
+{
+  public static void main(String[] args)
+  {
+    assert false;
+  }
+}
diff --git a/jbmc/regression/jbmc/classpath-class-with-one-dir/src/Test.class b/jbmc/regression/jbmc/classpath-class-with-one-dir/src/Test.class
new file mode 100644
index 00000000000..587e7a0bc95
Binary files /dev/null and b/jbmc/regression/jbmc/classpath-class-with-one-dir/src/Test.class differ
diff --git a/jbmc/regression/jbmc/classpath-class-with-one-dir/src/Test.java b/jbmc/regression/jbmc/classpath-class-with-one-dir/src/Test.java
new file mode 100644
index 00000000000..7038818c774
--- /dev/null
+++ b/jbmc/regression/jbmc/classpath-class-with-one-dir/src/Test.java
@@ -0,0 +1,7 @@
+class Test
+{
+  public static void main(String[] args)
+  {
+    assert true;
+  }
+}
diff --git a/jbmc/regression/jbmc/classpath1/test.desc b/jbmc/regression/jbmc/classpath-class-with-one-dir/test.desc
similarity index 70%
rename from jbmc/regression/jbmc/classpath1/test.desc
rename to jbmc/regression/jbmc/classpath-class-with-one-dir/test.desc
index 455f17677e9..9bb5514b8ff 100644
--- a/jbmc/regression/jbmc/classpath1/test.desc
+++ b/jbmc/regression/jbmc/classpath-class-with-one-dir/test.desc
@@ -1,6 +1,6 @@
 CORE
-test.class
--classpath my_cp:.
+Test.class
+--classpath src
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc/classpath-class-with-one-dir/test_override.desc b/jbmc/regression/jbmc/classpath-class-with-one-dir/test_override.desc
new file mode 100644
index 00000000000..93ba662c03b
--- /dev/null
+++ b/jbmc/regression/jbmc/classpath-class-with-one-dir/test_override.desc
@@ -0,0 +1,10 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--classpath wrong
+^EXIT=6$
+^SIGNAL=0$
+the program has no entry point
+--
+--
+We override the default path. Hence, Test cannot be found.
+Currently fails because symex-driven lazy-loading aborts without an error message.
diff --git a/jbmc/regression/jbmc/classpath-class-with-one-dir/test_prefix.desc b/jbmc/regression/jbmc/classpath-class-with-one-dir/test_prefix.desc
new file mode 100644
index 00000000000..540db90a556
--- /dev/null
+++ b/jbmc/regression/jbmc/classpath-class-with-one-dir/test_prefix.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+src/Test.class
+
+^EXIT=6$
+--
+Parsing src/Test.class
+--
+Test class is not in src package. Therefore, this must fail.
+Issue: 2864
diff --git a/jbmc/regression/jbmc/classpath1/my_cp/test2.class b/jbmc/regression/jbmc/classpath-class-with-two-dirs/my_cp/test2.class
similarity index 100%
rename from jbmc/regression/jbmc/classpath1/my_cp/test2.class
rename to jbmc/regression/jbmc/classpath-class-with-two-dirs/my_cp/test2.class
diff --git a/jbmc/regression/jbmc/classpath1/my_cp/test2.java b/jbmc/regression/jbmc/classpath-class-with-two-dirs/my_cp/test2.java
similarity index 100%
rename from jbmc/regression/jbmc/classpath1/my_cp/test2.java
rename to jbmc/regression/jbmc/classpath-class-with-two-dirs/my_cp/test2.java
diff --git a/jbmc/regression/jbmc/classpath1/test.class b/jbmc/regression/jbmc/classpath-class-with-two-dirs/test.class
similarity index 100%
rename from jbmc/regression/jbmc/classpath1/test.class
rename to jbmc/regression/jbmc/classpath-class-with-two-dirs/test.class
diff --git a/jbmc/regression/jbmc/classpath-class-with-two-dirs/test.desc b/jbmc/regression/jbmc/classpath-class-with-two-dirs/test.desc
new file mode 100644
index 00000000000..d0d1ee2ef5e
--- /dev/null
+++ b/jbmc/regression/jbmc/classpath-class-with-two-dirs/test.desc
@@ -0,0 +1,8 @@
+CORE
+test.class
+--classpath `../../../../scripts/format_classpath.sh my_cp .`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/jbmc/regression/jbmc/classpath1/test.java b/jbmc/regression/jbmc/classpath-class-with-two-dirs/test.java
similarity index 100%
rename from jbmc/regression/jbmc/classpath1/test.java
rename to jbmc/regression/jbmc/classpath-class-with-two-dirs/test.java
diff --git a/jbmc/regression/jbmc/invalid_classpath/Test.class b/jbmc/regression/jbmc/classpath-invalid/Test.class
similarity index 100%
rename from jbmc/regression/jbmc/invalid_classpath/Test.class
rename to jbmc/regression/jbmc/classpath-invalid/Test.class
diff --git a/jbmc/regression/jbmc/invalid_classpath/Test.java b/jbmc/regression/jbmc/classpath-invalid/Test.java
similarity index 100%
rename from jbmc/regression/jbmc/invalid_classpath/Test.java
rename to jbmc/regression/jbmc/classpath-invalid/Test.java
diff --git a/jbmc/regression/jbmc/invalid_classpath/test-jar.desc b/jbmc/regression/jbmc/classpath-invalid/test-jar.desc
similarity index 100%
rename from jbmc/regression/jbmc/invalid_classpath/test-jar.desc
rename to jbmc/regression/jbmc/classpath-invalid/test-jar.desc
diff --git a/jbmc/regression/jbmc/invalid_classpath/test-path.desc b/jbmc/regression/jbmc/classpath-invalid/test-path.desc
similarity index 100%
rename from jbmc/regression/jbmc/invalid_classpath/test-path.desc
rename to jbmc/regression/jbmc/classpath-invalid/test-path.desc
diff --git a/jbmc/regression/jbmc/classpath-invalid/test_jar_warning.desc b/jbmc/regression/jbmc/classpath-invalid/test_jar_warning.desc
new file mode 100644
index 00000000000..6a9b4ae290b
--- /dev/null
+++ b/jbmc/regression/jbmc/classpath-invalid/test_jar_warning.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+Test.class
+--classpath ./NotHere.jar
+^EXIT=0$
+^SIGNAL=0$
+^Warning: file './NotHere.jar' does not exist$
+--
+--
+Issue: 2864
diff --git a/jbmc/regression/jbmc/classpath-invalid/test_path_warning.desc b/jbmc/regression/jbmc/classpath-invalid/test_path_warning.desc
new file mode 100644
index 00000000000..8bb4dcbc9f0
--- /dev/null
+++ b/jbmc/regression/jbmc/classpath-invalid/test_path_warning.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+Test.class
+--classpath `../../../../scripts/format_classpath.sh ./NotHere .`
+^EXIT=0$
+^SIGNAL=0$
+^Warning: path './NotHere' does not exist$
+--
+--
diff --git a/jbmc/regression/jbmc/classpath-jar-incorrect-package/src/Test.java b/jbmc/regression/jbmc/classpath-jar-incorrect-package/src/Test.java
new file mode 100644
index 00000000000..0054455a672
--- /dev/null
+++ b/jbmc/regression/jbmc/classpath-jar-incorrect-package/src/Test.java
@@ -0,0 +1,9 @@
+package com.diffblue;
+
+class Test
+{
+  public static void main(String[] args)
+  {
+    assert true;
+  }
+}
diff --git a/jbmc/regression/jbmc/classpath-jar-incorrect-package/test.jar b/jbmc/regression/jbmc/classpath-jar-incorrect-package/test.jar
new file mode 100644
index 00000000000..cb1a50cbab5
Binary files /dev/null and b/jbmc/regression/jbmc/classpath-jar-incorrect-package/test.jar differ
diff --git a/jbmc/regression/jbmc/classpath-jar-incorrect-package/test_class.desc b/jbmc/regression/jbmc/classpath-jar-incorrect-package/test_class.desc
new file mode 100644
index 00000000000..e4f84fe8460
--- /dev/null
+++ b/jbmc/regression/jbmc/classpath-jar-incorrect-package/test_class.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+Test.class
+--classpath test.jar
+^EXIT=6$
+--
+Java main class: Test
+failed to open input file `Test.class'
+--
+Test.class is not in the right directory corresponding to its package.
+Issue: 2864
diff --git a/jbmc/regression/jbmc/classpath-jar-incorrect-package/test_jar_main_class.desc b/jbmc/regression/jbmc/classpath-jar-incorrect-package/test_jar_main_class.desc
new file mode 100644
index 00000000000..4571dd6f8ce
--- /dev/null
+++ b/jbmc/regression/jbmc/classpath-jar-incorrect-package/test_jar_main_class.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+test.jar
+--main-class Test.class
+^EXIT=6$
+--
+Java main class: Test
+failed to open input file `Test.class'
+--
+Test.class is not in the right directory corresponding to its package.
+Issue: 2864
diff --git a/jbmc/regression/jbmc/jar-file2/jar-file2.jar b/jbmc/regression/jbmc/classpath-jar-main-class/jar-file2.jar
similarity index 100%
rename from jbmc/regression/jbmc/jar-file2/jar-file2.jar
rename to jbmc/regression/jbmc/classpath-jar-main-class/jar-file2.jar
diff --git a/jbmc/regression/jbmc/jar-file2/some_class.java b/jbmc/regression/jbmc/classpath-jar-main-class/some_class.java
similarity index 100%
rename from jbmc/regression/jbmc/jar-file2/some_class.java
rename to jbmc/regression/jbmc/classpath-jar-main-class/some_class.java
diff --git a/jbmc/regression/jbmc/jar-file2/test.desc b/jbmc/regression/jbmc/classpath-jar-main-class/test.desc
similarity index 100%
rename from jbmc/regression/jbmc/jar-file2/test.desc
rename to jbmc/regression/jbmc/classpath-jar-main-class/test.desc
diff --git a/jbmc/regression/jbmc/jar-file3/A.jar b/jbmc/regression/jbmc/classpath-jar-with-two-jars/A.jar
similarity index 100%
rename from jbmc/regression/jbmc/jar-file3/A.jar
rename to jbmc/regression/jbmc/classpath-jar-with-two-jars/A.jar
diff --git a/jbmc/regression/jbmc/jar-file3/B.jar b/jbmc/regression/jbmc/classpath-jar-with-two-jars/B.jar
similarity index 100%
rename from jbmc/regression/jbmc/jar-file3/B.jar
rename to jbmc/regression/jbmc/classpath-jar-with-two-jars/B.jar
diff --git a/jbmc/regression/jbmc/jar-file3/C.jar b/jbmc/regression/jbmc/classpath-jar-with-two-jars/C.jar
similarity index 100%
rename from jbmc/regression/jbmc/jar-file3/C.jar
rename to jbmc/regression/jbmc/classpath-jar-with-two-jars/C.jar
diff --git a/jbmc/regression/jbmc/classpath2/jarfile3.class b/jbmc/regression/jbmc/classpath-jar-with-two-jars/jarfile3.class
similarity index 100%
rename from jbmc/regression/jbmc/classpath2/jarfile3.class
rename to jbmc/regression/jbmc/classpath-jar-with-two-jars/jarfile3.class
diff --git a/jbmc/regression/jbmc/classpath2/jarfile3.java b/jbmc/regression/jbmc/classpath-jar-with-two-jars/jarfile3.java
similarity index 100%
rename from jbmc/regression/jbmc/classpath2/jarfile3.java
rename to jbmc/regression/jbmc/classpath-jar-with-two-jars/jarfile3.java
diff --git a/jbmc/regression/jbmc/classpath-jar-with-two-jars/test.desc b/jbmc/regression/jbmc/classpath-jar-with-two-jars/test.desc
new file mode 100644
index 00000000000..3b323648e78
--- /dev/null
+++ b/jbmc/regression/jbmc/classpath-jar-with-two-jars/test.desc
@@ -0,0 +1,8 @@
+CORE
+C.jar
+--function jarfile3.f -classpath `../../../../scripts/format_classpath.sh A.jar B.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL
+--
+^warning: ignoring
diff --git a/jbmc/regression/jbmc/jar-file1/some_jar.jar b/jbmc/regression/jbmc/classpath-jar/some_jar.jar
similarity index 100%
rename from jbmc/regression/jbmc/jar-file1/some_jar.jar
rename to jbmc/regression/jbmc/classpath-jar/some_jar.jar
diff --git a/jbmc/regression/jbmc/jar-file1/test.desc b/jbmc/regression/jbmc/classpath-jar/test.desc
similarity index 100%
rename from jbmc/regression/jbmc/jar-file1/test.desc
rename to jbmc/regression/jbmc/classpath-jar/test.desc
diff --git a/jbmc/regression/jbmc/classpath-two-classes/Test.class b/jbmc/regression/jbmc/classpath-two-classes/Test.class
new file mode 100644
index 00000000000..9190401ce1b
Binary files /dev/null and b/jbmc/regression/jbmc/classpath-two-classes/Test.class differ
diff --git a/jbmc/regression/jbmc/classpath-two-classes/Test.java b/jbmc/regression/jbmc/classpath-two-classes/Test.java
new file mode 100644
index 00000000000..c28b4cdcfec
--- /dev/null
+++ b/jbmc/regression/jbmc/classpath-two-classes/Test.java
@@ -0,0 +1,8 @@
+class Test
+{
+  public static void main(String[] args)
+  {
+    Test2.foo();
+    assert true;
+  }
+}
diff --git a/jbmc/regression/jbmc/classpath-two-classes/Test2.class b/jbmc/regression/jbmc/classpath-two-classes/Test2.class
new file mode 100644
index 00000000000..a8d84461a86
Binary files /dev/null and b/jbmc/regression/jbmc/classpath-two-classes/Test2.class differ
diff --git a/jbmc/regression/jbmc/classpath-two-classes/Test2.java b/jbmc/regression/jbmc/classpath-two-classes/Test2.java
new file mode 100644
index 00000000000..ad41a0b21ac
--- /dev/null
+++ b/jbmc/regression/jbmc/classpath-two-classes/Test2.java
@@ -0,0 +1,7 @@
+class Test2
+{
+  public static void foo()
+  {
+    assert false;
+  }
+}
diff --git a/jbmc/regression/jbmc/classpath-two-classes/test.desc b/jbmc/regression/jbmc/classpath-two-classes/test.desc
new file mode 100644
index 00000000000..0e52df3241e
--- /dev/null
+++ b/jbmc/regression/jbmc/classpath-two-classes/test.desc
@@ -0,0 +1,8 @@
+CORE
+Test.class
+
+^EXIT=10$
+^VERIFICATION FAILED$
+--
+--
+Test2 is found because . is default classpath.
diff --git a/jbmc/regression/jbmc/classpath-two-classes/test_incorrect.desc b/jbmc/regression/jbmc/classpath-two-classes/test_incorrect.desc
new file mode 100644
index 00000000000..be27fd91d49
--- /dev/null
+++ b/jbmc/regression/jbmc/classpath-two-classes/test_incorrect.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+Test.class
+Test2.class
+^EXIT=6$
+--
+Invariant check failed
+--
+We don't allow two classes passed on the command line.
+Issue: 2864
diff --git a/jbmc/regression/jbmc/classpath-two-jars/Test.java b/jbmc/regression/jbmc/classpath-two-jars/Test.java
new file mode 100644
index 00000000000..c28b4cdcfec
--- /dev/null
+++ b/jbmc/regression/jbmc/classpath-two-jars/Test.java
@@ -0,0 +1,8 @@
+class Test
+{
+  public static void main(String[] args)
+  {
+    Test2.foo();
+    assert true;
+  }
+}
diff --git a/jbmc/regression/jbmc/classpath-two-jars/Test2.java b/jbmc/regression/jbmc/classpath-two-jars/Test2.java
new file mode 100644
index 00000000000..ad41a0b21ac
--- /dev/null
+++ b/jbmc/regression/jbmc/classpath-two-jars/Test2.java
@@ -0,0 +1,7 @@
+class Test2
+{
+  public static void foo()
+  {
+    assert false;
+  }
+}
diff --git a/jbmc/regression/jbmc/classpath-two-jars/lib/test2.jar b/jbmc/regression/jbmc/classpath-two-jars/lib/test2.jar
new file mode 100644
index 00000000000..d8e347697f3
Binary files /dev/null and b/jbmc/regression/jbmc/classpath-two-jars/lib/test2.jar differ
diff --git a/jbmc/regression/jbmc/classpath-two-jars/libs/test.jar b/jbmc/regression/jbmc/classpath-two-jars/libs/test.jar
new file mode 100644
index 00000000000..44d7af405d6
Binary files /dev/null and b/jbmc/regression/jbmc/classpath-two-jars/libs/test.jar differ
diff --git a/jbmc/regression/jbmc/classpath-two-jars/test.desc b/jbmc/regression/jbmc/classpath-two-jars/test.desc
new file mode 100644
index 00000000000..3b4730cad82
--- /dev/null
+++ b/jbmc/regression/jbmc/classpath-two-jars/test.desc
@@ -0,0 +1,8 @@
+CORE
+libs/test.jar
+--main-class Test --classpath lib/test2.jar
+^EXIT=10$
+^VERIFICATION FAILED$
+--
+--
+This is a correct way of dealing with two jars.
diff --git a/jbmc/regression/jbmc/classpath-two-jars/test2.desc b/jbmc/regression/jbmc/classpath-two-jars/test2.desc
new file mode 100644
index 00000000000..3a040529ef8
--- /dev/null
+++ b/jbmc/regression/jbmc/classpath-two-jars/test2.desc
@@ -0,0 +1,8 @@
+CORE
+lib/test2.jar
+--main-class Test --classpath libs/test.jar
+^EXIT=10$
+^VERIFICATION FAILED$
+--
+--
+This is a correct way of dealing with two jars.
diff --git a/jbmc/regression/jbmc/classpath-two-jars/test_incorrect.desc b/jbmc/regression/jbmc/classpath-two-jars/test_incorrect.desc
new file mode 100644
index 00000000000..8cf2f2aea0a
--- /dev/null
+++ b/jbmc/regression/jbmc/classpath-two-jars/test_incorrect.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+libs/test.jar
+lib/test2.jar --main-class Test.class
+^EXIT=6$
+--
+Invariant check failed
+the program has no entry point
+--
+We don't allow two jar files passed on the command line.
+Issue: 2864
diff --git a/jbmc/regression/jbmc/classpath-two-jars/test_incorrect2.desc b/jbmc/regression/jbmc/classpath-two-jars/test_incorrect2.desc
new file mode 100644
index 00000000000..39ab68717bb
--- /dev/null
+++ b/jbmc/regression/jbmc/classpath-two-jars/test_incorrect2.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+Test.class
+--classpath `../../../../scripts/format_classpath.sh libs/test.jar lib/test2.jar`
+^EXIT=6$
+--
+--
+This is incorrect as it would search for a Test.class file outside the jar files.
+Issue: 2864
diff --git a/jbmc/regression/jbmc/jar-file4/A.jar b/jbmc/regression/jbmc/cp-include-path-json/A.jar
similarity index 100%
rename from jbmc/regression/jbmc/jar-file4/A.jar
rename to jbmc/regression/jbmc/cp-include-path-json/A.jar
diff --git a/jbmc/regression/jbmc/jar-file4/B.jar b/jbmc/regression/jbmc/cp-include-path-json/B.jar
similarity index 100%
rename from jbmc/regression/jbmc/jar-file4/B.jar
rename to jbmc/regression/jbmc/cp-include-path-json/B.jar
diff --git a/jbmc/regression/jbmc/jar-file4/C.jar b/jbmc/regression/jbmc/cp-include-path-json/C.jar
similarity index 100%
rename from jbmc/regression/jbmc/jar-file4/C.jar
rename to jbmc/regression/jbmc/cp-include-path-json/C.jar
diff --git a/jbmc/regression/jbmc/jar-file4/jar.json b/jbmc/regression/jbmc/cp-include-path-json/jar.json
similarity index 100%
rename from jbmc/regression/jbmc/jar-file4/jar.json
rename to jbmc/regression/jbmc/cp-include-path-json/jar.json
diff --git a/jbmc/regression/jbmc/jar-file4/test.desc b/jbmc/regression/jbmc/cp-include-path-json/test.desc
similarity index 100%
rename from jbmc/regression/jbmc/jar-file4/test.desc
rename to jbmc/regression/jbmc/cp-include-path-json/test.desc
diff --git a/jbmc/regression/jbmc/classpath2/jarfile3$A.class b/jbmc/regression/jbmc/cp-include-path/jarfile3$A.class
similarity index 100%
rename from jbmc/regression/jbmc/classpath2/jarfile3$A.class
rename to jbmc/regression/jbmc/cp-include-path/jarfile3$A.class
diff --git a/jbmc/regression/jbmc/classpath2/jarfile3$B.class b/jbmc/regression/jbmc/cp-include-path/jarfile3$B.class
similarity index 100%
rename from jbmc/regression/jbmc/classpath2/jarfile3$B.class
rename to jbmc/regression/jbmc/cp-include-path/jarfile3$B.class
diff --git a/jbmc/regression/jbmc/jar-file3/jarfile3.class b/jbmc/regression/jbmc/cp-include-path/jarfile3.class
similarity index 100%
rename from jbmc/regression/jbmc/jar-file3/jarfile3.class
rename to jbmc/regression/jbmc/cp-include-path/jarfile3.class
diff --git a/jbmc/regression/jbmc/jar-file3/jarfile3.java b/jbmc/regression/jbmc/cp-include-path/jarfile3.java
similarity index 100%
rename from jbmc/regression/jbmc/jar-file3/jarfile3.java
rename to jbmc/regression/jbmc/cp-include-path/jarfile3.java
diff --git a/jbmc/regression/jbmc/classpath2/test.desc b/jbmc/regression/jbmc/cp-include-path/test.desc
similarity index 100%
rename from jbmc/regression/jbmc/classpath2/test.desc
rename to jbmc/regression/jbmc/cp-include-path/test.desc
diff --git a/jbmc/regression/jbmc/jar-file3/test.desc b/jbmc/regression/jbmc/jar-file3/test.desc
deleted file mode 100644
index 8d3b495e1c6..00000000000
--- a/jbmc/regression/jbmc/jar-file3/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-CORE
-C.jar
---function jarfile3.f -classpath A.jar:B.jar
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL
---
-^warning: ignoring