diff --git a/src/Assembly/Symbolic.v b/src/Assembly/Symbolic.v
index 5849e9547a..2e55f5237d 100644
--- a/src/Assembly/Symbolic.v
+++ b/src/Assembly/Symbolic.v
@@ -4199,7 +4199,7 @@ Definition SymexNormalInstruction {opts : symbolic_options_computed_opt} {descr:
   let s : OperationSize := s in
   let resize_reg r := some_or (fun _ => reg_of_index_and_shift_and_bitcount_opt (reg_index r, 0%N (* offset *), s)) (fun _ => error.unimplemented_instruction instr) in
   match instr.(Syntax.op), instr.(args) with
-  | (mov | movzx), [dst; src] => (* Note: unbundle when switching from N to Z *)
+  | (mov | movzx | movabs), [dst; src] => (* Note: unbundle when switching from N to Z *)
     v <- GetOperand src;
     SetOperand dst v
   | xchg, [a; b] => (* Note: unbundle when switching from N to Z *)
diff --git a/src/Assembly/WithBedrock/Semantics.v b/src/Assembly/WithBedrock/Semantics.v
index d8f6ef024e..1bd86c4f55 100644
--- a/src/Assembly/WithBedrock/Semantics.v
+++ b/src/Assembly/WithBedrock/Semantics.v
@@ -165,7 +165,7 @@ Definition DenoteNormalInstruction (st : machine_state) (instr : NormalInstructi
   let resize_reg r := reg_of_index_and_shift_and_bitcount_opt (reg_index r, 0%N (* offset *), s) in
   match instr.(prefix) with None =>
   match instr.(op), instr.(args) with
-  | (mov | movzx), [dst; src] => (* Note: unbundle when switching from N to Z *)
+  | (mov | movzx | movabs), [dst; src] => (* Note: unbundle when switching from N to Z *)
     v <- DenoteOperand sa s st src;
     SetOperand sa s st dst v
   | xchg, [a; b] => (* Flags Affected: None *)