diff --git a/package/version b/package/version
index b67246167..5abb16f50 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.442
+0.1.443
diff --git a/pyproject.toml b/pyproject.toml
index 946acbfa0..73447ac3a 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.442"
+version = "0.1.443"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py
index f18999f0f..d3542944f 100644
--- a/src/pyk/proof/reachability.py
+++ b/src/pyk/proof/reachability.py
@@ -47,6 +47,7 @@ class APRProof(Proof, KCFGExploration):
     target: int
     logs: dict[int, tuple[LogEntry, ...]]
     circularity: bool
+    failure_info: APRFailureInfo | None
 
     def __init__(
         self,
@@ -65,6 +66,7 @@ def __init__(
         Proof.__init__(self, id, proof_dir=proof_dir, subproof_ids=subproof_ids, admitted=admitted)
         KCFGExploration.__init__(self, kcfg, terminal)
 
+        self.failure_info = None
         self.init = kcfg._resolve(init)
         self.target = kcfg._resolve(target)
         self.logs = logs
@@ -534,6 +536,7 @@ class APRProver(Prover):
     main_module_name: str
     dependencies_module_name: str
     circularities_module_name: str
+    counterexample_info: bool
 
     _checked_terminals: set[int]
 
@@ -541,10 +544,12 @@ def __init__(
         self,
         proof: APRProof,
         kcfg_explore: KCFGExplore,
+        counterexample_info: bool = False,
     ) -> None:
         super().__init__(kcfg_explore)
         self.proof = proof
         self.main_module_name = self.kcfg_explore.kprint.definition.main_module_name
+        self.counterexample_info = counterexample_info
 
         subproofs: list[Proof] = (
             [Proof.read_proof_data(proof.proof_dir, i) for i in proof.subproof_ids]
@@ -662,6 +667,9 @@ def advance_proof(
                 if self.proof.kcfg.is_leaf(node.id) and not self.proof.is_target(node.id):
                     self._check_subsume(node)
 
+        if self.proof.failed:
+            self.save_failure_info()
+
         self.proof.write_proof_data()
 
     def refute_node(self, node: KCFG.Node) -> RefutationProof | None:
@@ -730,8 +738,11 @@ def construct_node_refutation(self, node: KCFG.Node) -> RefutationProof | None:
         self.proof.add_subproof(refutation)
         return refutation
 
+    def save_failure_info(self) -> None:
+        self.proof.failure_info = self.failure_info()
+
     def failure_info(self) -> APRFailureInfo:
-        return APRFailureInfo.from_proof(self.proof, self.kcfg_explore)
+        return APRFailureInfo.from_proof(self.proof, self.kcfg_explore, counterexample_info=self.counterexample_info)
 
 
 @dataclass(frozen=True)
@@ -869,10 +880,12 @@ def __init__(
         self,
         proof: APRBMCProof,
         kcfg_explore: KCFGExplore,
+        counterexample_info: bool = False,
     ) -> None:
         super().__init__(
             proof,
             kcfg_explore=kcfg_explore,
+            counterexample_info=counterexample_info,
         )
         self._checked_nodes = []