diff --git a/package/version b/package/version index 09bc4f7cc..c037e80c7 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.558 +0.1.559 diff --git a/pyproject.toml b/pyproject.toml index 1f4c7061c..0f8ec8b46 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.558" +version = "0.1.559" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index 7d260a7ea..13a2e4f09 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -1280,7 +1280,7 @@ def steps(self, proof: APRProof) -> Iterable[APRProofStep]: target_is_terminal=(proof.target not in proof._terminal), main_module_name=self.prover.main_module_name, dependencies_as_claims=[d.as_claim(self.kprint) for d in apr_subproofs], - self_proof_as_claim=proof.as_claim(self.kprint), + self_proof_as_claim=(proof.as_claim(self.kprint) if proof.circularity else None), circularity=proof.circularity, depth_is_nonzero=self.prover.nonzero_depth(pending_node), ) @@ -1405,7 +1405,7 @@ class APRProofStep(parallel.ProofStep[APRProofResult, APRProofProcessData]): trace_rewrites: bool dependencies_as_claims: list[KClaim] - self_proof_as_claim: KClaim + self_proof_as_claim: KClaim | None circularity: bool depth_is_nonzero: bool @@ -1470,7 +1470,12 @@ def exec(self, data: APRProofProcessData) -> APRProofResult: kcfg_explore.add_dependencies_module( self.main_module_name, self.circularities_module_name, - self.dependencies_as_claims + ([self.self_proof_as_claim] if self.circularity else []), + self.dependencies_as_claims + + ( + [self.self_proof_as_claim] + if (self.circularity and (self.self_proof_as_claim is not None)) + else [] + ), priority=1, )