diff --git a/jbmc/regression/jbmc/temp_stack_variable_packing/External.class b/jbmc/regression/jbmc/temp_stack_variable_packing/External.class
new file mode 100644
index 00000000000..53e556f1c82
Binary files /dev/null and b/jbmc/regression/jbmc/temp_stack_variable_packing/External.class differ
diff --git a/jbmc/regression/jbmc/temp_stack_variable_packing/External.java b/jbmc/regression/jbmc/temp_stack_variable_packing/External.java
new file mode 100644
index 00000000000..6cf8781d39a
--- /dev/null
+++ b/jbmc/regression/jbmc/temp_stack_variable_packing/External.java
@@ -0,0 +1,5 @@
+public class External {
+    public void Accept(int... args) {
+
+    }
+}
diff --git a/jbmc/regression/jbmc/temp_stack_variable_packing/Primary.class b/jbmc/regression/jbmc/temp_stack_variable_packing/Primary.class
new file mode 100644
index 00000000000..868a8139746
Binary files /dev/null and b/jbmc/regression/jbmc/temp_stack_variable_packing/Primary.class differ
diff --git a/jbmc/regression/jbmc/temp_stack_variable_packing/Primary.java b/jbmc/regression/jbmc/temp_stack_variable_packing/Primary.java
new file mode 100644
index 00000000000..e7909fe7c28
--- /dev/null
+++ b/jbmc/regression/jbmc/temp_stack_variable_packing/Primary.java
@@ -0,0 +1,12 @@
+public class Primary {
+    private External ex = new External();
+
+    public void Run() {
+        this.ex.Accept(new int[]{0, 1, 2});
+        assert(false);
+    }
+
+    public void main() {
+        this.Run();
+    }
+}
diff --git a/jbmc/regression/jbmc/temp_stack_variable_packing/test.desc b/jbmc/regression/jbmc/temp_stack_variable_packing/test.desc
new file mode 100644
index 00000000000..19d1488e68e
--- /dev/null
+++ b/jbmc/regression/jbmc/temp_stack_variable_packing/test.desc
@@ -0,0 +1,7 @@
+CORE
+Primary.class
+--function Primary.main
+^\[java::Primary.Run:\(\)V\.assertion\.1\] assertion at file Primary\.java line 6 function java::Primary.Run:\(\)V bytecode-index 22: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
index 9eb8be9f585..a89498d2723 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -3241,7 +3241,8 @@ void java_bytecode_convert_methodt::save_stack_entries(
     }
     if(replace)
     {
-      create_stack_tmp_var(tmp_var_prefix, tmp_var_type, block, stack_entry);
+      create_stack_tmp_var(
+          tmp_var_prefix, stack_entry.type(), block, stack_entry);
     }
   }
 }