delete useless lemma comments.

runtimeverification · Jan 24, 2025 · abf5410 · abf5410
1 parent 05a772c
commit abf5410
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 22 deletions.
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k
@@ -47,7 +47,6 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic]
   // ########################
 
     rule N <=Int #sizeWordStack ( _ , N ) => true requires 0 <=Int N [simplification, smt-lemma]
-  //  rule #sizeWordStack ( _ : WS, 0 ) => 1 +Int #sizeWordStack ( WS, 0 ) [simplification, smt-lemma]
 
     // #newAddr range
     rule 0 <=Int #newAddr(_,_)             => true   [simplification]

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/summary-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/summary-simplification.k