diff --git a/regression/cbmc-java/LocalVarTable5/test.desc b/regression/cbmc-java/LocalVarTable5/test.desc
index bfe77ab09ad..19f3ddab499 100644
--- a/regression/cbmc-java/LocalVarTable5/test.desc
+++ b/regression/cbmc-java/LocalVarTable5/test.desc
@@ -4,7 +4,7 @@ test.class
 dead anonlocal::1i
 dead anonlocal::2i
 dead anonlocal::3a
-dead new_tmp0
+dead new_tmp[0123456789]+
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/cbmc-java/destructor1/test.desc b/regression/cbmc-java/destructor1/test.desc
index 53856821b22..32dea0b83f5 100644
--- a/regression/cbmc-java/destructor1/test.desc
+++ b/regression/cbmc-java/destructor1/test.desc
@@ -5,4 +5,4 @@ Break.class
 ^SIGNAL=0$
 dead i;
 --
-GOTO 10
+GOTO 11
diff --git a/regression/cbmc-java/stack_var1/README b/regression/cbmc-java/stack_var1/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/regression/cbmc-java/stack_var1/README
@@ -0,0 +1,9 @@
+This regression test is created from the .j file with the jasmin assembler.
+https://github.com/Sable/jasmin
+
+On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is
+sufficient to do
+
+> jasmin $FILE.j
+
+and it will create the corresponding $FILE.class file.
diff --git a/regression/cbmc-java/stack_var1/stack_test.class b/regression/cbmc-java/stack_var1/stack_test.class
new file mode 100644
index 00000000000..2b723f49df8
Binary files /dev/null and b/regression/cbmc-java/stack_var1/stack_test.class differ
diff --git a/regression/cbmc-java/stack_var1/stack_test.java b/regression/cbmc-java/stack_var1/stack_test.java
new file mode 100644
index 00000000000..cb404e89473
--- /dev/null
+++ b/regression/cbmc-java/stack_var1/stack_test.java
@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var1 s = new stack_var1();
+    int n = s.f(1);
+    assert(n==0);
+  }
+}
diff --git a/regression/cbmc-java/stack_var1/stack_var1.class b/regression/cbmc-java/stack_var1/stack_var1.class
new file mode 100644
index 00000000000..67a2f733081
Binary files /dev/null and b/regression/cbmc-java/stack_var1/stack_var1.class differ
diff --git a/regression/cbmc-java/stack_var1/stack_var1.j b/regression/cbmc-java/stack_var1/stack_var1.j
new file mode 100644
index 00000000000..a3736df18e2
--- /dev/null
+++ b/regression/cbmc-java/stack_var1/stack_var1.j
@@ -0,0 +1,22 @@
+.class public stack_var1
+.super java/lang/Object
+
+.method public <init>()V
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   return
+.end method
+
+.method public f(I)I
+   .limit stack 2
+   .limit locals 2
+
+   ;; copy of arg on stack
+   iload_1
+   ;; increment arg
+   iinc 1 1
+   ;; incremented copy on stack
+   iload_1
+   isub
+   ireturn
+.end method
diff --git a/regression/cbmc-java/stack_var1/test.desc b/regression/cbmc-java/stack_var1/test.desc
new file mode 100644
index 00000000000..3bf59401a5a
--- /dev/null
+++ b/regression/cbmc-java/stack_var1/test.desc
@@ -0,0 +1,9 @@
+CORE
+stack_test.class
+
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file stack_test.java line 5 function.*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/stack_var2/README b/regression/cbmc-java/stack_var2/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/regression/cbmc-java/stack_var2/README
@@ -0,0 +1,9 @@
+This regression test is created from the .j file with the jasmin assembler.
+https://github.com/Sable/jasmin
+
+On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is
+sufficient to do
+
+> jasmin $FILE.j
+
+and it will create the corresponding $FILE.class file.
diff --git a/regression/cbmc-java/stack_var2/stack_test.class b/regression/cbmc-java/stack_var2/stack_test.class
new file mode 100644
index 00000000000..f26c64d43d4
Binary files /dev/null and b/regression/cbmc-java/stack_var2/stack_test.class differ
diff --git a/regression/cbmc-java/stack_var2/stack_test.java b/regression/cbmc-java/stack_var2/stack_test.java
new file mode 100644
index 00000000000..822716f691c
--- /dev/null
+++ b/regression/cbmc-java/stack_var2/stack_test.java
@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var2 s = new stack_var2();
+    int n = s.f(1);
+    assert(n==0);
+  }
+}
diff --git a/regression/cbmc-java/stack_var2/stack_var2.class b/regression/cbmc-java/stack_var2/stack_var2.class
new file mode 100644
index 00000000000..6db13604864
Binary files /dev/null and b/regression/cbmc-java/stack_var2/stack_var2.class differ
diff --git a/regression/cbmc-java/stack_var2/stack_var2.j b/regression/cbmc-java/stack_var2/stack_var2.j
new file mode 100644
index 00000000000..e20a174070c
--- /dev/null
+++ b/regression/cbmc-java/stack_var2/stack_var2.j
@@ -0,0 +1,25 @@
+.class public stack_var2
+.super java/lang/Object
+
+.method public <init>()V
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   return
+.end method
+
+.method public f(I)I
+   .limit stack 3
+   .limit locals 2
+
+   ;; push local var1
+   iload_1
+   ;; duplicate
+   dup
+   ;; increment local var1
+   iinc 1 1
+   ;; push local var1
+   iload_1
+   isub
+   ;; incremented copy on stack
+   ireturn
+.end method
diff --git a/regression/cbmc-java/stack_var2/test.desc b/regression/cbmc-java/stack_var2/test.desc
new file mode 100644
index 00000000000..3bf59401a5a
--- /dev/null
+++ b/regression/cbmc-java/stack_var2/test.desc
@@ -0,0 +1,9 @@
+CORE
+stack_test.class
+
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file stack_test.java line 5 function.*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/stack_var3/README b/regression/cbmc-java/stack_var3/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/regression/cbmc-java/stack_var3/README
@@ -0,0 +1,9 @@
+This regression test is created from the .j file with the jasmin assembler.
+https://github.com/Sable/jasmin
+
+On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is
+sufficient to do
+
+> jasmin $FILE.j
+
+and it will create the corresponding $FILE.class file.
diff --git a/regression/cbmc-java/stack_var3/stack_test.class b/regression/cbmc-java/stack_var3/stack_test.class
new file mode 100644
index 00000000000..a42cc9101a1
Binary files /dev/null and b/regression/cbmc-java/stack_var3/stack_test.class differ
diff --git a/regression/cbmc-java/stack_var3/stack_test.java b/regression/cbmc-java/stack_var3/stack_test.java
new file mode 100644
index 00000000000..7ffc016070c
--- /dev/null
+++ b/regression/cbmc-java/stack_var3/stack_test.java
@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var3 s = new stack_var3();
+    int n = s.f();
+    assert(n==0);
+  }
+}
diff --git a/regression/cbmc-java/stack_var3/stack_var3.class b/regression/cbmc-java/stack_var3/stack_var3.class
new file mode 100644
index 00000000000..9a3a0d6d370
Binary files /dev/null and b/regression/cbmc-java/stack_var3/stack_var3.class differ
diff --git a/regression/cbmc-java/stack_var3/stack_var3.j b/regression/cbmc-java/stack_var3/stack_var3.j
new file mode 100644
index 00000000000..f215d15b4bc
--- /dev/null
+++ b/regression/cbmc-java/stack_var3/stack_var3.j
@@ -0,0 +1,33 @@
+.class public stack_var3
+.super java/lang/Object
+
+.method public <init>()V
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   return
+.end method
+
+.method public f()I
+   .limit stack 5
+   .limit locals 3
+
+   ;; 1->var1
+   ;; 0->var2
+   iconst_1
+   istore_1
+   iconst_0
+   istore_2
+   ;; push local var2 / var1
+   iload_2
+   iload_1
+   ;; dup var1
+   dup_x1
+   ;; sub one from var1
+   iinc 1 -1
+   ;; pop first var1
+   pop
+   ;; sub
+   isub
+   ;; incremented copy on stack
+   ireturn
+.end method
diff --git a/regression/cbmc-java/stack_var3/test.desc b/regression/cbmc-java/stack_var3/test.desc
new file mode 100644
index 00000000000..3bf59401a5a
--- /dev/null
+++ b/regression/cbmc-java/stack_var3/test.desc
@@ -0,0 +1,9 @@
+CORE
+stack_test.class
+
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file stack_test.java line 5 function.*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/stack_var4/README b/regression/cbmc-java/stack_var4/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/regression/cbmc-java/stack_var4/README
@@ -0,0 +1,9 @@
+This regression test is created from the .j file with the jasmin assembler.
+https://github.com/Sable/jasmin
+
+On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is
+sufficient to do
+
+> jasmin $FILE.j
+
+and it will create the corresponding $FILE.class file.
diff --git a/regression/cbmc-java/stack_var4/stack_test.class b/regression/cbmc-java/stack_var4/stack_test.class
new file mode 100644
index 00000000000..cfbb80f78e8
Binary files /dev/null and b/regression/cbmc-java/stack_var4/stack_test.class differ
diff --git a/regression/cbmc-java/stack_var4/stack_test.java b/regression/cbmc-java/stack_var4/stack_test.java
new file mode 100644
index 00000000000..1088dd5ac2e
--- /dev/null
+++ b/regression/cbmc-java/stack_var4/stack_test.java
@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var4 s = new stack_var4();
+    int n = s.f();
+    assert(n==0);
+  }
+}
diff --git a/regression/cbmc-java/stack_var4/stack_var4.class b/regression/cbmc-java/stack_var4/stack_var4.class
new file mode 100644
index 00000000000..782443dd6e3
Binary files /dev/null and b/regression/cbmc-java/stack_var4/stack_var4.class differ
diff --git a/regression/cbmc-java/stack_var4/stack_var4.j b/regression/cbmc-java/stack_var4/stack_var4.j
new file mode 100644
index 00000000000..99eecf3794a
--- /dev/null
+++ b/regression/cbmc-java/stack_var4/stack_var4.j
@@ -0,0 +1,37 @@
+.class public stack_var4
+.super java/lang/Object
+
+.method public <init>()V
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   return
+.end method
+
+.method public f()I
+   .limit stack 5
+   .limit locals 4
+
+   ;; 0->var1
+   ;; 1->var2
+   ;; 2->var3
+   iconst_0
+   istore_1
+   iconst_1
+   istore_2
+   iconst_2
+   istore_3
+
+   ;; push local var3 / var2 / var1
+   iload_3
+   iload_2
+   iload_1
+   ;; push var1 in front of var3
+   dup_x2
+   ;; add one to local var 1
+   iinc 1 1
+   pop
+   pop
+   pop
+   ;; incremented copy on stack
+   ireturn
+.end method
diff --git a/regression/cbmc-java/stack_var4/test.desc b/regression/cbmc-java/stack_var4/test.desc
new file mode 100644
index 00000000000..805e44acccd
--- /dev/null
+++ b/regression/cbmc-java/stack_var4/test.desc
@@ -0,0 +1,10 @@
+CORE
+stack_test.class
+
+^EXIT=0$
+^SIGNAL=0$
+^.*assertion at file stack_test.java line 5 function.*: SUCCESS
+$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/stack_var5/README b/regression/cbmc-java/stack_var5/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/regression/cbmc-java/stack_var5/README
@@ -0,0 +1,9 @@
+This regression test is created from the .j file with the jasmin assembler.
+https://github.com/Sable/jasmin
+
+On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is
+sufficient to do
+
+> jasmin $FILE.j
+
+and it will create the corresponding $FILE.class file.
diff --git a/regression/cbmc-java/stack_var5/stack_test.class b/regression/cbmc-java/stack_var5/stack_test.class
new file mode 100644
index 00000000000..57cf43dac86
Binary files /dev/null and b/regression/cbmc-java/stack_var5/stack_test.class differ
diff --git a/regression/cbmc-java/stack_var5/stack_test.java b/regression/cbmc-java/stack_var5/stack_test.java
new file mode 100644
index 00000000000..bfcbe79325d
--- /dev/null
+++ b/regression/cbmc-java/stack_var5/stack_test.java
@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var5 s = new stack_var5();
+    int n = s.f();
+    assert(n==1);
+  }
+}
diff --git a/regression/cbmc-java/stack_var5/stack_var5.class b/regression/cbmc-java/stack_var5/stack_var5.class
new file mode 100644
index 00000000000..6230e78a9c7
Binary files /dev/null and b/regression/cbmc-java/stack_var5/stack_var5.class differ
diff --git a/regression/cbmc-java/stack_var5/stack_var5.j b/regression/cbmc-java/stack_var5/stack_var5.j
new file mode 100644
index 00000000000..0871fb68e0b
--- /dev/null
+++ b/regression/cbmc-java/stack_var5/stack_var5.j
@@ -0,0 +1,33 @@
+.class public stack_var5
+.super java/lang/Object
+
+.method public <init>()V
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   return
+.end method
+
+.method public f()I
+   .limit stack 4
+   .limit locals 4
+
+   ;; 1->var1
+   ;; 2->var2
+   iconst_1
+   istore_1
+   iconst_2
+   istore_2
+
+   ;; push local var2 / var1
+   iload_2
+   iload_1
+
+   ;; duplicate var2 / var1
+   dup2
+   ;; add one to local var 1
+   iinc 1 1
+   ;; sub
+   isub
+   ;; incremented copy on stack
+   ireturn
+.end method
diff --git a/regression/cbmc-java/stack_var5/test.desc b/regression/cbmc-java/stack_var5/test.desc
new file mode 100644
index 00000000000..805e44acccd
--- /dev/null
+++ b/regression/cbmc-java/stack_var5/test.desc
@@ -0,0 +1,10 @@
+CORE
+stack_test.class
+
+^EXIT=0$
+^SIGNAL=0$
+^.*assertion at file stack_test.java line 5 function.*: SUCCESS
+$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/stack_var6/README b/regression/cbmc-java/stack_var6/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/regression/cbmc-java/stack_var6/README
@@ -0,0 +1,9 @@
+This regression test is created from the .j file with the jasmin assembler.
+https://github.com/Sable/jasmin
+
+On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is
+sufficient to do
+
+> jasmin $FILE.j
+
+and it will create the corresponding $FILE.class file.
diff --git a/regression/cbmc-java/stack_var6/stack_test.class b/regression/cbmc-java/stack_var6/stack_test.class
new file mode 100644
index 00000000000..c5e765b667b
Binary files /dev/null and b/regression/cbmc-java/stack_var6/stack_test.class differ
diff --git a/regression/cbmc-java/stack_var6/stack_test.java b/regression/cbmc-java/stack_var6/stack_test.java
new file mode 100644
index 00000000000..392d200d370
--- /dev/null
+++ b/regression/cbmc-java/stack_var6/stack_test.java
@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var6 s = new stack_var6();
+    int n = s.f(1,2,4);
+    assert(n==-2);
+  }
+}
diff --git a/regression/cbmc-java/stack_var6/stack_var6.class b/regression/cbmc-java/stack_var6/stack_var6.class
new file mode 100644
index 00000000000..05223a9a349
Binary files /dev/null and b/regression/cbmc-java/stack_var6/stack_var6.class differ
diff --git a/regression/cbmc-java/stack_var6/stack_var6.j b/regression/cbmc-java/stack_var6/stack_var6.j
new file mode 100644
index 00000000000..19108f70e36
--- /dev/null
+++ b/regression/cbmc-java/stack_var6/stack_var6.j
@@ -0,0 +1,25 @@
+.class public stack_var6
+.super java/lang/Object
+
+.method public <init>()V
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   return
+.end method
+
+.method public f(III)I
+   .limit stack 8
+   .limit locals 5
+
+   ;; push local var3 / var2 / var1
+   iload_1
+   iload_2
+   iload_3
+   dup2_x1
+   ;; add one to local var 2
+   iinc 2 1
+   ;; sub
+   isub
+   ;; incremented copy on stack
+   ireturn
+.end method
diff --git a/regression/cbmc-java/stack_var6/test.desc b/regression/cbmc-java/stack_var6/test.desc
new file mode 100644
index 00000000000..805e44acccd
--- /dev/null
+++ b/regression/cbmc-java/stack_var6/test.desc
@@ -0,0 +1,10 @@
+CORE
+stack_test.class
+
+^EXIT=0$
+^SIGNAL=0$
+^.*assertion at file stack_test.java line 5 function.*: SUCCESS
+$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/stack_var7/README b/regression/cbmc-java/stack_var7/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/regression/cbmc-java/stack_var7/README
@@ -0,0 +1,9 @@
+This regression test is created from the .j file with the jasmin assembler.
+https://github.com/Sable/jasmin
+
+On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is
+sufficient to do
+
+> jasmin $FILE.j
+
+and it will create the corresponding $FILE.class file.
diff --git a/regression/cbmc-java/stack_var7/stack_test.class b/regression/cbmc-java/stack_var7/stack_test.class
new file mode 100644
index 00000000000..21eabe9a029
Binary files /dev/null and b/regression/cbmc-java/stack_var7/stack_test.class differ
diff --git a/regression/cbmc-java/stack_var7/stack_test.java b/regression/cbmc-java/stack_var7/stack_test.java
new file mode 100644
index 00000000000..b742878507e
--- /dev/null
+++ b/regression/cbmc-java/stack_var7/stack_test.java
@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var7 s = new stack_var7();
+    int n = s.f();
+    assert(n==1);
+  }
+}
diff --git a/regression/cbmc-java/stack_var7/stack_var7.class b/regression/cbmc-java/stack_var7/stack_var7.class
new file mode 100644
index 00000000000..dcc6f0fc1b6
Binary files /dev/null and b/regression/cbmc-java/stack_var7/stack_var7.class differ
diff --git a/regression/cbmc-java/stack_var7/stack_var7.j b/regression/cbmc-java/stack_var7/stack_var7.j
new file mode 100644
index 00000000000..e75f96b833d
--- /dev/null
+++ b/regression/cbmc-java/stack_var7/stack_var7.j
@@ -0,0 +1,43 @@
+.class public stack_var7
+.super java/lang/Object
+
+.method public <init>()V
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   return
+.end method
+
+.method public f()I
+   .limit stack 8
+   .limit locals 5
+
+   ;; 1->var1
+   ;; 2->var2
+   ;; 4->var3
+   ;; 8->var4
+   iconst_1
+   istore_1
+   iconst_2
+   istore_2
+   iconst_4
+   istore_3
+   bipush 8
+   istore 4
+   ;; push local var4 / var3 / var2 / var1
+   iload 4
+   iload_3
+   iload_2
+   iload 1
+   ;; push var2 / var1 in on head
+   dup2_x2
+   ;; add one to local var 1
+   iinc 1 1
+   pop
+   pop
+   pop
+   pop
+   ;; sub
+   isub
+   ;; incremented copy on stack
+   ireturn
+.end method
diff --git a/regression/cbmc-java/stack_var7/test.desc b/regression/cbmc-java/stack_var7/test.desc
new file mode 100644
index 00000000000..805e44acccd
--- /dev/null
+++ b/regression/cbmc-java/stack_var7/test.desc
@@ -0,0 +1,10 @@
+CORE
+stack_test.class
+
+^EXIT=0$
+^SIGNAL=0$
+^.*assertion at file stack_test.java line 5 function.*: SUCCESS
+$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/stack_var8/README b/regression/cbmc-java/stack_var8/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/regression/cbmc-java/stack_var8/README
@@ -0,0 +1,9 @@
+This regression test is created from the .j file with the jasmin assembler.
+https://github.com/Sable/jasmin
+
+On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is
+sufficient to do
+
+> jasmin $FILE.j
+
+and it will create the corresponding $FILE.class file.
diff --git a/regression/cbmc-java/stack_var8/stack_test.class b/regression/cbmc-java/stack_var8/stack_test.class
new file mode 100644
index 00000000000..8ea61591cbc
Binary files /dev/null and b/regression/cbmc-java/stack_var8/stack_test.class differ
diff --git a/regression/cbmc-java/stack_var8/stack_test.java b/regression/cbmc-java/stack_var8/stack_test.java
new file mode 100644
index 00000000000..3a288890e69
--- /dev/null
+++ b/regression/cbmc-java/stack_var8/stack_test.java
@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var8 s = new stack_var8();
+    int n = s.f();
+    assert(n==0);
+  }
+}
diff --git a/regression/cbmc-java/stack_var8/stack_var8.class b/regression/cbmc-java/stack_var8/stack_var8.class
new file mode 100644
index 00000000000..5298a7d8c92
Binary files /dev/null and b/regression/cbmc-java/stack_var8/stack_var8.class differ
diff --git a/regression/cbmc-java/stack_var8/stack_var8.j b/regression/cbmc-java/stack_var8/stack_var8.j
new file mode 100644
index 00000000000..d5bec33279d
--- /dev/null
+++ b/regression/cbmc-java/stack_var8/stack_var8.j
@@ -0,0 +1,27 @@
+.class public stack_var8
+.super java/lang/Object
+
+.field private n I
+
+.method public <init>()V
+.limit stack 5
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   aload_0
+   iconst_0
+   putfield stack_var8/n I
+   return
+.end method
+
+.method public f()I
+   .limit stack 8
+   .limit locals 5
+
+   aload_0
+   getfield stack_var8/n I
+   aload_0
+   iconst_1
+   putfield stack_var8/n I
+
+   ireturn
+.end method
diff --git a/regression/cbmc-java/stack_var9/README b/regression/cbmc-java/stack_var9/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/regression/cbmc-java/stack_var9/README
@@ -0,0 +1,9 @@
+This regression test is created from the .j file with the jasmin assembler.
+https://github.com/Sable/jasmin
+
+On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is
+sufficient to do
+
+> jasmin $FILE.j
+
+and it will create the corresponding $FILE.class file.
diff --git a/regression/cbmc-java/stack_var9/stack_test.class b/regression/cbmc-java/stack_var9/stack_test.class
new file mode 100644
index 00000000000..4f20f14f7d1
Binary files /dev/null and b/regression/cbmc-java/stack_var9/stack_test.class differ
diff --git a/regression/cbmc-java/stack_var9/stack_test.java b/regression/cbmc-java/stack_var9/stack_test.java
new file mode 100644
index 00000000000..994e7974026
--- /dev/null
+++ b/regression/cbmc-java/stack_var9/stack_test.java
@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var9 s = new stack_var9();
+    int n = s.f();
+    assert(n==0);
+  }
+}
diff --git a/regression/cbmc-java/stack_var9/stack_var9.class b/regression/cbmc-java/stack_var9/stack_var9.class
new file mode 100644
index 00000000000..1fa90019a0e
Binary files /dev/null and b/regression/cbmc-java/stack_var9/stack_var9.class differ
diff --git a/regression/cbmc-java/stack_var9/stack_var9.j b/regression/cbmc-java/stack_var9/stack_var9.j
new file mode 100644
index 00000000000..aeee091def0
--- /dev/null
+++ b/regression/cbmc-java/stack_var9/stack_var9.j
@@ -0,0 +1,24 @@
+.class public stack_var9
+.super java/lang/Object
+
+.field private static n I
+
+.method public <init>()V
+.limit stack 5
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   iconst_0
+   putstatic stack_var9/n I
+   return
+.end method
+
+.method public f()I
+   .limit stack 8
+   .limit locals 5
+
+   getstatic stack_var9/n I
+   iconst_1
+   putstatic stack_var9/n I
+
+   ireturn
+.end method
diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index 43a2ded0af1..e49ba0264c7 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -1363,15 +1363,26 @@ codet java_bytecode_convert_methodt::convert_instructions(
       typet element_type=data_ptr.type().subtype();
       dereference_exprt element(data_plus_offset, element_type);
 
-      c=get_array_bounds_check(deref, op[1], i_it->source_location);
+      const exprt tmp_var=tmp_variable("stack_array_elem", element_type);
+      c=code_blockt();
+      c.copy_to_operands(
+        get_array_bounds_check(deref, op[1], i_it->source_location));
+      c.copy_to_operands(
+        code_assignt(tmp_var, java_bytecode_promotion(element)));
       c.add_source_location()=i_it->source_location;
-      results[0]=java_bytecode_promotion(element);
+      results[0]=tmp_var;
     }
     else if(statement==patternt("?load"))
     {
-      // load a value from a local variable
-      results[0]=
-        variable(arg0, statement[0], i_it->address, CAST_AS_NEEDED);
+      const char char_type=statement[0];
+      const typet t=java_bytecode_promotion(java_type_from_char(char_type));
+
+      // create new stack variable to hold the value of the local variable
+      const exprt tmp_var=tmp_variable("stack_var", t);
+      c=code_assignt(
+        tmp_var,
+        variable(arg0, statement[0], i_it->address, CAST_AS_NEEDED));
+      results[0]=tmp_var;
     }
     else if(statement=="ldc" || statement=="ldc_w" ||
             statement=="ldc2" || statement=="ldc2_w")
@@ -1731,19 +1742,49 @@ codet java_bytecode_convert_methodt::convert_instructions(
     else if(statement=="dup")
     {
       assert(op.size()==1 && results.size()==2);
-      results[0]=results[1]=op[0];
+      if(op[0].id()!=ID_constant)
+      {
+        // create new stack variable
+        const exprt tmp_var=
+          tmp_variable("stack_dup", op[0].type());
+        c=code_assignt(tmp_var, java_bytecode_promotion(op[0]));
+        results[0]=tmp_var;
+      }
+      else
+        results[0]=op[0];
+      results[1]=op[0];
     }
     else if(statement=="dup_x1")
     {
       assert(op.size()==2 && results.size()==3);
-      results[0]=op[1];
+      if(op[1].id()!=ID_constant)
+      {
+        // create new stack variable
+        const exprt tmp_var=
+          tmp_variable("stack_dup_x1", op[1].type());
+        c=code_assignt(tmp_var, java_bytecode_promotion(op[1]));
+        // op1 is value1, op0 is value2
+        results[0]=tmp_var;
+      }
+      else
+        results[0]=op[1];
       results[1]=op[0];
       results[2]=op[1];
     }
     else if(statement=="dup_x2")
     {
       assert(op.size()==3 && results.size()==4);
-      results[0]=op[2];
+      if(op[2].id()!=ID_constant)
+      {
+        // create new stack variable
+        const exprt tmp_var=
+          tmp_variable("stack_dup_x2", op[2].type());
+        c=code_assignt(tmp_var, java_bytecode_promotion(op[2]));
+        // op2 is value1, op1 is value2, op0 is value3
+        results[0]=tmp_var;
+      }
+      else
+        results[0]=op[2];
       results[1]=op[0];
       results[2]=op[1];
       results[3]=op[2];
@@ -1755,23 +1796,64 @@ codet java_bytecode_convert_methodt::convert_instructions(
       assert(!stack.empty() && results.empty());
 
       if(get_bytecode_type_width(stack.back().type())==32)
-        op=pop(2);
+      {
+        op=pop(2); // op0 is value1 op1 is value2
+        const exprt tmp_var1=
+          tmp_variable("stack_dup2_1", op[0].type());
+        const exprt tmp_var2=
+          tmp_variable("stack_dup2_2", op[1].type());
+        c=code_blockt();
+        c.copy_to_operands(
+          code_assignt(tmp_var1, java_bytecode_promotion(op[0])));
+        c.copy_to_operands(
+          code_assignt(tmp_var2, java_bytecode_promotion(op[1])));
+        results.push_back(tmp_var1);
+        results.push_back(tmp_var2);
+      }
       else
+      {
         op=pop(1);
+        const exprt tmp_var=
+          tmp_variable("stack_dup2", op[0].type());
+        c=code_assignt(tmp_var, java_bytecode_promotion(op[0]));
+        results.push_back(tmp_var);
+      }
 
       results.insert(results.end(), op.begin(), op.end());
-      results.insert(results.end(), op.begin(), op.end());
     }
     else if(statement=="dup2_x1")
     {
       assert(!stack.empty() && results.empty());
 
       if(get_bytecode_type_width(stack.back().type())==32)
+      {
         op=pop(3);
+        const exprt tmp_var1=
+          tmp_variable("stack_dup2_x1_1", op[2].type());
+        const exprt tmp_var2=
+          tmp_variable("stack_dup2_x1_2", op[1].type());
+        c=code_blockt();
+        c.copy_to_operands(
+          code_assignt(tmp_var1, java_bytecode_promotion(op[2])));
+        c.copy_to_operands(
+          code_assignt(tmp_var2, java_bytecode_promotion(op[1])));
+        results.push_back(tmp_var2);
+        results.push_back(tmp_var1);
+        c=code_blockt();
+        c.copy_to_operands(
+          code_assignt(tmp_var1, java_bytecode_promotion(op[2])));
+        c.copy_to_operands(
+          code_assignt(tmp_var2, java_bytecode_promotion(op[1])));
+      }
       else
+      {
         op=pop(2);
+        const exprt tmp_var=
+          tmp_variable("stack_dup2_x1", op[1].type());
+        results.push_back(tmp_var);
+        c=code_assignt(tmp_var, java_bytecode_promotion(op[1]));
+      }
 
-      results.insert(results.end(), op.begin()+1, op.end());
       results.insert(results.end(), op.begin(), op.end());
     }
     else if(statement=="dup2_x2")
@@ -1779,9 +1861,33 @@ codet java_bytecode_convert_methodt::convert_instructions(
       assert(!stack.empty() && results.empty());
 
       if(get_bytecode_type_width(stack.back().type())==32)
+      {
         op=pop(2);
+        const exprt tmp_var1=
+          tmp_variable("stack_dup2_x2_1", op[1].type());
+        const exprt tmp_var2=
+          tmp_variable("stack_dup2_x2_2", op[0].type());
+        c=code_blockt();
+        c.copy_to_operands(
+          code_assignt(tmp_var1, java_bytecode_promotion(op[1])));
+        c.copy_to_operands(
+          code_assignt(tmp_var2, java_bytecode_promotion(op[0])));
+        results.push_back(tmp_var2);
+        results.push_back(tmp_var1);
+        c=code_blockt();
+        c.copy_to_operands(
+          code_assignt(tmp_var1, java_bytecode_promotion(op[1])));
+        c.copy_to_operands(
+          code_assignt(tmp_var2, java_bytecode_promotion(op[0])));
+      }
       else
+      {
         op=pop(1);
+        const exprt tmp_var=
+          tmp_variable("stack_dup2_x2", op[0].type());
+        c=code_assignt(tmp_var, java_bytecode_promotion(op[0]));
+        results.push_back(tmp_var);
+      }
 
       assert(!stack.empty());
       exprt::operandst op2;
@@ -1806,7 +1912,11 @@ codet java_bytecode_convert_methodt::convert_instructions(
     else if(statement=="getfield")
     {
       assert(op.size()==1 && results.size()==1);
-      results[0]=java_bytecode_promotion(to_member(op[0], arg0));
+      // create a new stack variable to hold the value of the field
+      const exprt tmp_var=
+        tmp_variable("stack_field", java_bytecode_promotion(arg0.type()));
+      c=code_assignt(tmp_var, java_bytecode_promotion(to_member(op[0], arg0)));
+      results[0]=tmp_var;
     }
     else if(statement=="getstatic")
     {
@@ -1819,11 +1929,21 @@ codet java_bytecode_convert_methodt::convert_instructions(
         lazy_methods->add_needed_class(
           to_symbol_type(arg0.type()).get_identifier());
       }
-      results[0]=java_bytecode_promotion(symbol_expr);
-
       // set $assertionDisabled to false
       if(field_name.find("$assertionsDisabled")!=std::string::npos)
+      {
         c=code_assignt(symbol_expr, false_exprt());
+        results[0]=java_bytecode_promotion(symbol_expr);
+      }
+      else
+      {
+        // create a new stack variable to hold the value of the field
+        const exprt tmp_var=tmp_variable(
+          "stack_static_field",
+          java_bytecode_promotion(arg0.type()));
+        c=code_assignt(tmp_var, symbol_expr);
+        results[0]=java_bytecode_promotion(tmp_var);
+      }
     }
     else if(statement=="putfield")
     {