diff --git a/regression/cbmc-java/integer_without_simplify1/test.class b/regression/cbmc-java/integer_without_simplify1/test.class
new file mode 100644
index 00000000000..1ee5d36d95a
Binary files /dev/null and b/regression/cbmc-java/integer_without_simplify1/test.class differ
diff --git a/regression/cbmc-java/integer_without_simplify1/test.desc b/regression/cbmc-java/integer_without_simplify1/test.desc
new file mode 100644
index 00000000000..284277c7b4a
--- /dev/null
+++ b/regression/cbmc-java/integer_without_simplify1/test.desc
@@ -0,0 +1,7 @@
+CORE
+test.class
+--no-simplify --function test.f --cover location
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/integer_without_simplify1/test.java b/regression/cbmc-java/integer_without_simplify1/test.java
new file mode 100644
index 00000000000..62b2060b7c0
--- /dev/null
+++ b/regression/cbmc-java/integer_without_simplify1/test.java
@@ -0,0 +1,10 @@
+
+public class test {
+
+  public void f() {
+
+    int x = 50;
+
+  }
+
+}
diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index f9f75e45dbe..95bb864fa12 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/prefix.h>
 #include <util/arith_tools.h>
 #include <util/ieee_float.h>
+#include <util/simplify_expr.h>
 
 #include <linking/zero_initializer.h>
 
@@ -1416,7 +1417,10 @@ codet java_bytecode_convert_methodt::convert_instructions(
     else if(statement==patternt("?ipush"))
     {
       assert(results.size()==1);
-      results[0]=typecast_exprt(arg0, java_int_type());
+      mp_integer int_value;
+      bool ret=to_integer(to_constant_expr(arg0), int_value);
+      INVARIANT(!ret, "?ipush argument should be an integer");
+      results[0]=from_integer(int_value, java_int_type());
     }
     else if(statement==patternt("if_?cmp??"))
     {