Skip to content

Commit

Permalink
kontrol/prove: use factored out Minimizer
Browse files Browse the repository at this point in the history
  • Loading branch information
ehildenb committed Aug 28, 2024
1 parent 226a809 commit 61a5a3b
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion src/kontrol/prove.py
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@
from pyk.kast.inner import KApply, KSequence, KSort, KVariable, Subst
from pyk.kast.manip import flatten_label, set_cell
from pyk.kcfg import KCFG, KCFGExplore
from pyk.kcfg.minimize import KCFGMinimizer
from pyk.kore.rpc import KoreClient, TransportType, kore_server
from pyk.prelude.bytes import bytesToken
from pyk.prelude.collections import list_empty, map_empty, map_item, map_of, set_empty
Expand Down Expand Up @@ -730,7 +731,7 @@ def _method_to_cfg(
# Copy KCFG and minimize it
if graft_setup_proof:
cfg = KCFG.from_dict(setup_proof.kcfg.to_dict())
cfg.minimize()
KCFGMinimizer(cfg).minimize()
cfg.remove_node(setup_proof.target)
else:
cfg = KCFG()
Expand Down

0 comments on commit 61a5a3b

Please sign in to comment.