Merge remote-tracking branch 'origin/develop'

runtimeverification · Oct 7, 2024 · 8df24f5 · 8df24f5
2 parents c50060b + d40018b
commit 8df24f5
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 6 deletions.
diff --git a/pyk/src/pyk/kcfg/exploration.py b/pyk/src/pyk/kcfg/exploration.py
@@ -109,5 +109,5 @@ def to_dict(self) -> dict[str, Any]:
     #
 
     # Minimizing the KCFG
-    def minimize_kcfg(self) -> None:
-        KCFGMinimizer(self.kcfg).minimize()
+    def minimize_kcfg(self, merge: bool = False) -> None:
+        KCFGMinimizer(self.kcfg).minimize(merge=merge)
diff --git a/pyk/src/pyk/kcfg/minimize.py b/pyk/src/pyk/kcfg/minimize.py
@@ -288,7 +288,7 @@ def _is_mergeable(x: KCFG.Edge | KCFG.MergedEdge, y: KCFG.Edge | KCFG.MergedEdge
 
         return True
 
-    def minimize(self) -> None:
+    def minimize(self, merge: bool = False) -> None:
         """Minimize KCFG by repeatedly performing the lifting transformations.
 
         The KCFG is transformed to an equivalent in which no further lifting transformations are possible.
@@ -300,5 +300,5 @@ def minimize(self) -> None:
             repeat = self.lift_splits() or repeat
 
         repeat = True
-        while repeat:
+        while repeat and merge:
             repeat = self.merge_nodes()
diff --git a/pyk/src/tests/unit/kcfg/merge_node_data.py b/pyk/src/tests/unit/kcfg/merge_node_data.py
@@ -255,12 +255,12 @@ def util_check_constraint(constraint: KInner, merged_var: KVariable, under_check
 
 
 def check_merge_no(minimizer: KCFGMinimizer) -> None:
-    minimizer.minimize()
+    minimizer.minimize(merge=True)
     assert minimizer.kcfg.to_dict() == merge_node_test_kcfg().to_dict()
 
 
 def check_merged_one(minimizer: KCFGMinimizer) -> None:
-    minimizer.minimize()
+    minimizer.minimize(merge=True)
     # 1 --> merged bi: Merged Edge
     merged_edge = single(minimizer.kcfg.merged_edges(source_id=1))
     edges = {2: 9, 3: 10, 16: 20, 17: 21, 18: 22, 19: 23, 6: 13, 7: 14, 8: 15}