fix inconsistent use of the '_:_WS' klabel

runtimeverification · Sep 4, 2023 · 0569bfd · 0569bfd
1 parent eb5f2a4
commit 0569bfd
Showing 1 changed file with 2 additions and 3 deletions.
diff --git 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: