From 0569bfda4534c7ea4c494d1fb88dd6be12ef43c2 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Mon, 4 Sep 2023 14:29:50 +0200 Subject: [PATCH] fix inconsistent use of the '_:_WS' klabel --- kevm-pyk/src/kevm_pyk/kevm.py | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index e806c4ed64..4a0a158eb7 100644 --- a/kevm-pyk/src/kevm_pyk/kevm.py +++ b/kevm-pyk/src/kevm_pyk/kevm.py @@ -168,7 +168,6 @@ def _kevm_patch_symbol_table(cls, symbol_table: SymbolTable) -> None: '_|->_', '#And', '_andBool_', - '_:__EVM-TYPES_WordStack_Int_WordStack', '#Implies', '_impliesBool_', '_&Int_', @@ -214,7 +213,7 @@ def add_invariant(cterm: CTerm) -> CTerm: constraints = [] word_stack = cterm.cell('WORDSTACK_CELL') if type(word_stack) is not KVariable: - word_stack_items = flatten_label('_:__EVM-TYPES_WordStack_Int_WordStack', word_stack) + word_stack_items = flatten_label('_:_WS', word_stack) for i in word_stack_items[:-1]: constraints.append(mlEqualsTrue(KEVM.range_uint(256, i))) @@ -371,7 +370,7 @@ def account_cell( @staticmethod def wordstack_len(wordstack: KInner) -> int: - return len(flatten_label('_:__EVM-TYPES_WordStack_Int_WordStack', wordstack)) + return len(flatten_label('_:_WS', wordstack)) @staticmethod def parse_bytestack(s: KInner) -> KApply: