diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 533a8e82cb..94c03ea527 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.349" +version = "1.0.350" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index fb44402466..c9ec0c2476 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.349' +VERSION: Final = '1.0.350' diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 278205a38d..7ce4e000ef 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -295,7 +295,10 @@ def exec_prove( _ignore_arg(kwargs, 'md_selector', f'--md-selector: {kwargs["md_selector"]}') md_selector = 'k' - digest_file = save_directory / 'digest' if save_directory is not None else None + if save_directory is None: + save_directory = Path(tempfile.mkdtemp()) + + digest_file = save_directory / 'digest' if definition_dir is None: definition_dir = kdist.get('evm-semantics.haskell') @@ -305,9 +308,6 @@ def exec_prove( if smt_retry_limit is None: smt_retry_limit = 10 - if save_directory is None: - save_directory = Path(tempfile.TemporaryDirectory().name) - kevm = KEVM(definition_dir, use_directory=save_directory, bug_report=bug_report) include_dirs = [Path(include) for include in includes] @@ -363,22 +363,12 @@ def _init_and_run_proof(claim_job: KClaimJob) -> tuple[bool, list[str] | None]: ) as kcfg_explore: proof_problem: Proof if is_functional(claim): - if ( - save_directory is not None - and not reinit - and up_to_date - and EqualityProof.proof_exists(claim.label, save_directory) - ): + if not reinit and up_to_date and EqualityProof.proof_exists(claim.label, save_directory): proof_problem = EqualityProof.read_proof_data(save_directory, claim.label) else: proof_problem = EqualityProof.from_claim(claim, kevm.definition, proof_dir=save_directory) else: - if ( - save_directory is not None - and not reinit - and up_to_date - and APRProof.proof_data_exists(claim.label, save_directory) - ): + if not reinit and up_to_date and APRProof.proof_data_exists(claim.label, save_directory): proof_problem = APRProof.read_proof_data(save_directory, claim.label) else: diff --git a/package/version b/package/version index ad33520251..a208350217 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.349 +1.0.350