From fbe06253f70519dacd26d4993f95fafc4b83543b Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 1 Dec 2020 23:45:47 +0000
Subject: [PATCH 1/2] GraphML witness: creationtime is a graph attribute

SV-COMP requires that this is set, which we take care of in your sv-comp
wrapper script.
---
 src/xmllang/graphml.cpp | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/xmllang/graphml.cpp b/src/xmllang/graphml.cpp
index a734be72dc0..2604bf27627 100644
--- a/src/xmllang/graphml.cpp
+++ b/src/xmllang/graphml.cpp
@@ -402,6 +402,16 @@ bool write_graphml(const graphmlt &src, std::ostream &os)
     key.set_attribute("id", "producer");
   }
 
+  // <key attr.name="creationtime" attr.type="string" for="graph"
+  //      id="creationtime"/>
+  {
+    xmlt &key = graphml.new_element("key");
+    key.set_attribute("attr.name", "creationtime");
+    key.set_attribute("attr.type", "string");
+    key.set_attribute("for", "graph");
+    key.set_attribute("id", "creationtime");
+  }
+
   // <key attr.name="startline" attr.type="int" for="edge" id="startline"/>
   {
     xmlt &key=graphml.new_element("key");

From 50868cafcca78a93f5751992fa704fcd1fde5fd9 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 2 Dec 2020 22:23:16 +0000
Subject: [PATCH 2/2] GraphML witnesses: cyclehead is a node attribute

The witness linter enforces the spec spelled out in
https://github.com/sosy-lab/sv-witnesses/blob/master/termination/README.md.
---
 src/xmllang/graphml.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/xmllang/graphml.cpp b/src/xmllang/graphml.cpp
index 2604bf27627..a527a5790c8 100644
--- a/src/xmllang/graphml.cpp
+++ b/src/xmllang/graphml.cpp
@@ -305,7 +305,7 @@ bool write_graphml(const graphmlt &src, std::ostream &os)
     key.new_element("default").data="false";
   }
 
-  // <key attr.name="cyclehead" attr.type="boolean" for="edge"
+  // <key attr.name="cyclehead" attr.type="boolean" for="node"
   //      id="cyclehead">
   //   <default>false</default>
   // </key>
@@ -313,7 +313,7 @@ bool write_graphml(const graphmlt &src, std::ostream &os)
     xmlt &key = graphml.new_element("key");
     key.set_attribute("attr.name", "cyclehead");
     key.set_attribute("attr.type", "boolean");
-    key.set_attribute("for", "edge");
+    key.set_attribute("for", "node");
     key.set_attribute("id", "cyclehead");
 
     key.new_element("default").data = "false";