Fix witnesses excluding the rf edges they enforce. (#771)

xeren · web-flow · commit d2ccf4f0e2b6 · 2024-11-06T09:29:21.000+01:00
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
@@ -875,7 +875,7 @@ public MutableKnowledge visitReadFrom(ReadFrom rf) {
                 EventGraph g = witness.getReadFromKnowledge(program, alias);
                 must.addAll(g);
                 for (Event r : g.getRange()) {
-                    may.removeIf((e1, e2) -> e2 == r);
+                    may.removeIf((e1, e2) -> e2 == r && !g.contains(e1, e2));
                 }
             }
 
diff --git a/svcomp.properties b/svcomp.properties
@@ -3,5 +3,3 @@ encoding.integers=true
 svcomp.step=5
 svcomp.umax=27
 witness=graphml
-// We can get rid of the option below once #767 is fixed
-wmm.analysis.extendedRelationAnalysis=false

Original file line number	Diff line number	Diff line change
`@@ -875,7 +875,7 @@ public MutableKnowledge visitReadFrom(ReadFrom rf) {`
`875`	`875`	`EventGraph g = witness.getReadFromKnowledge(program, alias);`
`876`	`876`	`must.addAll(g);`
`877`	`877`	`for (Event r : g.getRange()) {`
`878`		`- may.removeIf((e1, e2) -> e2 == r);`
	`878`	`+ may.removeIf((e1, e2) -> e2 == r && !g.contains(e1, e2));`
`879`	`879`	`}`
`880`	`880`	`}`
`881`	`881`