From a81c330571b111f82f5f61c21a284cc8619013fb Mon Sep 17 00:00:00 2001
From: Hernan Ponce de Leon <zeta96@gmail.com>
Date: Sun, 12 Nov 2023 12:15:42 +0100
Subject: [PATCH] Svcomp witness file must be named witness.graphml (new rule)
 (#563)

Signed-off-by: Hernan Ponce de Leon <hernanl.leon@huawei.com>
Co-authored-by: Hernan Ponce de Leon <hernanl.leon@huawei.com>
---
 .../main/java/com/dat3m/dartagnan/witness/WitnessGraph.java    | 3 +--
 .../java/com/dat3m/dartagnan/witness/BuildWitnessTest.java     | 2 +-
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessGraph.java
index b4f3bf6a71..82f137ef3d 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessGraph.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessGraph.java
@@ -136,8 +136,7 @@ private static BooleanFormula equalsParsedValue(Formula operand, String value, F
 	}
 
 	public void write() {
-		try (FileWriter fw = new FileWriter(String.format("%s/%s.graphml",
-				getOrCreateOutputDirectory(), Files.getNameWithoutExtension(getProgram())))) {
+		try (FileWriter fw = new FileWriter(String.format("%s/witness.graphml", getOrCreateOutputDirectory()))) {
 			fw.write("<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n");
 			fw.write("<graphml xmlns=\"http://graphml.graphdrawing.org/xmlns\" xmlns:xsi=\"http://www.w3.org/2001/XMLSchema-instance\">\n");
 			for (GraphAttributes attr : GraphAttributes.values()) {
diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/witness/BuildWitnessTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/witness/BuildWitnessTest.java
index ee7c7d3d65..652eed0626 100644
--- a/dartagnan/src/test/java/com/dat3m/dartagnan/witness/BuildWitnessTest.java
+++ b/dartagnan/src/test/java/com/dat3m/dartagnan/witness/BuildWitnessTest.java
@@ -47,7 +47,7 @@ public void BuildWriteEncode() throws Exception {
             WitnessBuilder witnessBuilder = WitnessBuilder.of(modelChecker.getEncodingContext(), prover, res);
             config.inject(witnessBuilder);
             WitnessGraph graph = witnessBuilder.build();
-            File witnessFile = new File(getOutputDirectory() + "/lazy01-for-witness.graphml");
+            File witnessFile = new File(getOutputDirectory() + "/witness.graphml");
             // The file should not exist
             assertFalse(witnessFile.exists());
             // Write to file