diff --git a/package/version b/package/version index a52e04166..072d0fa39 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.35 +0.1.36 diff --git a/pyproject.toml b/pyproject.toml index ed3c8caf1..2df65056b 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.35" +version = "0.1.36" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index 026d9682c..72cbcf8c0 100644 --- a/src/kontrol/__init__.py +++ b/src/kontrol/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '0.1.35' +VERSION: Final = '0.1.36' diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 16c5578fb..6de58d587 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -364,16 +364,17 @@ def _method_to_cfg( new_node_ids = [] if setup_proof: - init_node_id = setup_proof.kcfg.node(setup_proof.init).id - - cfg = setup_proof.kcfg - final_states = [cover.source for cover in cfg.covers(target_id=setup_proof.target)] - cfg.remove_node(setup_proof.target) - if len(setup_proof.pending) > 0: + if setup_proof.pending: raise RuntimeError( f'Initial state proof {setup_proof.id} for {contract.name}.{method.signature} still has pending branches.' ) - if len(final_states) < 1: + + init_node_id = setup_proof.init + + cfg = KCFG.from_dict(setup_proof.kcfg.to_dict()) # Copy KCFG + final_states = [cover.source for cover in cfg.covers(target_id=setup_proof.target)] + cfg.remove_node(setup_proof.target) + if not final_states: _LOGGER.warning( f'Initial state proof {setup_proof.id} for {contract.name}.{method.signature} has no passing branches to build on. Method will not be executed.' )