diff --git a/regression/cbmc/graphml_witness1/main.c b/regression/cbmc/graphml_witness1/main.c
new file mode 100644
index 00000000000..585f39f87cf
--- /dev/null
+++ b/regression/cbmc/graphml_witness1/main.c
@@ -0,0 +1,34 @@
+extern int __VERIFIER_nondet_int(void);
+
+typedef enum {
+  LIST_BEG,
+  LIST_END
+} end_point_t;
+
+typedef enum {
+  ITEM_PREV,
+  ITEM_NEXT
+} direction_t;
+
+void remove_one(end_point_t from)
+{
+  const direction_t next_field = (LIST_BEG == from) ? ITEM_NEXT : ITEM_PREV;
+}
+
+end_point_t rand_end_point(void)
+{
+  _Bool choice;
+  if (choice)
+    return LIST_BEG;
+  else
+    return LIST_END;
+}
+
+int main()
+{
+  remove_one(rand_end_point());
+
+  __CPROVER_assert(0, "");
+
+  return 0;
+}
diff --git a/regression/cbmc/graphml_witness1/test.desc b/regression/cbmc/graphml_witness1/test.desc
new file mode 100644
index 00000000000..9e7f5b42724
--- /dev/null
+++ b/regression/cbmc/graphml_witness1/test.desc
@@ -0,0 +1,78 @@
+CORE
+main.c
+--graphml-witness -
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+<graphml xmlns="http://graphml.graphdrawing.org/xmlns" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
+  <key attr.name="invariant" attr.type="string" for="node" id="invariant"/>
+  <key attr.name="invariant.scope" attr.type="string" for="node" id="invariant.scope"/>
+  <key attr.name="nodeType" attr.type="string" for="node" id="nodetype">
+    <default>path</default>
+  </key>
+  <key attr.name="isFrontierNode" attr.type="boolean" for="node" id="frontier">
+    <default>false</default>
+  </key>
+  <key attr.name="isViolationNode" attr.type="boolean" for="node" id="violation">
+    <default>false</default>
+  </key>
+  <key attr.name="isEntryNode" attr.type="boolean" for="node" id="entry">
+    <default>false</default>
+  </key>
+  <key attr.name="isSinkNode" attr.type="boolean" for="node" id="sink">
+    <default>false</default>
+  </key>
+  <key attr.name="enterLoopHead" attr.type="boolean" for="edge" id="enterLoopHead">
+    <default>false</default>
+  </key>
+  <key attr.name="threadNumber" attr.type="int" for="node" id="thread">
+    <default>0</default>
+  </key>
+  <key attr.name="sourcecodeLanguage" attr.type="string" for="graph" id="sourcecodelang"/>
+  <key attr.name="programFile" attr.type="string" for="graph" id="programfile"/>
+  <key attr.name="programHash" attr.type="string" for="graph" id="programhash"/>
+  <key attr.name="specification" attr.type="string" for="graph" id="specification"/>
+  <key attr.name="architecture" attr.type="string" for="graph" id="architecture"/>
+  <key attr.name="producer" attr.type="string" for="graph" id="producer"/>
+  <key attr.name="sourcecode" attr.type="string" for="edge" id="sourcecode"/>
+  <key attr.name="startline" attr.type="int" for="edge" id="startline"/>
+  <key attr.name="control" attr.type="string" for="edge" id="control"/>
+  <key attr.name="assumption" attr.type="string" for="edge" id="assumption"/>
+  <key attr.name="assumption.resultfunction" attr.type="string" for="edge" id="assumption.resultfunction"/>
+  <key attr.name="assumption.scope" attr.type="string" for="edge" id="assumption.scope"/>
+  <key attr.name="enterFunction" attr.type="string" for="edge" id="enterFunction"/>
+  <key attr.name="returnFromFunction" attr.type="string" for="edge" id="returnFrom"/>
+  <key attr.name="witness-type" attr.type="string" for="graph" id="witness-type"/>
+  <graph edgedefault="directed">
+    <data key="sourcecodelang">C</data>
+    <node id="sink"/>
+    <node id="33.22">
+      <data key="entry">true</data>
+    </node>
+    <edge source="33.22" target="4.29">
+      <data key="originfile">main.c</data>
+      <data key="startline">21</data>
+    </edge>
+    <node id="4.29"/>
+    <edge source="4.29" target="29.31">
+      <data key="originfile">main.c</data>
+      <data key="startline">29</data>
+      <data key="assumption.scope">main</data>
+    </edge>
+    <node id="29.31"/>
+    <edge source="29.31" target="5.33">
+      <data key="originfile">main.c</data>
+      <data key="startline">15</data>
+      <data key="assumption.scope">remove_one</data>
+    </edge>
+    <node id="5.33">
+      <data key="violation">true</data>
+    </node>
+    <edge source="5.33" target="sink">
+      <data key="originfile">main.c</data>
+      <data key="startline">31</data>
+    </edge>
+  </graph>
+</graphml>
+--
+^warning: ignoring
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index 4982c1e38b3..ba970e659c8 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -25,7 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/xml_goto_trace.h>
 #include <goto-programs/json_goto_trace.h>
-#include <goto-programs/graphml_goto_trace.h>
+#include <goto-programs/graphml_witness.h>
 
 #include <goto-symex/build_goto_trace.h>
 #include <goto-symex/slice.h>
@@ -106,20 +106,40 @@ void bmct::error_trace()
     }
     break;
   }
+}
 
-  const std::string graphml=options.get_option("graphml-cex");
-  if(!graphml.empty())
-  {
-    graphmlt cex_graph;
-    convert(ns, goto_trace, cex_graph);
+/*******************************************************************\
 
-    if(graphml=="-")
-      write_graphml(cex_graph, std::cout);
-    else
-    {
-      std::ofstream out(graphml);
-      write_graphml(cex_graph, out);
-    }
+Function: bmct::output_graphml
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: outputs witnesses in graphml format
+
+\*******************************************************************/
+
+void bmct::output_graphml(
+  resultt result,
+  const goto_functionst &goto_functions)
+{
+  const std::string graphml=options.get_option("graphml-witness");
+  if(graphml.empty())
+    return;
+
+  graphml_witnesst graphml_witness(ns);
+  if(result==UNSAFE)
+    graphml_witness(safety_checkert::error_trace);
+  else
+    return;
+
+  if(graphml=="-")
+    write_graphml(graphml_witness.graph(), std::cout);
+  else
+  {
+    std::ofstream out(graphml);
+    write_graphml(graphml_witness.graph(), out);
   }
 }
 
@@ -294,79 +314,77 @@ void bmct::show_program()
 
   std::cout << "\n" << "Program constraints:" << "\n";
 
-  for(symex_target_equationt::SSA_stepst::const_iterator
-      it=equation.SSA_steps.begin();
-      it!=equation.SSA_steps.end(); it++)
+  for(const auto &step : equation.SSA_steps)
   {
-    std::cout << "// " << it->source.pc->location_number << " ";
-    std::cout << it->source.pc->source_location.as_string() << "\n";
+    std::cout << "// " << step.source.pc->location_number << " ";
+    std::cout << step.source.pc->source_location.as_string() << "\n";
 
-    if(it->is_assignment())
+    if(step.is_assignment())
     {
       std::string string_value;
-      languages.from_expr(it->cond_expr, string_value);
+      languages.from_expr(step.cond_expr, string_value);
       std::cout << "(" << count << ") " << string_value << "\n";
 
-      if(!it->guard.is_true())
+      if(!step.guard.is_true())
       {
-        languages.from_expr(it->guard, string_value);
+        languages.from_expr(step.guard, string_value);
         std::cout << std::string(i2string(count).size()+3, ' ');
         std::cout << "guard: " << string_value << "\n";
       }
 
       count++;
     }
-    else if(it->is_assert())
+    else if(step.is_assert())
     {
       std::string string_value;
-      languages.from_expr(it->cond_expr, string_value);
+      languages.from_expr(step.cond_expr, string_value);
       std::cout << "(" << count << ") ASSERT("
                 << string_value <<") " << "\n";
 
-      if(!it->guard.is_true())
+      if(!step.guard.is_true())
       {
-        languages.from_expr(it->guard, string_value);
+        languages.from_expr(step.guard, string_value);
         std::cout << std::string(i2string(count).size()+3, ' ');
         std::cout << "guard: " << string_value << "\n";
       }
 
       count++;
     }
-    else if(it->is_assume())
+    else if(step.is_assume())
     {
       std::string string_value;
-      languages.from_expr(it->cond_expr, string_value);
+      languages.from_expr(step.cond_expr, string_value);
       std::cout << "(" << count << ") ASSUME("
                 << string_value <<") " << "\n";
 
-      if(!it->guard.is_true())
+      if(!step.guard.is_true())
       {
-        languages.from_expr(it->guard, string_value);
+        languages.from_expr(step.guard, string_value);
         std::cout << std::string(i2string(count).size()+3, ' ');
         std::cout << "guard: " << string_value << "\n";
       }
 
       count++;
     }
-    else if(it->is_constraint())
+    else if(step.is_constraint())
     {
       std::string string_value;
-      languages.from_expr(it->cond_expr, string_value);
+      languages.from_expr(step.cond_expr, string_value);
       std::cout << "(" << count << ") CONSTRAINT("
                 << string_value <<") " << "\n";
 
       count++;
     }
-    else if(it->is_shared_read() || it->is_shared_write())
+    else if(step.is_shared_read() || step.is_shared_write())
     {
       std::string string_value;
-      languages.from_expr(it->ssa_lhs, string_value);
-      std::cout << "(" << count << ") SHARED_" << (it->is_shared_write()?"WRITE":"READ") << "("
+      languages.from_expr(step.ssa_lhs, string_value);
+      std::cout << "(" << count << ") SHARED_" << (step.is_shared_write()?"WRITE":"READ") << "("
                 << string_value <<") " << "\n";
 
-      if(!it->guard.is_true())
+      if(!step.guard.is_true())
       {
-        languages.from_expr(it->guard, string_value);
+        languages.from_expr(step.guard, string_value);
         std::cout << std::string(i2string(count).size()+3, ' ');
         std::cout << "guard: " << string_value << "\n";
       }
@@ -611,6 +629,7 @@ safety_checkert::resultt bmct::stop_on_fail(
           dynamic_cast<bv_cbmct &>(prop_conv), equation, ns);
 
       error_trace();
+      output_graphml(UNSAFE, goto_functions);
     }
 
     report_failure();
diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h
index 7a396fecede..4a2f683b028 100644
--- a/src/cbmc/bmc.h
+++ b/src/cbmc/bmc.h
@@ -103,7 +103,10 @@ class bmct:public safety_checkert
   virtual void report_failure();
 
   virtual void error_trace();
-
+  void output_graphml(
+    resultt result,
+    const goto_functionst &goto_functions);
+  
   bool cover(
     const goto_functionst &goto_functions,
     const optionst::value_listt &criteria);
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 09f2f17812d..de1b7060898 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -454,8 +454,12 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("outfile"))
     options.set_option("outfile", cmdline.get_value("outfile"));
 
-  if(cmdline.isset("graphml-cex"))
-    options.set_option("graphml-cex", cmdline.get_value("graphml-cex"));
+  if(cmdline.isset("graphml-witness"))
+  {
+    options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));
+    options.set_option("stop-on-fail", true);
+    options.set_option("trace", true);
+  }
 }
 
 /*******************************************************************\
@@ -1170,7 +1174,7 @@ void cbmc_parse_optionst::help()
     " --unwinding-assertions       generate unwinding assertions\n"
     " --partial-loops              permit paths with partial loops\n"
     " --no-pretty-names            do not simplify identifiers\n"
-    " --graphml-cex filename       write the counterexample in GraphML format to filename\n"
+    " --graphml-witness filename   write the witness in GraphML format to filename\n"
     "\n"
     "Backend options:\n"
     " --dimacs                     generate CNF in DIMACS format\n"
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index 1a4b9477cfd..16ea202ba8c 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -53,7 +53,7 @@ class optionst;
   "(arrays-uf-always)(arrays-uf-never)" \
   "(string-abstraction)(no-arch)(arch):" \
   "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
-  "(graphml-cex):" \
+  "(graphml-witness):" \
   "(localize-faults)(localize-faults-method):" \
   "(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear
 
diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile
index 0b0119112f2..932508b0edf 100644
--- a/src/goto-programs/Makefile
+++ b/src/goto-programs/Makefile
@@ -15,7 +15,7 @@ SRC = goto_convert.cpp goto_convert_function_call.cpp \
       compute_called_functions.cpp link_to_library.cpp \
       remove_returns.cpp osx_fat_reader.cpp remove_complex.cpp \
       goto_trace.cpp xml_goto_trace.cpp vcd_goto_trace.cpp \
-      graphml_goto_trace.cpp remove_virtual_functions.cpp \
+      graphml_witness.cpp remove_virtual_functions.cpp \
       class_hierarchy.cpp show_goto_functions.cpp get_goto_model.cpp
 
 INCLUDES= -I ..
diff --git a/src/goto-programs/graphml_goto_trace.h b/src/goto-programs/graphml_goto_trace.h
deleted file mode 100644
index d9b5e1787fd..00000000000
--- a/src/goto-programs/graphml_goto_trace.h
+++ /dev/null
@@ -1,23 +0,0 @@
-/*******************************************************************\
-
-Module: Traces of GOTO Programs
-
-Author: Daniel Kroening
-
-Date: January 2015
-
-\*******************************************************************/
-
-#ifndef CPROVER_GOTO_PROGRAMS_GRAPHML_GOTO_TRACE_H
-#define CPROVER_GOTO_PROGRAMS_GRAPHML_GOTO_TRACE_H
-
-#include <xmllang/graphml.h>
-
-#include "goto_trace.h"
-
-void convert(
-  const namespacet &ns,
-  const goto_tracet &goto_trace,
-  graphmlt &graphml);
-
-#endif
diff --git a/src/goto-programs/graphml_goto_trace.cpp b/src/goto-programs/graphml_witness.cpp
similarity index 93%
rename from src/goto-programs/graphml_goto_trace.cpp
rename to src/goto-programs/graphml_witness.cpp
index dc127cfb33b..f5236227de6 100644
--- a/src/goto-programs/graphml_goto_trace.cpp
+++ b/src/goto-programs/graphml_witness.cpp
@@ -1,11 +1,9 @@
 /*******************************************************************\
 
-Module: Traces of GOTO Programs
+Module: Witnesses for Traces and Proofs
 
 Author: Daniel Kroening
 
-  Date: January 2015
-
 \*******************************************************************/
 
 #include <util/config.h>
@@ -14,11 +12,11 @@ Author: Daniel Kroening
 #include <util/prefix.h>
 #include <util/ssa_expr.h>
 
-#include "graphml_goto_trace.h"
+#include "graphml_witness.h"
 
 /*******************************************************************\
 
-Function: remove_l0_l1
+Function: graphml_witnesst::remove_l0_l1
 
   Inputs:
 
@@ -28,7 +26,7 @@ Function: remove_l0_l1
 
 \*******************************************************************/
 
-static void remove_l0_l1(exprt &expr)
+void graphml_witnesst::remove_l0_l1(exprt &expr)
 {
   if(expr.id()==ID_symbol)
   {
@@ -56,7 +54,7 @@ static void remove_l0_l1(exprt &expr)
 
 /*******************************************************************\
 
-Function: convert_assign_rec
+Function: graphml_witnesst::convert_assign_rec
 
   Inputs:
 
@@ -66,8 +64,7 @@ Function: convert_assign_rec
 
 \*******************************************************************/
 
-static std::string convert_assign_rec(
-  const namespacet &ns,
+std::string graphml_witnesst::convert_assign_rec(
   const irep_idt &identifier,
   const code_assignt &assign)
 {
@@ -86,7 +83,7 @@ static std::string convert_assign_rec(
           from_integer(i++, signedbv_typet(config.ansi_c.pointer_width)),
           type.subtype());
       if(!result.empty()) result+=' ';
-      result+=convert_assign_rec(ns, identifier, code_assignt(index, *it));
+      result+=convert_assign_rec(identifier, code_assignt(index, *it));
     }
   }
   else if(assign.rhs().id()==ID_struct ||
@@ -116,7 +113,7 @@ static std::string convert_assign_rec(
           c_it->get_name(),
           it->type());
       if(!result.empty()) result+=' ';
-      result+=convert_assign_rec(ns, identifier, code_assignt(member, *it));
+      result+=convert_assign_rec(identifier, code_assignt(member, *it));
       ++c_it;
     }
   }
@@ -134,20 +131,17 @@ static std::string convert_assign_rec(
 
 /*******************************************************************\
 
-Function: convert
+Function: graphml_witnesst::operator()
 
   Inputs:
 
  Outputs:
 
- Purpose:
+ Purpose: counterexample witness
 
 \*******************************************************************/
 
-void convert(
-  const namespacet &ns,
-  const goto_tracet &goto_trace,
-  graphmlt &graphml)
+void graphml_witnesst::operator()(const goto_tracet &goto_trace)
 {
   const graphmlt::node_indext sink=graphml.add_node();
   graphml[sink].node_name="sink";
@@ -257,7 +251,7 @@ void convert(
           xmlt &val=edge.new_element("data");
           val.set_attribute("key", "assumption");
           code_assignt assign(it->lhs_object, it->lhs_object_value);
-          val.data=convert_assign_rec(ns, identifier, assign);
+          val.data=convert_assign_rec(identifier, assign);
 
           xmlt &val_s=edge.new_element("data");
           val_s.set_attribute("key", "assumption.scope");
diff --git a/src/goto-programs/graphml_witness.h b/src/goto-programs/graphml_witness.h
new file mode 100644
index 00000000000..412091a0c64
--- /dev/null
+++ b/src/goto-programs/graphml_witness.h
@@ -0,0 +1,42 @@
+/*******************************************************************\
+
+Module: Witnesses for Traces and Proofs
+
+Author: Daniel Kroening
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_PROGRAMS_GRAPHML_WITNESS_H
+#define CPROVER_GOTO_PROGRAMS_GRAPHML_WITNESS_H
+
+#include <xmllang/graphml.h>
+
+#include "goto_trace.h"
+
+class graphml_witnesst
+{
+public:
+  explicit graphml_witnesst(const namespacet &_ns)
+    : ns(_ns)
+  {
+  }
+
+  void operator()(const goto_tracet &goto_trace);
+
+  inline const graphmlt &graph()
+  {
+    return graphml;
+  }
+
+protected:
+  const namespacet &ns;
+  graphmlt graphml;
+
+  void remove_l0_l1(exprt &expr);
+  std::string convert_assign_rec(
+    const irep_idt &identifier,
+    const code_assignt &assign);
+
+};
+
+#endif
diff --git a/src/xmllang/graphml.cpp b/src/xmllang/graphml.cpp
index 343ce2d7bec..1a8530f7ae0 100644
--- a/src/xmllang/graphml.cpp
+++ b/src/xmllang/graphml.cpp
@@ -279,62 +279,37 @@ bool write_graphml(const graphmlt &src, std::ostream &os)
   graphml.set_attribute("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance");
   graphml.set_attribute("xmlns", "http://graphml.graphdrawing.org/xmlns");
 
-  // <key attr.name="assumption" attr.type="string" for="edge" id="assumption"/>
-  {
-    xmlt &key=graphml.new_element("key");
-    key.set_attribute("attr.name", "assumption");
-    key.set_attribute("attr.type", "string");
-    key.set_attribute("for", "edge");
-    key.set_attribute("id", "assumption");
-  }
-
-  // <key attr.name="sourcecode" attr.type="string" for="edge" id="sourcecode"/>
+  // <key attr.name="originFileName" attr.type="string" for="edge"
+  //      id="originfile">
+  //   <default>"&lt;command-line&gt;"</default>
+  // </key>
   {
     xmlt &key=graphml.new_element("key");
-    key.set_attribute("attr.name", "sourcecode");
+    key.set_attribute("attr.name", "originFileName");
     key.set_attribute("attr.type", "string");
     key.set_attribute("for", "edge");
-    key.set_attribute("id", "sourcecode");
-  }
+    key.set_attribute("id", "originfile");
 
-  // <key attr.name="sourcecodeLanguage" attr.type="string" for="graph" id="sourcecodelang"/>
-  {
-    xmlt &key=graphml.new_element("key");
-    key.set_attribute("attr.name", "sourcecodeLanguage");
-    key.set_attribute("attr.type", "string");
-    key.set_attribute("for", "graph");
-    key.set_attribute("id", "sourcecodelang");
+    key.new_element("default").data="<command-line>";
   }
 
-  // <key attr.name="control" attr.type="string" for="edge" id="control"/>
+  // <key attr.name="invariant" attr.type="string" for="node" id="invariant"/>
   {
     xmlt &key=graphml.new_element("key");
-    key.set_attribute("attr.name", "control");
+    key.set_attribute("attr.name", "invariant");
     key.set_attribute("attr.type", "string");
-    key.set_attribute("for", "edge");
-    key.set_attribute("id", "control");
-  }
-
-  // <key attr.name="startline" attr.type="int" for="edge" id="startline"/>
-  {
-    xmlt &key=graphml.new_element("key");
-    key.set_attribute("attr.name", "startline");
-    key.set_attribute("attr.type", "int");
-    key.set_attribute("for", "edge");
-    key.set_attribute("id", "startline");
+    key.set_attribute("for", "node");
+    key.set_attribute("id", "invariant");
   }
 
-  // <key attr.name="originFileName" attr.type="string" for="edge" id="originfile">
-  //     <default>"&lt;command-line&gt;"</default>
-  // </key>
+  //<key attr.name="invariant.scope" attr.type="string" for="node"
+  //     id="invariant.scope"/>
   {
     xmlt &key=graphml.new_element("key");
-    key.set_attribute("attr.name", "originFileName");
+    key.set_attribute("attr.name", "invariant.scope");
     key.set_attribute("attr.type", "string");
-    key.set_attribute("for", "edge");
-    key.set_attribute("id", "originfile");
-
-    key.new_element("default").data="<command-line>";
+    key.set_attribute("for", "node");
+    key.set_attribute("id", "invariant.scope");
   }
 
   // <key attr.name="nodeType" attr.type="string" for="node" id="nodetype">
@@ -350,7 +325,8 @@ bool write_graphml(const graphmlt &src, std::ostream &os)
     key.new_element("default").data="path";
   }
 
-  // <key attr.name="isFrontierNode" attr.type="boolean" for="node" id="frontier">
+  // <key attr.name="isFrontierNode" attr.type="boolean" for="node"
+  //      id="frontier">
   //     <default>false</default>
   // </key>
   {
@@ -363,7 +339,8 @@ bool write_graphml(const graphmlt &src, std::ostream &os)
     key.new_element("default").data="false";
   }
 
-  // <key attr.name="isViolationNode" attr.type="boolean" for="node" id="violation">
+  // <key attr.name="isViolationNode" attr.type="boolean" for="node"
+  //      id="violation">
   //     <default>false</default>
   // </key>
   {
@@ -402,7 +379,150 @@ bool write_graphml(const graphmlt &src, std::ostream &os)
     key.new_element("default").data="false";
   }
 
-  // <key attr.name="enterFunction" attr.type="string" for="edge" id="enterFunction"/>
+  // <key attr.name="enterLoopHead" attr.type="boolean" for="edge"
+  //      id="enterLoopHead">
+  //   <default>false</default>
+  // </key>
+  {
+    xmlt &key=graphml.new_element("key");
+    key.set_attribute("attr.name", "enterLoopHead");
+    key.set_attribute("attr.type", "boolean");
+    key.set_attribute("for", "edge");
+    key.set_attribute("id", "enterLoopHead");
+
+    key.new_element("default").data="false";
+  }
+
+  // <key attr.name="threadId" attr.type="string" for="edge" id="threadId"/>
+  // TODO: format for multi-threaded programs not defined yet
+  {
+    xmlt &key=graphml.new_element("key");
+    key.set_attribute("attr.name", "threadNumber");
+    key.set_attribute("attr.type", "int");
+    key.set_attribute("for", "node");
+    key.set_attribute("id", "thread");
+
+    key.new_element("default").data="0";
+  }
+
+  // <key attr.name="sourcecodeLanguage" attr.type="string" for="graph"
+  //      id="sourcecodelang"/>
+  {
+    xmlt &key=graphml.new_element("key");
+    key.set_attribute("attr.name", "sourcecodeLanguage");
+    key.set_attribute("attr.type", "string");
+    key.set_attribute("for", "graph");
+    key.set_attribute("id", "sourcecodelang");
+  }
+
+  // <key attr.name="programFile" attr.type="string" for="graph"
+  //      id="programfile"/>
+  {
+    xmlt &key=graphml.new_element("key");
+    key.set_attribute("attr.name", "programFile");
+    key.set_attribute("attr.type", "string");
+    key.set_attribute("for", "graph");
+    key.set_attribute("id", "programfile");
+  }
+
+  // <key attr.name="programHash" attr.type="string" for="graph"
+  //      id="programhash"/>
+  {
+    xmlt &key=graphml.new_element("key");
+    key.set_attribute("attr.name", "programHash");
+    key.set_attribute("attr.type", "string");
+    key.set_attribute("for", "graph");
+    key.set_attribute("id", "programhash");
+  }
+
+  // <key attr.name="specification" attr.type="string" for="graph"
+  //      id="specification"/>
+  {
+    xmlt &key=graphml.new_element("key");
+    key.set_attribute("attr.name", "specification");
+    key.set_attribute("attr.type", "string");
+    key.set_attribute("for", "graph");
+    key.set_attribute("id", "specification");
+  }
+
+  // <key attr.name="architecture" attr.type="string" for="graph"
+  //      id="architecture"/>
+  {
+    xmlt &key=graphml.new_element("key");
+    key.set_attribute("attr.name", "architecture");
+    key.set_attribute("attr.type", "string");
+    key.set_attribute("for", "graph");
+    key.set_attribute("id", "architecture");
+  }
+
+  // <key attr.name="producer" attr.type="string" for="graph"
+  //      id="producer"/>
+  {
+    xmlt &key=graphml.new_element("key");
+    key.set_attribute("attr.name", "producer");
+    key.set_attribute("attr.type", "string");
+    key.set_attribute("for", "graph");
+    key.set_attribute("id", "producer");
+  }
+
+  // <key attr.name="sourcecode" attr.type="string" for="edge" id="sourcecode"/>
+  {
+    xmlt &key=graphml.new_element("key");
+    key.set_attribute("attr.name", "sourcecode");
+    key.set_attribute("attr.type", "string");
+    key.set_attribute("for", "edge");
+    key.set_attribute("id", "sourcecode");
+  }
+
+  // <key attr.name="startline" attr.type="int" for="edge" id="startline"/>
+  {
+    xmlt &key=graphml.new_element("key");
+    key.set_attribute("attr.name", "startline");
+    key.set_attribute("attr.type", "int");
+    key.set_attribute("for", "edge");
+    key.set_attribute("id", "startline");
+  }
+
+  // <key attr.name="control" attr.type="string" for="edge" id="control"/>
+  {
+    xmlt &key=graphml.new_element("key");
+    key.set_attribute("attr.name", "control");
+    key.set_attribute("attr.type", "string");
+    key.set_attribute("for", "edge");
+    key.set_attribute("id", "control");
+  }
+
+  // <key attr.name="assumption" attr.type="string" for="edge" id="assumption"/>
+  {
+    xmlt &key=graphml.new_element("key");
+    key.set_attribute("attr.name", "assumption");
+    key.set_attribute("attr.type", "string");
+    key.set_attribute("for", "edge");
+    key.set_attribute("id", "assumption");
+  }
+
+  // <key attr.name="assumption.resultfunction" attr.type="string" for="edge"
+  //      id="assumption.resultfunction"/>
+  {
+    xmlt &key=graphml.new_element("key");
+    key.set_attribute("attr.name", "assumption.resultfunction");
+    key.set_attribute("attr.type", "string");
+    key.set_attribute("for", "edge");
+    key.set_attribute("id", "assumption.resultfunction");
+  }
+
+  // <key attr.name="assumption.scope" attr.type="string" for="edge"
+  //      id="assumption.scope"/>
+  {
+    xmlt &key=graphml.new_element("key");
+    key.set_attribute("attr.name", "assumption.scope");
+    key.set_attribute("attr.type", "string");
+    key.set_attribute("for", "edge");
+    key.set_attribute("id", "assumption.scope");
+  }
+
+  // <key attr.name="enterFunction" attr.type="string" for="edge"
+  //      id="enterFunction"/>
   {
     xmlt &key=graphml.new_element("key");
     key.set_attribute("attr.name", "enterFunction");
@@ -411,7 +531,8 @@ bool write_graphml(const graphmlt &src, std::ostream &os)
     key.set_attribute("id", "enterFunction");
   }
 
-  // <key attr.name="returnFromFunction" attr.type="string" for="edge" id="returnFrom"/>
+  // <key attr.name="returnFromFunction" attr.type="string" for="edge"
+  //      id="returnFrom"/>
   {
     xmlt &key=graphml.new_element("key");
     key.set_attribute("attr.name", "returnFromFunction");
@@ -420,17 +541,16 @@ bool write_graphml(const graphmlt &src, std::ostream &os)
     key.set_attribute("id", "returnFrom");
   }
 
+  // <key attr.name="witness-type" attr.type="string" for="graph"
+  //      id="witness-type"/>
   {
     xmlt &key=graphml.new_element("key");
-    key.set_attribute("attr.name", "threadNumber");
-    key.set_attribute("attr.type", "int");
-    key.set_attribute("for", "node");
-    key.set_attribute("id", "thread");
-
-    key.new_element("default").data="0";
+    key.set_attribute("attr.name", "witness-type");
+    key.set_attribute("attr.type", "string");
+    key.set_attribute("for", "graph");
+    key.set_attribute("id", "witness-type");
   }
 
-
   xmlt &graph=graphml.new_element("graph");
   graph.set_attribute("edgedefault", "directed");