diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 53b1b26e586..fab28f6cc60 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -507,14 +507,17 @@ def one_line_summary(self) -> str: nodes = len(self.kcfg.nodes) pending = len(self.pending) failing = len(self.failing) - branches = len(self.kcfg.ndbranches()) + len(self.kcfg.splits()) + branches = 0 + for branch in self.kcfg.ndbranches() + self.kcfg.splits(): + branches += len(branch.targets) vacuous = len(self.kcfg.vacuous) terminal = len(self.terminal) stuck = len(self.kcfg.stuck) passed = len([cover for cover in self.kcfg.covers() if cover.target.id == self.target]) + refuted = len(self.node_refutations) return ( super().one_line_summary - + f'|{nodes} nodes|{pending} pending|{passed} passed|{failing} failing|{branches} branches|{vacuous} vacuous|{terminal} terminal|{stuck} stuck' + + f' --- {nodes} nodes|{branches} branches|{terminal} terminal --- {pending} pending|{passed} passed|{failing} failing|{vacuous} vacuous|{refuted} refuted|{stuck} stuck' ) def get_refutation_id(self, node_id: int) -> str: