Status bar improvements (#4575)

- Adds the number of refuted nodes to the proof status bar.
- Adds a separator which separates the one line summary into 3 parts,
one which is the proof status, one to do with structure, and one to do
with status of the leaves.
- Changes the definition of `branches` to mean "how many `Split` and
`NDBranch` targets are there?" instead of "how many `Split`s and
`NDBranch`es are there?" to more accurately reflect the degree of
branching in a proof.

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: