solve error call for legacy_explore and incorrect name for #next[_]

runtimeverification · Jan 7, 2025 · a45ca20 · a45ca20
1 parent dfe2bae
commit a45ca20
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/kevm-pyk/src/kevm_pyk/summarizer.py b/kevm-pyk/src/kevm_pyk/summarizer.py
@@ -24,7 +24,7 @@ class KEVMSummarizer:
     1. Build the proof to symbolically execute one abitrary instruction.
     2. Run the proof to get the KCFG.
     3. Summarize the KCFG to get the summarized rules for the instructions.
-    rdots(pyk.KRewrite(pyk.KApply('#next[_]_EVM_InternalOp_OpCode', [opcode]), pyk.KConstant('#EmptyK')))
+    rdots(pyk.KRewrite(pyk.KApply('#next[_]_EVM_InternalOp_MaybeOpCode', [opcode]), pyk.KConstant('#EmptyK')))
     """
     _cterm_symbolic: CTermSymbolic
     kevm: KEVM
@@ -44,7 +44,7 @@ def build_spec(self, ) -> APRProof:
 
         def _to_init(kast: KInner) -> KInner:
             if type(kast) is KVariable and kast.name == 'K_CELL':
-                return KSequence([KApply('#next[_]_EVM_InternalOp_OpCode', KVariable('OP_CODE', KSort('OpCode'))), KVariable('K_CELL')])
+                return KSequence([KApply('#next[_]_EVM_InternalOp_MaybeOpCode', KVariable('OP_CODE', KSort('OpCode'))), KVariable('K_CELL')])
             return kast
 
         def _to_final(kast: KInner) -> KInner:
@@ -79,7 +79,7 @@ def _init_and_run_proof(proof: APRProof) -> tuple[bool, list[str] | None]:
                 log_succ_rewrites=True,
                 log_fail_rewrites=True,
                 fallback_on=None,
-                interim_simplification=True,
+                interim_simplification=25,
                 no_post_exec_simplify=False,
                 port=None,
                 haskell_threads=8,