Fix useless rule warning (#535)

runtimeverification · Nov 4, 2019 · c1425a3 · c1425a3
1 parent b304508
commit c1425a3
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/web3.md b/web3.md
@@ -1043,7 +1043,9 @@ Transaction Receipts
     syntax KItem ::= "#eth_estimateGas_finalize" Int
  // ------------------------------------------------
     rule <k> #eth_estimateGas_finalize INITGUSED:Int => #popNetworkState ~> #sendResponse ("result": #unparseQuantity( GUSED -Int INITGUSED )) ... </k>
+         <statusCode> STATUSCODE </statusCode>
          <gasUsed> GUSED </gasUsed>
+      requires STATUSCODE =/=K EVMC_OUT_OF_GAS
 
     rule <k> #eth_estimateGas_finalize _ => #popNetworkState ~> #sendResponse ( "error": {"code": -32000, "message":"base fee exceeds gas limit"}) ... </k>
          <statusCode> EVMC_OUT_OF_GAS </statusCode>