Skip to content

Commit db011d7

Browse files
Stevengrerv-auditortothtamas28
authored
Add optimize_kcfg parameter in SymTool (#134)
This is needed when the `max_depth` is small but `max_iteractions` is big. --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>
1 parent c72b80f commit db011d7

4 files changed

Lines changed: 5 additions & 3 deletions

File tree

package/version

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
0.1.103
1+
0.1.104

pyproject.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ build-backend = "hatchling.build"
44

55
[project]
66
name = "kriscv"
7-
version = "0.1.103"
7+
version = "0.1.104"
88
description = "K tooling for the RISC-V architecture"
99
readme = "README.md"
1010
requires-python = "~=3.10"

src/kriscv/symtools.py

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -94,6 +94,7 @@ def prove(
9494
max_depth: int | None = None,
9595
max_iterations: int | None = None,
9696
includes: Iterable[str | Path] | None = None,
97+
optimize_kcfg: bool | None = None,
9798
) -> APRProof:
9899
from pyk.ktool.claim_loader import ClaimLoader
99100
from pyk.proof.reachability import APRProver
@@ -121,6 +122,7 @@ def prove(
121122
prover = APRProver(
122123
kcfg_explore=kcfg_explore,
123124
execute_depth=max_depth,
125+
optimize_kcfg=bool(optimize_kcfg),
124126
)
125127
prover.advance_proof(proof, max_iterations=max_iterations)
126128

uv.lock

Lines changed: 1 addition & 1 deletion
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

0 commit comments

Comments
 (0)