From 6466343c621e62ce46847a45b8f18057e559c65a Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Thu, 26 Sep 2024 20:45:42 +0100 Subject: [PATCH] adding lemmas --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 index 4b660d9cba..9cb1706607 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k @@ -46,7 +46,8 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic] // Word Reasoning // ######################## - rule 0 <=Int #sizeWordStack(_) => true [simplification] + rule 0 <=Int #sizeWordStack(_) => true [simplification, smt-lemma] + rule #sizeWordStack(_) false requires N <=Int 0 [simplification, smt-lemma] // #newAddr range rule 0 <=Int #newAddr(_,_) => true [simplification]