diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py
index d3f9247e49f..835aea290c5 100644
--- a/pyk/src/pyk/kcfg/kcfg.py
+++ b/pyk/src/pyk/kcfg/kcfg.py
@@ -1188,7 +1188,19 @@ def shortest_distance_between(self, node_1_id: NodeIdLike, node_2_id: NodeIdLike
         return distance
 
     def zero_depth_between(self, node_1_id: NodeIdLike, node_2_id: NodeIdLike) -> bool:
-        shortest_distance = self.shortest_distance_between(node_1_id, node_2_id)
+        _node_1_id = self._resolve(node_1_id)
+        _node_2_id = self._resolve(node_2_id)
+        if _node_1_id == _node_2_id:
+            return True
+        # Short-circuit and don't run pathing algorithm if there is no 0 length path on the first step.
+        path_lengths = [
+            self.path_length([successor]) for successor in self.successors(_node_1_id) + self.successors(_node_2_id)
+        ]
+        if 0 not in path_lengths:
+            return False
+
+        shortest_distance = self.shortest_distance_between(_node_1_id, _node_2_id)
+
         return shortest_distance is not None and shortest_distance == 0
 
     def paths_between(self, source_id: NodeIdLike, target_id: NodeIdLike) -> list[tuple[Successor, ...]]:
diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py
index 2a62fe37f5b..58c9bb24df0 100644
--- a/pyk/src/pyk/proof/reachability.py
+++ b/pyk/src/pyk/proof/reachability.py
@@ -167,7 +167,8 @@ def get_steps(self) -> list[APRProofStep]:
                     else:
                         shortest_path.append(succ.source)
 
-            module_name = self.circularities_module_name if self.nonzero_depth(node) else self.dependencies_module_name
+            nonzero_depth = self.nonzero_depth(node)
+            module_name = self.circularities_module_name if nonzero_depth else self.dependencies_module_name
 
             steps.append(
                 APRProofStep(
@@ -179,7 +180,7 @@ def get_steps(self) -> list[APRProofStep]:
                     shortest_path_to_node=tuple(shortest_path),
                     prior_loops_cache=FrozenDict(self.prior_loops_cache),
                     circularity=self.circularity,
-                    nonzero_depth=self.nonzero_depth(node),
+                    nonzero_depth=nonzero_depth,
                     circularity_rule_id=f'{self.rule_id}-{self.init}-TO-{self.target}',
                 )
             )