From bdc5c9320974002fb8051eb51aa4d76371bf0873 Mon Sep 17 00:00:00 2001
From: palinatolmach <polina.tolmach@gmail.com>
Date: Thu, 9 Jan 2025 18:09:31 +0400
Subject: [PATCH] Experiment: increase SMT timeout for `sum-to-n-spec`

---
 kevm-pyk/src/tests/integration/test_prove.py | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py
index c49202a2d5..2220c8684a 100644
--- a/kevm-pyk/src/tests/integration/test_prove.py
+++ b/kevm-pyk/src/tests/integration/test_prove.py
@@ -218,6 +218,9 @@ def _test_prove(
         break_on_basic_blocks = name in TEST_PARAMS and TEST_PARAMS[name].break_on_basic_blocks
         if workers is None:
             workers = 1 if name not in TEST_PARAMS else TEST_PARAMS[name].workers
+        smt_timeout = 300 if name not in TEST_PARAMS else TEST_PARAMS[name].smt_timeout
+        smt_retry_limit = 10 if name not in TEST_PARAMS else TEST_PARAMS[name].smt_retry_limit
+
         options = ProveOptions(
             {
                 'spec_file': spec_file,
@@ -233,6 +236,8 @@ def _test_prove(
                 'break_on_basic_blocks': break_on_basic_blocks,
                 'workers': workers,
                 'direct_subproof_rules': direct_subproof_rules,
+                'smt_timeout': smt_timeout,
+                'smt_retry_limit': smt_retry_limit,
             }
         )
         exec_prove(options=options)
@@ -287,6 +292,8 @@ class TParams:
     break_on_calls: bool
     break_on_basic_blocks: bool
     workers: int
+    smt_timeout: int
+    retry_limit: int
 
     def __init__(
         self,
@@ -295,17 +302,22 @@ def __init__(
         break_on_calls: bool = False,
         break_on_basic_blocks: bool = False,
         workers: int = 1,
+        smt_timeout: int | None = 300,
+        smt_retry_limit: int | None = 10,
     ) -> None:
         self.main_claim_id = main_claim_id
         self.leaf_number = leaf_number
         self.break_on_calls = break_on_calls
         self.break_on_basic_blocks = break_on_basic_blocks
         self.workers = workers
+        self.smt_timeout = smt_timeout
+        self.smt_retry_limit = smt_retry_limit
 
 
 TEST_PARAMS: dict[str, TParams] = {
     'functional/lemmas-spec.k': TParams(workers=8),
     'examples/sum-to-n-foundry-spec.k': TParams(break_on_basic_blocks=True),
+    'examples/sum-to-n-spec.k': TParams(smt_timeout=600, smt_retry_limit=20),
 }