Fixing incorrect removal of terminal nodes (runtimeverification/pyk#626)

This PR corrects an error that occurs when pruning a node from the
`kcfg` - the node would be removed and *then* its `id` would be
resolved, causing said error.

---------

Co-authored-by: devops <devops@runtimeverification.com>

pyk/package/version

@@ -1 +1 @@
-0.1.429
+0.1.430

pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.429"
+version = "0.1.430"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

pyk/src/pyk/kcfg/exploration.py

@@ -54,15 +54,16 @@ def add_terminal(self, node_id: NodeIdLike) -> None:
         self._terminal.add(self.kcfg._resolve(node_id))
 
     # Unmarking a given node as terminal
-    def remove_terminal(self, node_id: NodeIdLike) -> None:
-        self._terminal.discard(self.kcfg._resolve(node_id))
+    def remove_terminal(self, node_id: int) -> None:
+        self._terminal.discard(node_id)
 
     #
     # Lifted KCFG functions that may affect terminal nodes
     #
 
     # Removing a given node
     def remove_node(self, node_id: NodeIdLike) -> None:
+        node_id = self.kcfg._resolve(node_id)
         self.kcfg.remove_node(node_id)
         self.remove_terminal(node_id)
 

pyk/src/pyk/proof/reachability.py

@@ -122,6 +122,10 @@ def shortest_path_to(self, node_id: NodeIdLike) -> tuple[KCFG.Successor, ...]:
         assert spb is not None
         return spb
 
+    def prune(self, node_id: NodeIdLike, keep_nodes: Iterable[NodeIdLike] = ()) -> list[int]:
+        pruned_nodes = super().prune(node_id, keep_nodes=list(keep_nodes) + [self.init, self.target])
+        return pruned_nodes
+
     @staticmethod
     def read_proof(id: str, proof_dir: Path) -> APRProof:
         proof_path = proof_dir / f'{hash_str(id)}.json'
@@ -427,7 +431,7 @@ def is_failing(self, node_id: NodeIdLike) -> bool:
         return super().is_failing(node_id) and not self.is_bounded(node_id)
 
     def prune(self, node_id: NodeIdLike, keep_nodes: Iterable[NodeIdLike] = ()) -> list[int]:
-        pruned_nodes = self.prune(node_id, keep_nodes=keep_nodes)
+        pruned_nodes = super().prune(node_id, keep_nodes=keep_nodes)
         for nid in pruned_nodes:
             self.remove_bounded(nid)
         return pruned_nodes
@@ -495,8 +499,8 @@ def from_claim_with_bmc_depth(
     def add_bounded(self, nid: NodeIdLike) -> None:
         self._bounded.add(self.kcfg._resolve(nid))
 
-    def remove_bounded(self, node_id: NodeIdLike) -> None:
-        self._bounded.discard(self.kcfg._resolve(node_id))
+    def remove_bounded(self, node_id: int) -> None:
+        self._bounded.discard(node_id)
 
     @property
     def summary(self) -> CompositeSummary: