diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
index 370350eb969..56bc4f0b65e 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -1749,7 +1749,6 @@ codet java_bytecode_convert_methodt::convert_instructions(
       else
         op=pop(1);
 
-      assert(!stack.empty());
       exprt::operandst op2;
 
       if(get_bytecode_type_width(stack.back().type())==32)