diff --git a/src/Assembly/Symbolic.v b/src/Assembly/Symbolic.v
index 5849e9547a..c6f2f1f643 100644
--- a/src/Assembly/Symbolic.v
+++ b/src/Assembly/Symbolic.v
@@ -4386,6 +4386,9 @@ Definition SymexNormalInstruction {opts : symbolic_options_computed_opt} {descr:
        rsp' <- Symeval (s:=stack_addr_size) (add stack_addr_size@(rsp', PreARG ((Z.of_N s/8)%Z)));
        _    <- SetOperand rsp rsp';
                SetOperand dst v
+
+  | nop, [] => ret tt
+
   | _, _ => err (error.unimplemented_instruction instr)
  end
   | Some prefix => err (error.unimplemented_prefix instr) end
diff --git a/src/Assembly/WithBedrock/Semantics.v b/src/Assembly/WithBedrock/Semantics.v
index d8f6ef024e..c96d023b42 100644
--- a/src/Assembly/WithBedrock/Semantics.v
+++ b/src/Assembly/WithBedrock/Semantics.v
@@ -369,6 +369,8 @@ Definition DenoteNormalInstruction (st : machine_state) (instr : NormalInstructi
        st   <- SetOperand stack_addr_size s st rsp rsp';
                SetOperand sa s st dst v
 
+  | nop, [] => Some st
+
   | ret, _ => None (* not sure what to do with this ret, maybe exlude it? *)
 
   | adc, _