diff --git a/regression/cbmc-java/NegativeArraySizeException2/NegativeArraySizeExceptionTest.class b/regression/cbmc-java/NegativeArraySizeException2/NegativeArraySizeExceptionTest.class
new file mode 100644
index 00000000000..c51fb8edf43
Binary files /dev/null and b/regression/cbmc-java/NegativeArraySizeException2/NegativeArraySizeExceptionTest.class differ
diff --git a/regression/cbmc-java/NegativeArraySizeException2/NegativeArraySizeExceptionTest.java b/regression/cbmc-java/NegativeArraySizeException2/NegativeArraySizeExceptionTest.java
new file mode 100644
index 00000000000..b9361f0ed00
--- /dev/null
+++ b/regression/cbmc-java/NegativeArraySizeException2/NegativeArraySizeExceptionTest.java
@@ -0,0 +1,10 @@
+public class NegativeArraySizeExceptionTest {
+  public static void main(String args[]) {
+      try {
+          int a[]=new int[-1];
+      }
+      catch (Exception exc) {
+          assert false;
+      }
+  }
+}
diff --git a/regression/cbmc-java/NegativeArraySizeException2/java/lang/NegativeArraySizeException.class b/regression/cbmc-java/NegativeArraySizeException2/java/lang/NegativeArraySizeException.class
new file mode 100644
index 00000000000..ec5f9692af7
Binary files /dev/null and b/regression/cbmc-java/NegativeArraySizeException2/java/lang/NegativeArraySizeException.class differ
diff --git a/regression/cbmc-java/NegativeArraySizeException2/java/lang/NegativeArraySizeException.java b/regression/cbmc-java/NegativeArraySizeException2/java/lang/NegativeArraySizeException.java
new file mode 100644
index 00000000000..ec7cea1e756
--- /dev/null
+++ b/regression/cbmc-java/NegativeArraySizeException2/java/lang/NegativeArraySizeException.java
@@ -0,0 +1,4 @@
+package java.lang;
+
+public class NegativeArraySizeException extends RuntimeException {
+}
diff --git a/regression/cbmc-java/NegativeArraySizeException2/java/lang/RuntimeException.class b/regression/cbmc-java/NegativeArraySizeException2/java/lang/RuntimeException.class
new file mode 100644
index 00000000000..2f0ac26544c
Binary files /dev/null and b/regression/cbmc-java/NegativeArraySizeException2/java/lang/RuntimeException.class differ
diff --git a/regression/cbmc-java/NegativeArraySizeException2/java/lang/RuntimeException.java b/regression/cbmc-java/NegativeArraySizeException2/java/lang/RuntimeException.java
new file mode 100644
index 00000000000..3be7f777cc0
--- /dev/null
+++ b/regression/cbmc-java/NegativeArraySizeException2/java/lang/RuntimeException.java
@@ -0,0 +1,4 @@
+package java.lang;
+
+public class RuntimeException extends Exception {
+}
diff --git a/regression/cbmc-java/NegativeArraySizeException2/test.desc b/regression/cbmc-java/NegativeArraySizeException2/test.desc
new file mode 100644
index 00000000000..a203a79a628
--- /dev/null
+++ b/regression/cbmc-java/NegativeArraySizeException2/test.desc
@@ -0,0 +1,9 @@
+CORE
+NegativeArraySizeExceptionTest.class
+--java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file NegativeArraySizeExceptionTest.java line 7 function.*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring