diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index 47bd70abf7..d68c66c8b3 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -586,6 +586,7 @@ def log(message: str, *, warning: bool = False) -> None: log(f'abstraction node: {node.id}') case Step(cterm, depth, next_node_logs, rule_labels, _): + node_id = node.id next_node = self.create_node(cterm) # Optimization for steps consists of on-the-fly merging of consecutive edges and can # be performed only if the current node has a single predecessor connected by an Edge @@ -596,12 +597,13 @@ def log(message: str, *, warning: bool = False) -> None: ): # The existing edge is removed and the step parameters are updated accordingly self.remove_edge(in_edge.source.id, node.id) + node_id = in_edge.source.id depth += in_edge.depth rule_labels = list(in_edge.rules) + rule_labels next_node_logs = logs[node.id] + next_node_logs if node.id in logs else next_node_logs - self.create_edge(in_edge.source.id, next_node.id, depth, rule_labels) + self.create_edge(node_id, next_node.id, depth, rule_labels) logs[next_node.id] = next_node_logs - log(f'basic block at depth {depth}: {node.id} --> {next_node.id}') + log(f'basic block at depth {depth}: {node_id} --> {next_node.id}') case Branch(branches, _): branch_node_ids = self.split_on_constraints(node.id, branches)