1 files changed, 6 insertions, 5 deletions
diff --git a/x86/Asm.v b/x86/Asm.v
index 32235c2d..58e28c40 100644
--- a/x86/Asm.v
+++ b/x86/Asm.v
@@ -851,11 +851,12 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Ptestq_ri r1 n =>
       Next (nextinstr (compare_longs (Val.andl (rs r1) (Vlong n)) (Vlong Int64.zero) rs m)) m
   | Pcmov c rd r1 =>
-      match eval_testcond c rs with
-      | Some true => Next (nextinstr (rs#rd <- (rs#r1))) m
-      | Some false => Next (nextinstr rs) m
-      | None => Next (nextinstr (rs#rd <- Vundef)) m
-      end
+      let v :=
+        match eval_testcond c rs with
+        | Some b => if b then rs#r1 else rs#rd
+        | None   => Vundef
+      end in
+      Next (nextinstr (rs#rd <- v)) m
   | Psetcc c rd =>
       Next (nextinstr (rs#rd <- (Val.of_optbool (eval_testcond c rs)))) m
   (** Arithmetic operations over double-precision floats *)