1 files changed, 1 insertions, 1 deletions
diff --git a/ia32/Asm.v b/ia32/Asm.v
index 9d4036ff..304cb8e4 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -913,7 +913,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       | Vint n =>
           match list_nth_z tbl (Int.unsigned n) with
           | None => Stuck
-          | Some lbl => goto_label f lbl rs m
+          | Some lbl => goto_label f lbl (rs #RAX <- Vundef #RDX <- Vundef) m
           end
       | _ => Stuck
       end