diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index c2f0584321..57129bf97a 100644 --- a/kevm-pyk/src/kevm_pyk/kevm.py +++ b/kevm-pyk/src/kevm_pyk/kevm.py @@ -237,7 +237,7 @@ def _kevm_patch_symbol_table(cls, symbol_table: SymbolTable) -> None: '_Set_', 'typedArgs', '_up/Int__EVM-TYPES_Int_Int_Int', - '_:__EVM-TYPES_WordStack_Int_WordStack', + '_WS_' ] for symb in paren_symbols: if symb in symbol_table: @@ -281,7 +281,7 @@ def _add_account_invariant(account: KApply) -> list[KApply]: 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))) @@ -475,7 +475,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: