fix booster aborting early

runtimeverification · Mar 28, 2024 · f90ec4b · f90ec4b
1 parent e29cf52
commit f90ec4b
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
@@ -477,11 +477,11 @@ We make sure the given arguments (to be interpreted as addresses) are with 160 b
  // --------------------------------------------
     rule <k> #addr [ OP:OpCode ] => .K ... </k>
          <wordStack> WS => WS [ 0 <- #addr({WS [ 0 ]}:>Int) ] </wordStack>
-      requires isAddr1Op(OP)
+      requires isAddr1Op(OP) [preserves-definedness]
 
     rule <k> #addr [ OP:OpCode ] => .K ... </k>
          <wordStack> WS => WS [ 1 <- #addr({WS [ 1 ]}:>Int) ] </wordStack>
-      requires isAddr2Op(OP)
+      requires isAddr2Op(OP) [preserves-definedness]
 
     rule <k> #addr [ OP:OpCode ] => .K ... </k>
       requires notBool ( isAddr1Op(OP) orBool isAddr2Op(OP) )