Skip to content

Commit 4774b8c

Browse files
committed
kevm-pyk: thread step_timeout through run_prover
Adds a `step_timeout: int | None = None` parameter to `run_prover` and forwards it to the `APRProver` constructor. `APRProver` enforces the per-step wall-clock budget (interrupt + halve `execute_depth` + retry), so `run_prover` only needs to pass the value through. Default `None` keeps the prior behavior (no per-step timeout).
1 parent c9c53eb commit 4774b8c

1 file changed

Lines changed: 2 additions & 0 deletions

File tree

kevm-pyk/src/kevm_pyk/utils.py

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -117,6 +117,7 @@ def run_prover(
117117
assume_defined: bool = False,
118118
extra_module: KFlatModule | None = None,
119119
optimize_kcfg: bool = False,
120+
step_timeout: int | None = None,
120121
) -> bool:
121122
prover: APRProver | ImpliesProver
122123
try:
@@ -134,6 +135,7 @@ def create_prover() -> APRProver:
134135
assume_defined=assume_defined,
135136
extra_module=extra_module,
136137
optimize_kcfg=optimize_kcfg,
138+
step_timeout=step_timeout,
137139
)
138140

139141
def update_status_bar(_proof: Proof) -> None:

0 commit comments

Comments
 (0)