Merge branch 'develop' into _update-deps/runtimeverification/llvm-bac…

…kend

pyk/src/pyk/proof/proof.py

@@ -326,6 +326,7 @@ def parallel_advance_proof(
     fail_fast: bool = False,
     max_workers: int = 1,
     callback: Callable[[P], None] = (lambda x: None),
+    maintenance_rate: int = 1,
 ) -> None:
     """Advance proof with multithreaded strategy.
 
@@ -347,7 +348,8 @@ def parallel_advance_proof(
         fail_fast: If the proof is failing after finishing a step,
           halt execution even if there are still available steps.
         max_workers: Maximum number of worker threads the pool can spawn.
-        callback: Callable to run in between each completed step, useful for getting real-time information about the proof.
+        callback: Callable to run during proof maintenance, useful for getting real-time information about the proof.
+        maintenance_rate: Number of iterations between proof maintenance (writing to disk and executing callback).
     """
     pending: set[Future[Any]] = set()
     explored: set[PS] = set()
@@ -376,9 +378,10 @@ def submit_steps(_steps: Iterable[PS]) -> None:
                 proof_results = future.result()
                 for result in proof_results:
                     proof.commit(result)
-                proof.write_proof_data()
-                callback(proof)
                 iterations += 1
+                if iterations % maintenance_rate == 0:
+                    proof.write_proof_data()
+                    callback(proof)
                 if max_iterations is not None and max_iterations <= iterations:
                     break
                 if fail_fast and proof.failed:
@@ -502,6 +505,7 @@ def advance_proof(
         max_iterations: int | None = None,
         fail_fast: bool = False,
         callback: Callable[[P], None] = (lambda x: None),
+        maintenance_rate: int = 1,
     ) -> None:
         """Advance a proof.
 
@@ -513,6 +517,7 @@ def advance_proof(
             fail_fast: If the proof is failing after finishing a step,
               halt execution even if there are still available steps.
             callback: Callable to run in between each completed step, useful for getting real-time information about the proof.
+            maintenance_rate: Number of iterations between proof maintenance (writing to disk and executing callback).
         """
         iterations = 0
         _LOGGER.info(f'Initializing proof: {proof.id}')
@@ -533,7 +538,9 @@ def advance_proof(
                 results = self.step_proof(step)
                 for result in results:
                     proof.commit(result)
-                proof.write_proof_data()
-                callback(proof)
+                if iterations % maintenance_rate == 0:
+                    proof.write_proof_data()
+                    callback(proof)
+
         if proof.failed:
             proof.failure_info = self.failure_info(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: