Svcomp witness file must be named witness.graphml (new rule) (hernanp…

…oncedeleon#563) Signed-off-by: Hernan Ponce de Leon <[email protected]> Co-authored-by: Hernan Ponce de Leon <[email protected]>
xFrednet · Nov 12, 2023 · a81c330 · a81c330
1 parent ebe38ef
commit a81c330
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 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
@@ -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
@@ -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