We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
ImpNodePrinter
1 parent 8d0c36d commit 45b762fCopy full SHA for 45b762f
1 file changed
src/kimp/kimp.py
@@ -374,7 +374,7 @@ def show_kcfg(
374
claim_id: str,
375
) -> None:
376
proof = APRProof.read_proof_data(proof_dir=self.proof_dir, id=f'{spec_module}.{claim_id}')
377
- proof_show = APRProofShow(self.kprove, node_printer=ImpNodePrinter(kimp=self))
+ proof_show = APRProofShow(self.definition, node_printer=ImpNodePrinter(kimp=self))
378
res_lines = proof_show.show(
379
proof,
380
)
@@ -385,7 +385,9 @@ class ImpNodePrinter(NodePrinter):
385
kimp: KImp
386
387
def __init__(self, kimp: KImp):
388
- NodePrinter.__init__(self, kimp.kprove)
+ from pyk.cterm.show import CTermShow
389
+
390
+ super().__init__(cterm_show=CTermShow(kimp.format))
391
self.kimp = kimp
392
393
def print_node(self, kcfg: KCFG, node: KCFG.Node) -> list[str]:
0 commit comments