diff --git a/regression/cbmc-java/divide_by_zero/DivideByZero.class b/regression/cbmc-java/divide_by_zero/DivideByZero.class
new file mode 100644
index 00000000000..04eeb36fc8f
Binary files /dev/null and b/regression/cbmc-java/divide_by_zero/DivideByZero.class differ
diff --git a/regression/cbmc-java/divide_by_zero/DivideByZero.java b/regression/cbmc-java/divide_by_zero/DivideByZero.java
new file mode 100644
index 00000000000..816be580ab9
--- /dev/null
+++ b/regression/cbmc-java/divide_by_zero/DivideByZero.java
@@ -0,0 +1,6 @@
+public class DivideByZero {
+    public static void main(String args[]) {
+        int i=0;
+        int j=10/i;
+    }
+}
diff --git a/regression/cbmc-java/divide_by_zero/test.desc b/regression/cbmc-java/divide_by_zero/test.desc
new file mode 100644
index 00000000000..8b37d5b8064
--- /dev/null
+++ b/regression/cbmc-java/divide_by_zero/test.desc
@@ -0,0 +1,9 @@
+CORE
+DivideByZero.class
+
+^EXIT=10$
+^SIGNAL=0$
+Denominator should be nonzero: FAILURE
+^VERIFICATION FAILED
+--
+^warning: ignoring
diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp
index 66f62e6ff78..909b839d8be 100644
--- a/src/java_bytecode/java_bytecode_instrument.cpp
+++ b/src/java_bytecode/java_bytecode_instrument.cpp
@@ -143,7 +143,7 @@ codet java_bytecode_instrumentt::throw_exception(
 /// flag is set.
 /// \return Based on the value of the flag `throw_runtime_exceptions`,
 /// it returns code that either throws an ArithmeticException
-/// or is a skip
+/// or asserts a nonzero denominator.
 codet java_bytecode_instrumentt::check_arithmetic_exception(
   const exprt &denominator,
   const source_locationt &original_loc)
@@ -157,7 +157,11 @@ codet java_bytecode_instrumentt::check_arithmetic_exception(
       original_loc,
       "java.lang.ArithmeticException");
 
-  return code_skipt();
+  code_assertt ret(binary_relation_exprt(denominator, ID_notequal, zero));
+  ret.add_source_location()=original_loc;
+  ret.add_source_location().set_comment("Denominator should be nonzero");
+  ret.add_source_location().set_property_class("integer-divide-by-zero");
+  return ret;
 }
 
 /// Checks whether the array access array_struct[idx] is out-of-bounds,