diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/witness/visitors/VisitorXML.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/witness/visitors/VisitorXML.java
index ec51148664..773596b044 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/witness/visitors/VisitorXML.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/witness/visitors/VisitorXML.java
@@ -5,18 +5,17 @@
 import com.dat3m.dartagnan.parsers.XMLParser.ElementContext;
 import com.dat3m.dartagnan.parsers.XMLParserBaseVisitor;
 import com.dat3m.dartagnan.witness.Edge;
+import com.dat3m.dartagnan.witness.ElemWithAttributes;
 import com.dat3m.dartagnan.witness.Node;
 import com.dat3m.dartagnan.witness.WitnessGraph;
 
-import static com.dat3m.dartagnan.witness.GraphAttributes.*;
-import static com.dat3m.dartagnan.witness.NodeAttributes.*;
-
-import java.util.stream.Collectors;
+import static com.dat3m.dartagnan.witness.GraphAttributes.PRODUCER;
+import static com.dat3m.dartagnan.witness.GraphAttributes.WITNESSTYPE;
 
 public class VisitorXML extends XMLParserBaseVisitor<Object> {
 
     private final WitnessGraph graph = new WitnessGraph();
-    private String lastAddedNodeId;
+    private ElemWithAttributes current = graph;
 
     @Override
     public WitnessGraph visitDocument(XMLParser.DocumentContext ctx) {
@@ -29,52 +28,45 @@ public WitnessGraph visitDocument(XMLParser.DocumentContext ctx) {
 
     @Override
     public Object visitElement(XMLParser.ElementContext ctx) {
-        if (ctx.content() != null) {
-            if (ctx.Name(0).getText().equals("data")) {
-                if (ctx.content() != null) {
-                    String key = ctx.attribute(0).STRING().getText();
-                    key = key.substring(1, key.length() - 1);
-                    String value = ctx.content().getText();
-                    if (key.equals(PROGRAMFILE.toString()) || key.equals(PRODUCER.toString())
-                            || key.equals(UNROLLBOUND.toString())) {
-                        graph.addAttribute(key, value);
-                    }
-                    if (key.equals(WITNESSTYPE.toString()) && !value.equals("violation_witness")) {
-                        throw new ParsingException("Dartagnan can only validate violation witnesses");
-                    }
-                    if (key.equals(ENTRY.toString()) || key.equals(VIOLATION.toString())) {
-                        graph.getNode(lastAddedNodeId).addAttribute(key, value);
-                    }
+        final String elementType = ctx.Name(0).getText();
+        return switch (elementType) {
+            case "data" -> {
+                final String key = getAttributeString(ctx, 0);
+                final String value = ctx.content().getText();
+                if (key.equals(WITNESSTYPE.toString()) && !value.equals("violation_witness")) {
+                    throw new ParsingException("Dartagnan can only validate violation witnesses");
                 }
+                current.addAttribute(key, value);
+                yield null;
             }
-            if (ctx.Name(0).getText().equals("node")) {
-                String name = ctx.attribute(0).STRING().toString();
-                lastAddedNodeId = name.substring(1, name.length() - 1);
-                graph.addNode(lastAddedNodeId);
+            case "node" -> {
+                final String name = getAttributeString(ctx, 0);
+                graph.addNode(name);
+                current = graph.getNode(name);
+                visitChildren(ctx);
+                current = graph;
+                yield null;
             }
-            if (ctx.Name(0).getText().equals("edge")) {
-                int idx = ctx.attribute().stream().map(a -> a.Name().toString()).collect(Collectors.toList())
-                        .indexOf("source");
-                String name = ctx.attribute(idx).STRING().toString();
-                name = name.substring(1, name.length() - 1);
-                Node v0 = graph.hasNode(name) ? graph.getNode(name) : new Node(name);
-                idx = ctx.attribute().stream().map(a -> a.Name().toString()).collect(Collectors.toList())
-                        .indexOf("target");
-                name = ctx.attribute(idx).STRING().toString();
-                name = name.substring(1, name.length() - 1);
-                Node v1 = graph.hasNode(name) ? graph.getNode(name) : new Node(name);
-                Edge edge = new Edge(v0, v1);
-                if (ctx.content() != null) {
-                    for (ElementContext elem : ctx.content().element()) {
-                        String key = elem.attribute(0).STRING().getText();
-                        key = key.substring(1, key.length() - 1);
-                        String value = elem.content().getText();
-                        edge.addAttribute(key, value);
-                    }
-                }
+            case "edge" -> {
+                final Edge edge = new Edge(getNode(ctx, "source"), getNode(ctx, "target"));
                 graph.addEdge(edge);
+                current = edge;
+                visitChildren(ctx);
+                current = graph;
+                yield null;
             }
-        }
-        return visitChildren(ctx);
+            default -> visitChildren(ctx);
+        };
+    }
+
+    private Node getNode(ElementContext ctx, String vertex) {
+        final int idx = ctx.attribute().stream().map(a -> a.Name().toString()).toList().indexOf(vertex);
+        final String name = getAttributeString(ctx, idx);
+        return graph.hasNode(name) ? graph.getNode(name) : new Node(name);
+    }
+
+    private String getAttributeString(ElementContext ctx, int index) {
+        final String attributeStr = ctx.attribute(index).STRING().toString();
+        return attributeStr.substring(1, attributeStr.length() - 1);
     }
 }
\ No newline at end of file
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 bfc3922365..1411a84d7e 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessGraph.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessGraph.java
@@ -9,15 +9,18 @@
 import com.dat3m.dartagnan.program.event.metadata.SourceLocation;
 import com.dat3m.dartagnan.wmm.utils.EventGraph;
 import com.google.common.collect.Lists;
-import org.sosy_lab.java_smt.api.*;
+import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.BooleanFormulaManager;
 
 import java.io.FileWriter;
 import java.io.IOException;
 import java.util.*;
 
 import static com.dat3m.dartagnan.GlobalSettings.getOrCreateOutputDirectory;
-import static com.dat3m.dartagnan.witness.GraphAttributes.*;
-import static com.dat3m.dartagnan.witness.NodeAttributes.*;
+import static com.dat3m.dartagnan.witness.GraphAttributes.PRODUCER;
+import static com.dat3m.dartagnan.witness.GraphAttributes.PROGRAMFILE;
+import static com.dat3m.dartagnan.witness.NodeAttributes.ENTRY;
+import static com.dat3m.dartagnan.witness.NodeAttributes.VIOLATION;
 
 public class WitnessGraph extends ElemWithAttributes {
 
@@ -140,9 +143,9 @@ public EventGraph getReadFromKnowledge(Program program, AliasAnalysis alias) {
             current = currents.size() == 1 ? currents.get(0) : null;
             // If a graph edge implies a hb-relation, inter-thread communication guarantees
             // same address and thus rf.
-            if (last != null && current != null && last instanceof Store && current instanceof Load
+            if (last instanceof Store && current instanceof Load
                     && ((graphEdgeImpliesHbEdge() && !last.getThread().equals(current.getThread()))
-                            || alias.mustAlias(last, current))) {
+                    || alias.mustAlias(last, current))) {
                 k.add(last, current);
             }
             last = current;