update kevm.py with new symbol names for WS constructors

runtimeverification · Mar 25, 2024 · 9ce02c7 · 9ce02c7
1 parent 3e6c88a
commit 9ce02c7
Showing 1 changed file with 3 additions and 3 deletions.
diff --git 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: