Merge remote-tracking branch 'origin/master' into release

Author: rv-auditor

src/kontrol/cli.py

@@ -576,6 +576,13 @@ def parse(s: str) -> list[T]:
         action='store_true',
         help='Generate a Solidity test contract with concrete counterexample values when proofs fail.',
     )
+    prove_args.add_argument(
+        '--step-timeout',
+        type=int,
+        default=None,
+        dest='step_timeout',
+        help='Per-step wall-clock budget in whole seconds; on timeout the backend request is interrupted and the execution depth is halved before retrying. Disabled by default.',
+    )
 
     show_args = command_parser.add_parser(
         'show',

src/kontrol/options.py

@@ -350,6 +350,7 @@ class ProveOptions(
     extra_module: str | None
     symbolic_caller: bool
     generate_counterexample: bool
+    step_timeout: int | None
 
     def __init__(self, args: dict[str, Any]) -> None:
         super().__init__(args)
@@ -383,6 +384,7 @@ def default() -> dict[str, Any]:
             'extra_module': None,
             'symbolic_caller': False,
             'generate_counterexample': False,
+            'step_timeout': None,
         }
 
     @staticmethod

src/kontrol/prove.py

@@ -461,6 +461,7 @@ def create_kcfg_explore() -> KCFGExplore:
                 assume_defined=options.assume_defined,
                 extra_module=lemmas_module,
                 optimize_kcfg=options.optimize_kcfg,
+                step_timeout=options.step_timeout,
             )
 
             if progress is not None and task is not None: