Fix smt solver parameters not getting sent to foundry_show in tests a…

…nd fix foundry_merge_nodes not using parameters in foundry_step_node
runtimeverification · Aug 22, 2023 · c024dc0 · c024dc0
1 parent 17f2270
commit c024dc0
Show file tree

Hide file tree

Showing 3 changed files with 24 additions and 9 deletions.
diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py
@@ -326,6 +326,7 @@ def legacy_explore(
     trace_rewrites: bool = False,
 ) -> Iterator[KCFGExplore]:
     # Old way of handling KCFGExplore, to be removed
+
     with kore_server(
         definition_dir=kprint.definition_dir,
         llvm_definition_dir=llvm_definition_dir,

diff --git a/kevm-pyk/src/kontrol/foundry.py b/kevm-pyk/src/kontrol/foundry.py
@@ -697,6 +697,8 @@ def foundry_show(
     failing: bool = False,
     failure_info: bool = False,
     counterexample_info: bool = False,
+    smt_timeout: int | None = None,
+    smt_retry_limit: int | None = None,
 ) -> str:
     contract_name = test.split('.')[0]
     foundry = Foundry(foundry_root)
@@ -731,7 +733,13 @@ def foundry_show(
     )
 
     if failure_info:
-        with legacy_explore(foundry.kevm, kcfg_semantics=KEVMSemantics(), id=proof.id) as kcfg_explore:
+        with legacy_explore(
+            foundry.kevm,
+            kcfg_semantics=KEVMSemantics(),
+            id=proof.id,
+            smt_timeout=smt_timeout,
+            smt_retry_limit=smt_retry_limit,
+        ) as kcfg_explore:
             res_lines += print_failure_info(proof, kcfg_explore, counterexample_info)
             res_lines += Foundry.help_info()
 

diff --git a/kevm-pyk/src/tests/integration/test_foundry_prove.py b/kevm-pyk/src/tests/integration/test_foundry_prove.py
@@ -105,8 +105,8 @@ def test_foundry_prove(test_id: str, foundry_root: Path, update_expected_output:
         foundry_root,
         tests=[test_id],
         simplify_init=False,
-        smt_timeout=300,
-        smt_retry_limit=10,
+        smt_timeout=50,
+        smt_retry_limit=1,
         use_booster=use_booster,
         counterexample_info=True,
     )
@@ -128,6 +128,8 @@ def test_foundry_prove(test_id: str, foundry_root: Path, update_expected_output:
         failing=True,
         failure_info=True,
         counterexample_info=True,
+        smt_timeout=300,
+        smt_retry_limit=10,
     )
 
     # Then
@@ -167,6 +169,8 @@ def test_foundry_fail(test_id: str, foundry_root: Path, update_expected_output:
         failing=True,
         failure_info=True,
         counterexample_info=True,
+        smt_timeout=300,
+        smt_retry_limit=10,
     )
 
     # Then
@@ -203,15 +207,15 @@ def test_foundry_merge_nodes(foundry_root: Path, use_booster: bool) -> None:
     foundry_prove(
         foundry_root,
         tests=[test_id],
-        smt_timeout=125,
-        smt_retry_limit=4,
+        smt_timeout=300,
+        smt_retry_limit=10,
         max_iterations=4,
         use_booster=use_booster,
     )
     check_pending(foundry_root, test_id, [6, 7])
 
-    foundry_step_node(foundry_root, test_id, node=6, depth=49)
-    foundry_step_node(foundry_root, test_id, node=7, depth=50)
+    foundry_step_node(foundry_root, test_id, node=6, depth=49, smt_timeout=300, smt_retry_limit=10)
+    foundry_step_node(foundry_root, test_id, node=7, depth=50, smt_timeout=300, smt_retry_limit=10)
 
     check_pending(foundry_root, test_id, [8, 9])
 
@@ -222,8 +226,8 @@ def test_foundry_merge_nodes(foundry_root: Path, use_booster: bool) -> None:
     prove_res = foundry_prove(
         foundry_root,
         tests=[test_id],
-        smt_timeout=125,
-        smt_retry_limit=4,
+        smt_timeout=300,
+        smt_retry_limit=10,
         use_booster=use_booster,
     )
     assert_pass(test_id, prove_res)
@@ -255,6 +259,8 @@ def test_foundry_auto_abstraction(foundry_root: Path, update_expected_output: bo
         pending=True,
         failing=True,
         failure_info=True,
+        smt_timeout=300,
+        smt_retry_limit=10,
     )
 
     assert_or_update_show_output(show_res, TEST_DATA_DIR / 'gas-abstraction.expected', update=update_expected_output)