diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py index 4aeebc356a..26bcf540b4 100644 --- a/kevm-pyk/src/kevm_pyk/utils.py +++ b/kevm-pyk/src/kevm_pyk/utils.py @@ -30,7 +30,7 @@ from collections.abc import Callable, Collection, Iterable, Iterator from typing import Final, TypeVar - from pyk.kast.outer import KClaim, KDefinition + from pyk.kast.outer import KClaim, KDefinition, KFlatModule from pyk.kcfg import KCFG from pyk.kcfg.semantics import KCFGSemantics from pyk.kore.rpc import FallbackReason @@ -114,6 +114,7 @@ def run_prover( task_id: TaskID | None = None, maintenance_rate: int = 1, assume_defined: bool = False, + extra_module: KFlatModule | None = None, ) -> bool: prover: APRProver | ImpliesProver try: @@ -129,6 +130,7 @@ def create_prover() -> APRProver: fast_check_subsumption=fast_check_subsumption, direct_subproof_rules=direct_subproof_rules, assume_defined=assume_defined, + extra_module=extra_module, ) def update_status_bar(_proof: Proof) -> None: