Merge branch 'master' into _update-deps/runtimeverification/k

Author: automergerpr-permission-manager[bot]

Diff for: .github/workflows/test-pr.yml

@@ -110,7 +110,7 @@ jobs:
           - name: 'Summarization'
             test-suite: 'test-summarize'
             test-args:
-            timeout: 150
+            timeout: 30
             parallel: 6
           - name: 'DSS'
             test-suite: 'test-prove-dss'

Diff for: kevm-pyk/src/kevm_pyk/summarizer.py

@@ -559,7 +559,7 @@ def create_kcfg_explore() -> KCFGExplore:
                 passed = run_prover(
                     proof,
                     create_kcfg_explore=create_kcfg_explore,
-                    max_depth=1000,
+                    max_depth=1,
                     max_iterations=None,
                     cut_point_rules=KEVMSemantics.cut_point_rules(
                         break_on_jumpi=False,

Diff for: kevm-pyk/src/tests/integration/test_summarize.py

@@ -9,7 +9,8 @@
 def test_summarize(opcode: str) -> None:
     if get_summary_status(opcode) != 'PASSED':
         pytest.skip(f'{opcode} status: {OPCODES_SUMMARY_STATUS[opcode]}')
-    if opcode in ['DUP', 'SWAP', 'BALANCE', 'SDIV', 'LOG', 'SMOD', 'BYTE']:
+
+    if opcode in ['DUP', 'SWAP', 'LOG']:
         pytest.skip(f'{opcode} summarization is time-consuming')
 
     print(f'[{opcode}] selected')