Merge pull request #8553 from peterschrammel/ps/compile-java-regressi…

…on-test-sources4 Compile Java regression test sources (4/n)
diffblue · Jan 6, 2025 · 5ae1452 · 5ae1452
2 parents 1e99418 + 7e4897c
commit 5ae1452
Show file tree

Hide file tree

Showing 280 changed files with 1,554 additions and 93 deletions.
diff --git a/jbmc/CMakeLists.txt b/jbmc/CMakeLists.txt
@@ -56,3 +56,5 @@ add_custom_command(OUTPUT ${java_regression_compiled_sources}
 add_custom_target(java-regression ALL
     DEPENDS ${java_regression_compiled_sources}
 )
+
+add_dependencies(java-regression java-models-library)
diff --git a/jbmc/regression/jbmc/ArithmeticException2/ArithmeticExceptionTest.class b/jbmc/regression/jbmc/ArithmeticException2/ArithmeticExceptionTest.class
diff --git a/jbmc/regression/jbmc/ArithmeticException2/pom.xml b/jbmc/regression/jbmc/ArithmeticException2/pom.xml
@@ -0,0 +1,30 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project xmlns="http://maven.apache.org/POM/4.0.0"
+         xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+         xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
+    <modelVersion>4.0.0</modelVersion>
+    <groupId>org.cprover.regression</groupId>
+    <artifactId>regression.jbmc.ArithmeticException2</artifactId>
+    <version>1.0-SNAPSHOT</version>
+
+    <parent>
+        <groupId>org.cprover.regression</groupId>
+        <artifactId>regression.jbmc</artifactId>
+        <version>1.0-SNAPSHOT</version>
+    </parent>
+
+    <build>
+        <plugins>
+            <plugin>
+                <artifactId>maven-jar-plugin</artifactId>
+                <executions>
+                    <execution>
+                        <id>default-jar</id>
+                        <phase>none</phase>
+                    </execution>
+                </executions>
+            </plugin>
+        </plugins>
+    </build>
+
+</project>
diff --git a/...icException2/ArithmeticExceptionTest.java → ...rc/main/java/ArithmeticExceptionTest.java b/...icException2/ArithmeticExceptionTest.java → ...rc/main/java/ArithmeticExceptionTest.java
diff --git a/jbmc/regression/jbmc/ArithmeticException2/test.desc b/jbmc/regression/jbmc/ArithmeticException2/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest
---throw-runtime-exceptions
+--throw-runtime-exceptions -cp target/classes
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 9 function.*: FAILURE$

diff --git a/jbmc/regression/jbmc/ArithmeticException3/ArithmeticExceptionTest.class b/jbmc/regression/jbmc/ArithmeticException3/ArithmeticExceptionTest.class
diff --git a/jbmc/regression/jbmc/ArithmeticException3/pom.xml b/jbmc/regression/jbmc/ArithmeticException3/pom.xml
@@ -0,0 +1,30 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project xmlns="http://maven.apache.org/POM/4.0.0"
+         xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+         xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
+    <modelVersion>4.0.0</modelVersion>
+    <groupId>org.cprover.regression</groupId>
+    <artifactId>regression.jbmc.ArithmeticException3</artifactId>
+    <version>1.0-SNAPSHOT</version>
+
+    <parent>
+        <groupId>org.cprover.regression</groupId>
+        <artifactId>regression.jbmc</artifactId>
+        <version>1.0-SNAPSHOT</version>
+    </parent>
+
+    <build>
+        <plugins>
+            <plugin>
+                <artifactId>maven-jar-plugin</artifactId>
+                <executions>
+                    <execution>
+                        <id>default-jar</id>
+                        <phase>none</phase>
+                    </execution>
+                </executions>
+            </plugin>
+        </plugins>
+    </build>
+
+</project>
diff --git a/...icException3/ArithmeticExceptionTest.java → ...rc/main/java/ArithmeticExceptionTest.java b/...icException3/ArithmeticExceptionTest.java → ...rc/main/java/ArithmeticExceptionTest.java
diff --git a/jbmc/regression/jbmc/ArithmeticException3/test.desc b/jbmc/regression/jbmc/ArithmeticException3/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest
---throw-runtime-exceptions
+--throw-runtime-exceptions -cp target/classes
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$

diff --git a/jbmc/regression/jbmc/ArithmeticException4/ArithmeticExceptionTest.class b/jbmc/regression/jbmc/ArithmeticException4/ArithmeticExceptionTest.class
diff --git a/jbmc/regression/jbmc/ArithmeticException4/pom.xml b/jbmc/regression/jbmc/ArithmeticException4/pom.xml
@@ -0,0 +1,30 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project xmlns="http://maven.apache.org/POM/4.0.0"
+         xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+         xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
+    <modelVersion>4.0.0</modelVersion>
+    <groupId>org.cprover.regression</groupId>
+    <artifactId>regression.jbmc.ArithmeticException4</artifactId>
+    <version>1.0-SNAPSHOT</version>
+
+    <parent>
+        <groupId>org.cprover.regression</groupId>
+        <artifactId>regression.jbmc</artifactId>
+        <version>1.0-SNAPSHOT</version>
+    </parent>
+
+    <build>
+        <plugins>
+            <plugin>
+                <artifactId>maven-jar-plugin</artifactId>
+                <executions>
+                    <execution>
+                        <id>default-jar</id>
+                        <phase>none</phase>
+                    </execution>
+                </executions>
+            </plugin>
+        </plugins>
+    </build>
+
+</project>
diff --git a/...icException4/ArithmeticExceptionTest.java → ...rc/main/java/ArithmeticExceptionTest.java b/...icException4/ArithmeticExceptionTest.java → ...rc/main/java/ArithmeticExceptionTest.java
diff --git a/jbmc/regression/jbmc/ArithmeticException4/test.desc b/jbmc/regression/jbmc/ArithmeticException4/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest
---throw-runtime-exceptions
+--throw-runtime-exceptions -cp target/classes
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 9 function.*: FAILURE$

diff --git a/jbmc/regression/jbmc/ArithmeticException5/ArithmeticExceptionTest.class b/jbmc/regression/jbmc/ArithmeticException5/ArithmeticExceptionTest.class
diff --git a/jbmc/regression/jbmc/ArithmeticException5/pom.xml b/jbmc/regression/jbmc/ArithmeticException5/pom.xml
@@ -0,0 +1,30 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project xmlns="http://maven.apache.org/POM/4.0.0"
+         xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+         xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
+    <modelVersion>4.0.0</modelVersion>
+    <groupId>org.cprover.regression</groupId>
+    <artifactId>regression.jbmc.ArithmeticException5</artifactId>
+    <version>1.0-SNAPSHOT</version>
+
+    <parent>
+        <groupId>org.cprover.regression</groupId>
+        <artifactId>regression.jbmc</artifactId>
+        <version>1.0-SNAPSHOT</version>
+    </parent>
+
+    <build>
+        <plugins>
+            <plugin>
+                <artifactId>maven-jar-plugin</artifactId>
+                <executions>
+                    <execution>
+                        <id>default-jar</id>
+                        <phase>none</phase>
+                    </execution>
+                </executions>
+            </plugin>
+        </plugins>
+    </build>
+
+</project>
diff --git a/...icException5/ArithmeticExceptionTest.java → ...rc/main/java/ArithmeticExceptionTest.java b/...icException5/ArithmeticExceptionTest.java → ...rc/main/java/ArithmeticExceptionTest.java
diff --git a/jbmc/regression/jbmc/ArithmeticException5/test.desc b/jbmc/regression/jbmc/ArithmeticException5/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest
---throw-runtime-exceptions
+--throw-runtime-exceptions -cp target/classes
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

diff --git a/jbmc/regression/jbmc/ArithmeticException6/ArithmeticExceptionTest.class b/jbmc/regression/jbmc/ArithmeticException6/ArithmeticExceptionTest.class
diff --git a/jbmc/regression/jbmc/ArithmeticException6/pom.xml b/jbmc/regression/jbmc/ArithmeticException6/pom.xml
@@ -0,0 +1,30 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project xmlns="http://maven.apache.org/POM/4.0.0"
+         xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+         xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
+    <modelVersion>4.0.0</modelVersion>
+    <groupId>org.cprover.regression</groupId>
+    <artifactId>regression.jbmc.ArithmeticException6</artifactId>
+    <version>1.0-SNAPSHOT</version>
+
+    <parent>
+        <groupId>org.cprover.regression</groupId>
+        <artifactId>regression.jbmc</artifactId>
+        <version>1.0-SNAPSHOT</version>
+    </parent>
+
+    <build>
+        <plugins>
+            <plugin>
+                <artifactId>maven-jar-plugin</artifactId>
+                <executions>
+                    <execution>
+                        <id>default-jar</id>
+                        <phase>none</phase>
+                    </execution>
+                </executions>
+            </plugin>
+        </plugins>
+    </build>
+
+</project>
diff --git a/...icException6/ArithmeticExceptionTest.java → ...rc/main/java/ArithmeticExceptionTest.java b/...icException6/ArithmeticExceptionTest.java → ...rc/main/java/ArithmeticExceptionTest.java
diff --git a/jbmc/regression/jbmc/ArithmeticException6/test.desc b/jbmc/regression/jbmc/ArithmeticException6/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest
---throw-runtime-exceptions --function ArithmeticExceptionTest.main
+--throw-runtime-exceptions --function ArithmeticExceptionTest.main -cp target/classes
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 7 function.*: FAILURE$

diff --git a/jbmc/regression/jbmc/ArithmeticException7/ArithmeticExceptionTest.class b/jbmc/regression/jbmc/ArithmeticException7/ArithmeticExceptionTest.class
diff --git a/jbmc/regression/jbmc/ArithmeticException7/java/lang/ArithmeticException.class b/jbmc/regression/jbmc/ArithmeticException7/java/lang/ArithmeticException.class
diff --git a/jbmc/regression/jbmc/ArithmeticException7/java/lang/RuntimeException.class b/jbmc/regression/jbmc/ArithmeticException7/java/lang/RuntimeException.class
diff --git a/jbmc/regression/jbmc/ArithmeticException7/pom.xml b/jbmc/regression/jbmc/ArithmeticException7/pom.xml
@@ -0,0 +1,30 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project xmlns="http://maven.apache.org/POM/4.0.0"
+         xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+         xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
+    <modelVersion>4.0.0</modelVersion>
+    <groupId>org.cprover.regression</groupId>
+    <artifactId>regression.jbmc.ArithmeticException7</artifactId>
+    <version>1.0-SNAPSHOT</version>
+
+    <parent>
+        <groupId>org.cprover.regression</groupId>
+        <artifactId>regression.jbmc</artifactId>
+        <version>1.0-SNAPSHOT</version>
+    </parent>
+
+    <build>
+        <plugins>
+            <plugin>
+                <artifactId>maven-jar-plugin</artifactId>
+                <executions>
+                    <execution>
+                        <id>default-jar</id>
+                        <phase>none</phase>
+                    </execution>
+                </executions>
+            </plugin>
+        </plugins>
+    </build>
+
+</project>
diff --git a/...icException7/ArithmeticExceptionTest.java → ...rc/main/java/ArithmeticExceptionTest.java b/...icException7/ArithmeticExceptionTest.java → ...rc/main/java/ArithmeticExceptionTest.java
diff --git a/...ption7/java/lang/ArithmeticException.java → ...n/java/java/lang/ArithmeticException.java b/...ption7/java/lang/ArithmeticException.java → ...n/java/java/lang/ArithmeticException.java
diff --git a/...xception7/java/lang/RuntimeException.java → ...main/java/java/lang/RuntimeException.java b/...xception7/java/lang/RuntimeException.java → ...main/java/java/lang/RuntimeException.java
diff --git a/jbmc/regression/jbmc/ArithmeticException7/test.desc b/jbmc/regression/jbmc/ArithmeticException7/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest
---throw-runtime-exceptions
+--throw-runtime-exceptions -cp target/classes
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$

diff --git a/.../regression/jbmc/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.class b/.../regression/jbmc/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.class
diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/pom.xml b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/pom.xml
@@ -0,0 +1,30 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project xmlns="http://maven.apache.org/POM/4.0.0"
+         xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+         xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
+    <modelVersion>4.0.0</modelVersion>
+    <groupId>org.cprover.regression</groupId>
+    <artifactId>regression.jbmc.ArrayIndexOutOfBoundsException1</artifactId>
+    <version>1.0-SNAPSHOT</version>
+
+    <parent>
+        <groupId>org.cprover.regression</groupId>
+        <artifactId>regression.jbmc</artifactId>
+        <version>1.0-SNAPSHOT</version>
+    </parent>
+
+    <build>
+        <plugins>
+            <plugin>
+                <artifactId>maven-jar-plugin</artifactId>
+                <executions>
+                    <execution>
+                        <id>default-jar</id>
+                        <phase>none</phase>
+                    </execution>
+                </executions>
+            </plugin>
+        </plugins>
+    </build>
+
+</project>
diff --git a/...1/ArrayIndexOutOfBoundsExceptionTest.java → ...a/ArrayIndexOutOfBoundsExceptionTest.java b/...1/ArrayIndexOutOfBoundsExceptionTest.java → ...a/ArrayIndexOutOfBoundsExceptionTest.java
diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/test.desc b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArrayIndexOutOfBoundsExceptionTest
---throw-runtime-exceptions
+--throw-runtime-exceptions -cp target/classes
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 8 function.*: FAILURE$

diff --git a/.../regression/jbmc/ArrayIndexOutOfBoundsException2/ArrayIndexOutOfBoundsExceptionTest.class b/.../regression/jbmc/ArrayIndexOutOfBoundsException2/ArrayIndexOutOfBoundsExceptionTest.class
diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/pom.xml b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/pom.xml
@@ -0,0 +1,30 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project xmlns="http://maven.apache.org/POM/4.0.0"
+         xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+         xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
+    <modelVersion>4.0.0</modelVersion>
+    <groupId>org.cprover.regression</groupId>
+    <artifactId>regression.jbmc.ArrayIndexOutOfBoundsException2</artifactId>
+    <version>1.0-SNAPSHOT</version>
+
+    <parent>
+        <groupId>org.cprover.regression</groupId>
+        <artifactId>regression.jbmc</artifactId>
+        <version>1.0-SNAPSHOT</version>
+    </parent>
+
+    <build>
+        <plugins>
+            <plugin>
+                <artifactId>maven-jar-plugin</artifactId>
+                <executions>
+                    <execution>
+                        <id>default-jar</id>
+                        <phase>none</phase>
+                    </execution>
+                </executions>
+            </plugin>
+        </plugins>
+    </build>
+
+</project>
diff --git a/...2/ArrayIndexOutOfBoundsExceptionTest.java → ...a/ArrayIndexOutOfBoundsExceptionTest.java b/...2/ArrayIndexOutOfBoundsExceptionTest.java → ...a/ArrayIndexOutOfBoundsExceptionTest.java
diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/test.desc b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArrayIndexOutOfBoundsExceptionTest
---throw-runtime-exceptions
+--throw-runtime-exceptions -cp target/classes
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 8 function.*: FAILURE$

diff --git a/.../regression/jbmc/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.class b/.../regression/jbmc/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.class
diff --git a/...ssion/jbmc/ArrayIndexOutOfBoundsException3/java/lang/ArrayIndexOutOfBoundsException.class b/...ssion/jbmc/ArrayIndexOutOfBoundsException3/java/lang/ArrayIndexOutOfBoundsException.class
diff --git a/...regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.class b/...regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.class
diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/RuntimeException.class b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/RuntimeException.class
diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/pom.xml b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/pom.xml
@@ -0,0 +1,30 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project xmlns="http://maven.apache.org/POM/4.0.0"
+         xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+         xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
+    <modelVersion>4.0.0</modelVersion>
+    <groupId>org.cprover.regression</groupId>
+    <artifactId>regression.jbmc.ArrayIndexOutOfBoundsException3</artifactId>
+    <version>1.0-SNAPSHOT</version>
+
+    <parent>
+        <groupId>org.cprover.regression</groupId>
+        <artifactId>regression.jbmc</artifactId>
+        <version>1.0-SNAPSHOT</version>
+    </parent>
+
+    <build>
+        <plugins>
+            <plugin>
+                <artifactId>maven-jar-plugin</artifactId>
+                <executions>
+                    <execution>
+                        <id>default-jar</id>
+                        <phase>none</phase>
+                    </execution>
+                </executions>
+            </plugin>
+        </plugins>
+    </build>
+
+</project>
diff --git a/...3/ArrayIndexOutOfBoundsExceptionTest.java → ...a/ArrayIndexOutOfBoundsExceptionTest.java b/...3/ArrayIndexOutOfBoundsExceptionTest.java → ...a/ArrayIndexOutOfBoundsExceptionTest.java
diff --git a/.../lang/ArrayIndexOutOfBoundsException.java → .../lang/ArrayIndexOutOfBoundsException.java b/.../lang/ArrayIndexOutOfBoundsException.java → .../lang/ArrayIndexOutOfBoundsException.java
diff --git a/.../java/lang/IndexOutOfBoundsException.java → .../java/lang/IndexOutOfBoundsException.java b/.../java/lang/IndexOutOfBoundsException.java → .../java/lang/IndexOutOfBoundsException.java
diff --git a/...xception3/java/lang/RuntimeException.java → ...main/java/java/lang/RuntimeException.java b/...xception3/java/lang/RuntimeException.java → ...main/java/java/lang/RuntimeException.java
diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/test.desc b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/test.desc
@@ -1,6 +1,6 @@
 CORE
 ArrayIndexOutOfBoundsExceptionTest
---throw-runtime-exceptions
+--throw-runtime-exceptions -cp target/classes
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 8 function.*: FAILURE$

diff --git a/jbmc/regression/jbmc/aastore_aaload1/A.class b/jbmc/regression/jbmc/aastore_aaload1/A.class
diff --git a/jbmc/regression/jbmc/aastore_aaload1/aastore_aaload1.class b/jbmc/regression/jbmc/aastore_aaload1/aastore_aaload1.class
diff --git a/jbmc/regression/jbmc/aastore_aaload1/pom.xml b/jbmc/regression/jbmc/aastore_aaload1/pom.xml
@@ -0,0 +1,30 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project xmlns="http://maven.apache.org/POM/4.0.0"
+         xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+         xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
+    <modelVersion>4.0.0</modelVersion>
+    <groupId>org.cprover.regression</groupId>
+    <artifactId>regression.jbmc.aastore_aaload1</artifactId>
+    <version>1.0-SNAPSHOT</version>
+
+    <parent>
+        <groupId>org.cprover.regression</groupId>
+        <artifactId>regression.jbmc</artifactId>
+        <version>1.0-SNAPSHOT</version>
+    </parent>
+
+    <build>
+        <plugins>
+            <plugin>
+                <artifactId>maven-jar-plugin</artifactId>
+                <executions>
+                    <execution>
+                        <id>default-jar</id>
+                        <phase>none</phase>
+                    </execution>
+                </executions>
+            </plugin>
+        </plugins>
+    </build>
+
+</project>
diff --git a/...jbmc/aastore_aaload1/aastore_aaload1.java → ...aload1/src/main/java/aastore_aaload1.java b/...jbmc/aastore_aaload1/aastore_aaload1.java → ...aload1/src/main/java/aastore_aaload1.java
diff --git a/jbmc/regression/jbmc/aastore_aaload1/test.desc b/jbmc/regression/jbmc/aastore_aaload1/test.desc
@@ -1,6 +1,6 @@
 CORE
 aastore_aaload1
-
+-cp target/classes
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

diff --git a/jbmc/regression/jbmc/address_space_size_limit1/Test.class b/jbmc/regression/jbmc/address_space_size_limit1/Test.class