Require the existence of violation node when validate violation witne…

…ss (#754) Signed-off-by: Hernan Ponce de Leon <[email protected]> Co-authored-by: Hernan Ponce de Leon <[email protected]>
hernanponcedeleon · Oct 12, 2024 · 878d282 · 878d282
1 parent c3aa592
commit 878d282
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphml/WitnessGraph.java
@@ -10,6 +10,7 @@
 import com.dat3m.dartagnan.wmm.utils.graph.EventGraph;
 import com.dat3m.dartagnan.wmm.utils.graph.mutable.MapEventGraph;
 import com.dat3m.dartagnan.wmm.utils.graph.mutable.MutableEventGraph;
+import com.google.common.base.Preconditions;
 import com.google.common.collect.Lists;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.BooleanFormulaManager;
@@ -113,6 +114,9 @@ private List<MemoryCoreEvent> getEventsFromEdge(Program program, Edge edge) {
     }
 
     public BooleanFormula encode(EncodingContext context) {
+        // If there is something to encode (i.e., edges is not empty),
+        // then there must be a violation node.
+        Preconditions.checkState(edges.isEmpty() || !getPathToViolation().isEmpty());
         Program program = context.getTask().getProgram();
         BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
         List<BooleanFormula> enc = new ArrayList<>();