diff --git a/regression/cbmc-java/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.class b/regression/cbmc-java/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.class
index 4aeaf643291..ca15fe999ec 100644
Binary files a/regression/cbmc-java/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.class and b/regression/cbmc-java/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.class differ
diff --git a/regression/cbmc-java/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.java b/regression/cbmc-java/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.java
index 265b89ec489..2013694f875 100644
--- a/regression/cbmc-java/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.java
+++ b/regression/cbmc-java/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.java
@@ -3,7 +3,6 @@ public static void main(String args[]) {
       try {
           int[] a=new int[4];
           a[4]=0;
-          throw new RuntimeException();
       }
       catch (ArrayIndexOutOfBoundsException exc) {
           assert false;
diff --git a/regression/cbmc-java/ArrayIndexOutOfBoundsException1/test.desc b/regression/cbmc-java/ArrayIndexOutOfBoundsException1/test.desc
index 092cbf0b1f4..e6216e07c79 100644
--- a/regression/cbmc-java/ArrayIndexOutOfBoundsException1/test.desc
+++ b/regression/cbmc-java/ArrayIndexOutOfBoundsException1/test.desc
@@ -3,7 +3,7 @@ ArrayIndexOutOfBoundsExceptionTest.class
 --java-throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
-^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 9 function.*: FAILURE$
+^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 8 function.*: FAILURE$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-java/ArrayIndexOutOfBoundsException2/ArrayIndexOutOfBoundsExceptionTest.class b/regression/cbmc-java/ArrayIndexOutOfBoundsException2/ArrayIndexOutOfBoundsExceptionTest.class
new file mode 100644
index 00000000000..3de63e25a0f
Binary files /dev/null and b/regression/cbmc-java/ArrayIndexOutOfBoundsException2/ArrayIndexOutOfBoundsExceptionTest.class differ
diff --git a/regression/cbmc-java/ArrayIndexOutOfBoundsException2/ArrayIndexOutOfBoundsExceptionTest.java b/regression/cbmc-java/ArrayIndexOutOfBoundsException2/ArrayIndexOutOfBoundsExceptionTest.java
new file mode 100644
index 00000000000..b1f8683115e
--- /dev/null
+++ b/regression/cbmc-java/ArrayIndexOutOfBoundsException2/ArrayIndexOutOfBoundsExceptionTest.java
@@ -0,0 +1,11 @@
+public class ArrayIndexOutOfBoundsExceptionTest {
+  public static void main(String args[]) {
+      try {
+          int[] a=new int[4];
+          int i=a[5];
+      }
+      catch (ArrayIndexOutOfBoundsException exc) {
+          assert false;
+      }
+  }
+}
diff --git a/regression/cbmc-java/ArrayIndexOutOfBoundsException2/test.desc b/regression/cbmc-java/ArrayIndexOutOfBoundsException2/test.desc
new file mode 100644
index 00000000000..e6216e07c79
--- /dev/null
+++ b/regression/cbmc-java/ArrayIndexOutOfBoundsException2/test.desc
@@ -0,0 +1,9 @@
+CORE
+ArrayIndexOutOfBoundsExceptionTest.class
+--java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 8 function.*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.class b/regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.class
index de62bd5ca58..f791d7e4fcd 100644
Binary files a/regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.class and b/regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.class differ
diff --git a/regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.java b/regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.java
index bb7eacd1647..e3a87f5a163 100644
--- a/regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.java
+++ b/regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.java
@@ -3,7 +3,6 @@ public static void main(String args[]) {
       try {
           Object x = new Integer(0);
           String y = (String)x;
-          throw new RuntimeException();
       }
       catch (ClassCastException exc) {
           assert false;
diff --git a/regression/cbmc-java/ClassCastException1/test.desc b/regression/cbmc-java/ClassCastException1/test.desc
index 983d5f730d8..fa84bf185ab 100644
--- a/regression/cbmc-java/ClassCastException1/test.desc
+++ b/regression/cbmc-java/ClassCastException1/test.desc
@@ -3,7 +3,7 @@ ClassCastExceptionTest.class
 --java-throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
-^.*assertion at file ClassCastExceptionTest.java line 9 function.*: FAILURE$
+^.*assertion at file ClassCastExceptionTest.java line 8 function.*: FAILURE$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.java b/regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.java
index d8979415dbc..6b83050ca6a 100644
--- a/regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.java
+++ b/regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.java
@@ -9,9 +9,6 @@ public static void main(String args[]) {
       try {
           A c = new C();
           B b = (B)c;
-          // TODO: an explicit throw is currently needed in order
-          // for CBMC to convert the exception handler
-          throw new RuntimeException();
       }
       catch (ClassCastException exc) {
           assert false;
diff --git a/regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeExceptionTest.class b/regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeExceptionTest.class
new file mode 100644
index 00000000000..70adc3ee839
Binary files /dev/null and b/regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeExceptionTest.class differ
diff --git a/regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeExceptionTest.java b/regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeExceptionTest.java
new file mode 100644
index 00000000000..d9c9859aa1f
--- /dev/null
+++ b/regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeExceptionTest.java
@@ -0,0 +1,10 @@
+public class NegativeArraySizeExceptionTest {
+  public static void main(String args[]) {
+      try {
+          int a[]=new int[-1];
+      }
+      catch (NegativeArraySizeException exc) {
+          assert false;
+      }
+  }
+}
diff --git a/regression/cbmc-java/NegativeArraySizeException/test.desc b/regression/cbmc-java/NegativeArraySizeException/test.desc
new file mode 100644
index 00000000000..a203a79a628
--- /dev/null
+++ b/regression/cbmc-java/NegativeArraySizeException/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
diff --git a/regression/cbmc-java/NullPointerException2/Test.class b/regression/cbmc-java/NullPointerException2/Test.class
index e49a2d70d61..9885d01cc77 100644
Binary files a/regression/cbmc-java/NullPointerException2/Test.class and b/regression/cbmc-java/NullPointerException2/Test.class differ
diff --git a/regression/cbmc-java/NullPointerException2/Test.java b/regression/cbmc-java/NullPointerException2/Test.java
index cf04d9edefb..684e6725a70 100644
--- a/regression/cbmc-java/NullPointerException2/Test.java
+++ b/regression/cbmc-java/NullPointerException2/Test.java
@@ -9,9 +9,6 @@ public static void main(String args[]) {
         A a=null;
         try {
             a.i=0;
-            // TODO: an explicit throw is currently needed in order
-            // for CBMC to convert the exception handler
-            throw new B();
         }
         catch (NullPointerException exc) {
             assert false;
diff --git a/regression/cbmc-java/NullPointerException2/test.desc b/regression/cbmc-java/NullPointerException2/test.desc
index ed7e923ae16..e4ad2c5739d 100644
--- a/regression/cbmc-java/NullPointerException2/test.desc
+++ b/regression/cbmc-java/NullPointerException2/test.desc
@@ -3,7 +3,7 @@ Test.class
 --java-throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
-^.*assertion at file Test.java line 17 function.*: FAILURE$
+^.*assertion at file Test.java line 14 function.*: FAILURE$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-java/NullPointerException3/Test.class b/regression/cbmc-java/NullPointerException3/Test.class
index 77c124a4b86..7f90d2404b4 100644
Binary files a/regression/cbmc-java/NullPointerException3/Test.class and b/regression/cbmc-java/NullPointerException3/Test.class differ
diff --git a/regression/cbmc-java/NullPointerException3/Test.java b/regression/cbmc-java/NullPointerException3/Test.java
index 35df442dd61..398d90b0c21 100644
--- a/regression/cbmc-java/NullPointerException3/Test.java
+++ b/regression/cbmc-java/NullPointerException3/Test.java
@@ -9,9 +9,6 @@ public static void main(String args[]) {
         A a=null;
         try {
             int i=a.i;
-            // TODO: an explicit throw is currently needed in order
-            // for CBMC to convert the exception handler
-            throw new B();
         }
         catch (NullPointerException exc) {
             assert false;
diff --git a/regression/cbmc-java/NullPointerException3/test.desc b/regression/cbmc-java/NullPointerException3/test.desc
index ed7e923ae16..e4ad2c5739d 100644
--- a/regression/cbmc-java/NullPointerException3/test.desc
+++ b/regression/cbmc-java/NullPointerException3/test.desc
@@ -3,7 +3,7 @@ Test.class
 --java-throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
-^.*assertion at file Test.java line 17 function.*: FAILURE$
+^.*assertion at file Test.java line 14 function.*: FAILURE$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index 190de5ac702..4ae7c72ed69 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -1046,6 +1046,13 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
 
     if(i_it->statement=="athrow" ||
+       i_it->statement=="putfield" ||
+       i_it->statement=="getfield" ||
+       i_it->statement=="checkcast" ||
+       i_it->statement=="newarray" ||
+       i_it->statement=="anewarray" ||
+       i_it->statement==patternt("?astore") ||
+       i_it->statement==patternt("?aload") ||
        i_it->statement=="invokestatic" ||
        i_it->statement=="invokevirtual" ||
        i_it->statement=="invokespecial" ||