From c1425a3ef056834600f9bc24eb511543fe80db9e Mon Sep 17 00:00:00 2001
From: gtrepta <50716988+gtrepta@users.noreply.github.com>
Date: Mon, 4 Nov 2019 13:27:03 -0600
Subject: [PATCH] Fix useless rule warning (#535)

---
 web3.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/web3.md b/web3.md
index d1d35d3cc9..9937492bb8 100644
--- 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>