Skip to content

Commit

Permalink
source node correction
Browse files Browse the repository at this point in the history
  • Loading branch information
PetarMax committed Dec 12, 2024
1 parent 5f278fe commit c60dd15
Showing 1 changed file with 4 additions and 2 deletions.
6 changes: 4 additions & 2 deletions pyk/src/pyk/kcfg/kcfg.py
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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)
Expand Down

0 comments on commit c60dd15

Please sign in to comment.