diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java index 4e22ad1de9..048e03d4d1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java @@ -1622,15 +1622,15 @@ public Delta visitTransitiveClosure(TransitiveClosure trans) { } private EventGraph computeTransitiveClosure(EventGraph oldOuter, EventGraph inner, boolean isMay) { - EventGraph next; EventGraph outer = new EventGraph(oldOuter); - outer.addAll(inner); - for (EventGraph current = EventGraph.difference(inner, oldOuter); !current.isEmpty(); current = next) { - next = new EventGraph(); - computeComposition(next, current, outer, isMay); - computeComposition(next, outer, current, isMay); - next.removeAll(outer); - outer.addAll(next); + EventGraph update = inner.filter(outer::add); + EventGraph updateComposition = new EventGraph(); + computeComposition(updateComposition, update, oldOuter, isMay); + update.addAll(updateComposition.filter(outer::add)); + while (!update.isEmpty()) { + EventGraph t = new EventGraph(); + computeComposition(t, inner, update, isMay); + update = t.filter(outer::add); } return outer; }