diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
index 8e0a1ba9120..a18b05fa78b 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -3184,10 +3184,6 @@ void java_bytecode_convert_methodt::save_stack_entries(
 {
   for(auto &stack_entry : stack)
   {
-    // remove typecasts if existing
-    while(stack_entry.id()==ID_typecast)
-      stack_entry=to_typecast_expr(stack_entry).op();
-
     // variables or static fields and symbol -> save symbols with same id
     if((write_type==bytecode_write_typet::VARIABLE ||
         write_type==bytecode_write_typet::STATIC_FIELD) &&