diff --git a/decoder.k b/decoder.k
index 6838e660d6550b12547ed32d824b2dedd5315486..d48f61c2726c63dd5d01557db9443f9f08592dba 100644
--- a/decoder.k
+++ b/decoder.k
@@ -512,15 +512,18 @@ module DECODER
        requires I:Int =/=Int 0 // Already saw VEX, bail out.
 
   rule <k> ScanForEVEX => DecoderOutOfBytes ... </k>
+       <VEXVALID> 0 </VEXVALID>
        <decoderBuffer> .Ints </decoderBuffer>
 
   rule <k> ScanForEVEX => . ... </k>
+       <VEXVALID> 0 </VEXVALID>
        <decoderBuffer> I:Int Is:Ints </decoderBuffer>
        requires I:Int =/=Int 98
 
   syntax K ::= "ParseEVEX" | "VerifyNotBound"
 
   rule <k> ScanForEVEX => VerifyNotBound ... </k>
+       <VEXVALID> 0 </VEXVALID>
        <decoderBuffer> 98 Is </decoderBuffer>
 
   rule <k> VerifyNotBound => ParseEVEX ... </k>