diff --git a/src/Assembly/Symbolic.v b/src/Assembly/Symbolic.v
index f05cee59cb..4ef6244e93 100644
--- a/src/Assembly/Symbolic.v
+++ b/src/Assembly/Symbolic.v
@@ -4202,6 +4202,14 @@ Definition SymexNormalInstruction {opts : symbolic_options_computed_opt} {descr:
   | (mov | movzx | movabs | movdqa | movdqu | movq | movd | movups), [dst; src] => (* Note: unbundle when switching from N to Z *)
     v <- GetOperand src;
     SetOperand dst v
+  | movsx, [dst; src] => (* Move with Sign-Extend *)
+    v <- GetOperand src;
+    src_size <- match standalone_operand_size src with
+                | Some s => ret s
+                | None => err (error.ambiguous_operation_size instr)
+                end;
+    let v := signed src_size v in
+    SetOperand dst v
   | xchg, [a; b] => (* Note: unbundle when switching from N to Z *)
     va <- GetOperand a;
     vb <- GetOperand b;
diff --git a/src/Assembly/WithBedrock/Semantics.v b/src/Assembly/WithBedrock/Semantics.v
index d8029ed8f1..516bcb91f9 100644
--- a/src/Assembly/WithBedrock/Semantics.v
+++ b/src/Assembly/WithBedrock/Semantics.v
@@ -168,6 +168,11 @@ Definition DenoteNormalInstruction (st : machine_state) (instr : NormalInstructi
   | (mov | movzx | movabs | movdqa | movdqu | movq | movd | movups), [dst; src] => (* Note: unbundle when switching from N to Z *)
     v <- DenoteOperand sa s st src;
     SetOperand sa s st dst v
+  | movsx, [dst; src] => (* Move with Sign-Extend *)
+    v <- DenoteOperand sa s st src;
+    src_size <- standalone_operand_size src ;
+    let v := signed src_size v in
+    SetOperand sa s st dst v
   | xchg, [a; b] => (* Flags Affected: None *)
     va <- DenoteOperand sa s st a;
     vb <- DenoteOperand sa s st b;