diff --git a/regression/cbmc/graphml_witness1/test.desc b/regression/cbmc/graphml_witness1/test.desc
index cb22eaba5d0..d0428e2738d 100644
--- a/regression/cbmc/graphml_witness1/test.desc
+++ b/regression/cbmc/graphml_witness1/test.desc
@@ -7,34 +7,21 @@ main.c
 <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"/>
@@ -45,7 +32,6 @@ main.c
   <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="[0-9\.]*">
       <data key="entry">true</data>
     </node>
@@ -57,7 +43,7 @@ main.c
     <edge source="[0-9\.]*" target="[0-9\.]*">
       <data key="originfile">main.c</data>
       <data key="startline">29</data>
-      <data key="assumption.scope">main</data>
+      <data key="assumption.scope">remove_one</data>
     </edge>
     <node id="[0-9\.]*"/>
     <edge source="[0-9\.]*" target="[0-9\.]*">
@@ -68,10 +54,6 @@ main.c
     <node id="[0-9\.]*">
       <data key="violation">true</data>
     </node>
-    <edge source="[0-9\.]*" target="sink">
-      <data key="originfile">main.c</data>
-      <data key="startline">31</data>
-    </edge>
   </graph>
 </graphml>
 --
diff --git a/regression/cbmc/graphml_witness2/main.c b/regression/cbmc/graphml_witness2/main.c
new file mode 100644
index 00000000000..ebe307a73c0
--- /dev/null
+++ b/regression/cbmc/graphml_witness2/main.c
@@ -0,0 +1,31 @@
+extern void __VERIFIER_error();
+
+static float one(float *foo)
+{
+  return *foo;
+}
+
+static float two(float *foo)
+{
+  return *foo;
+}
+
+float x = 0;
+
+void step()
+{
+  x = one(0);
+}
+
+int main(void)
+{
+  while(1)
+  {
+    step();
+    if(x == 0)
+    {
+      __VERIFIER_error();
+    }
+  }
+  return 0;
+}
diff --git a/regression/cbmc/graphml_witness2/test.desc b/regression/cbmc/graphml_witness2/test.desc
new file mode 100644
index 00000000000..6a97a4749fb
--- /dev/null
+++ b/regression/cbmc/graphml_witness2/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--graphml-witness - --unwindset main.0:1 --unwinding-assertions
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+<data key="assumption">foo = \(\(float \*\)0\);</data>
+<data key="assumption.scope">one</data>
+--
+^warning: ignoring
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index da3e16c4d11..077c43b2b39 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -42,7 +42,8 @@ expr2c_configurationt expr2c_configurationt::default_configuration
   true,
   true,
   "TRUE",
-  "FALSE"
+  "FALSE",
+  true
 };
 
 expr2c_configurationt expr2c_configurationt::clean_configuration
@@ -51,7 +52,8 @@ expr2c_configurationt expr2c_configurationt::clean_configuration
   false,
   false,
   "1",
-  "0"
+  "0",
+  false
 };
 
 // clang-format on
@@ -1857,14 +1859,39 @@ std::string expr2ct::convert_constant(
     else if(dest.size()==4 &&
             (dest[0]=='+' || dest[0]=='-'))
     {
-      if(dest=="+inf")
-        dest="+INFINITY";
-      else if(dest=="-inf")
-        dest="-INFINITY";
-      else if(dest=="+NaN")
-        dest="+NAN";
-      else if(dest=="-NaN")
-        dest="-NAN";
+      if(configuration.use_library_macros)
+      {
+        if(dest == "+inf")
+          dest = "+INFINITY";
+        else if(dest == "-inf")
+          dest = "-INFINITY";
+        else if(dest == "+NaN")
+          dest = "+NAN";
+        else if(dest == "-NaN")
+          dest = "-NAN";
+      }
+      else
+      {
+        // ANSI-C: double is default; float/long-double require annotation
+        std::string suffix = "";
+        if(src.type() == float_type())
+          suffix = "f";
+        else if(
+          src.type() == long_double_type() &&
+          double_type() != long_double_type())
+        {
+          suffix = "l";
+        }
+
+        if(dest == "+inf")
+          dest = "(1.0" + suffix + "/0.0" + suffix + ")";
+        else if(dest == "-inf")
+          dest = "(-1.0" + suffix + "/0.0" + suffix + ")";
+        else if(dest == "+NaN")
+          dest = "(0.0" + suffix + "/0.0" + suffix + ")";
+        else if(dest == "-NaN")
+          dest = "(-0.0" + suffix + "/0.0" + suffix + ")";
+      }
     }
   }
   else if(type.id()==ID_fixedbv)
@@ -1885,16 +1912,14 @@ std::string expr2ct::convert_constant(
   }
   else if(type.id()==ID_pointer)
   {
-    if(value==ID_NULL)
-    {
-      dest="NULL";
-      if(type.subtype().id()!=ID_empty)
-        dest="(("+convert(type)+")"+dest+")";
-    }
-    else if(value==std::string(value.size(), '0') &&
-            config.ansi_c.NULL_is_zero)
+    if(
+      value == ID_NULL ||
+      (value == std::string(value.size(), '0') && config.ansi_c.NULL_is_zero))
     {
-      dest="NULL";
+      if(configuration.use_library_macros)
+        dest = "NULL";
+      else
+        dest = "0";
       if(type.subtype().id()!=ID_empty)
         dest="(("+convert(type)+")"+dest+")";
     }
diff --git a/src/ansi-c/expr2c.h b/src/ansi-c/expr2c.h
index 03460c01909..e025a7f8b34 100644
--- a/src/ansi-c/expr2c.h
+++ b/src/ansi-c/expr2c.h
@@ -36,17 +36,22 @@ struct expr2c_configurationt final
   /// This is the string that will be printed for the false boolean expression
   std::string false_string;
 
+  /// This is the string that will be printed for null pointers
+  bool use_library_macros;
+
   expr2c_configurationt(
     const bool include_struct_padding_components,
     const bool print_struct_body_in_type,
     const bool include_array_size,
     const std::string &true_string,
-    const std::string &false_string)
+    const std::string &false_string,
+    const bool use_library_macros)
     : include_struct_padding_components(include_struct_padding_components),
       print_struct_body_in_type(print_struct_body_in_type),
       include_array_size(include_array_size),
       true_string(true_string),
-      false_string(false_string)
+      false_string(false_string),
+      use_library_macros(use_library_macros)
   {
   }
 
diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp
index 4e919938376..c81bbc9ef6d 100644
--- a/src/goto-programs/graphml_witness.cpp
+++ b/src/goto-programs/graphml_witness.cpp
@@ -11,16 +11,31 @@ Author: Daniel Kroening
 
 #include "graphml_witness.h"
 
+#include <util/arith_tools.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
-#include <util/arith_tools.h>
+#include <util/cprover_prefix.h>
+#include <util/pointer_predicates.h>
 #include <util/prefix.h>
 #include <util/ssa_expr.h>
+#include <util/string_container.h>
 
 #include <langapi/language_util.h>
+#include <langapi/mode.h>
+
+#include <ansi-c/expr2c.h>
 
 #include "goto_program.h"
 
+static std::string
+expr_to_string(const namespacet &ns, const irep_idt &id, const exprt &expr)
+{
+  if(get_mode_from_identifier(ns, id) == ID_C)
+    return expr2c(expr, ns, expr2c_configurationt::clean_configuration);
+  else
+    return from_expr(ns, id, expr);
+}
+
 void graphml_witnesst::remove_l0_l1(exprt &expr)
 {
   if(expr.id()==ID_symbol)
@@ -51,9 +66,32 @@ std::string graphml_witnesst::convert_assign_rec(
   const irep_idt &identifier,
   const code_assignt &assign)
 {
+#ifdef USE_DSTRING
+  const auto cit = cache.find({identifier.get_no(), &assign.read()});
+#else
+  const auto cit =
+    cache.find({get_string_container()[id2string(identifier)], &assign.read()});
+#endif
+  if(cit != cache.end())
+    return cit->second;
+
   std::string result;
 
-  if(assign.rhs().id()==ID_array)
+  if(assign.rhs().id() == ID_array_list)
+  {
+    const array_list_exprt &array_list = to_array_list_expr(assign.rhs());
+    const auto &ops = array_list.operands();
+
+    for(std::size_t listidx = 0; listidx != ops.size(); listidx += 2)
+    {
+      const index_exprt index{assign.lhs(), ops[listidx]};
+      if(!result.empty())
+        result += ' ';
+      result +=
+        convert_assign_rec(identifier, code_assignt{index, ops[listidx + 1]});
+    }
+  }
+  else if(assign.rhs().id() == ID_array)
   {
     const array_typet &type = to_array_type(assign.rhs().type());
 
@@ -124,18 +162,57 @@ std::string graphml_witnesst::convert_assign_rec(
         break;
     }
   }
+  else if(assign.rhs().id() == ID_with)
+  {
+    const with_exprt &with_expr = to_with_expr(assign.rhs());
+    const auto &ops = with_expr.operands();
+
+    for(std::size_t i = 1; i < ops.size(); i += 2)
+    {
+      if(!result.empty())
+        result += ' ';
+
+      if(ops[i].id() == ID_member_name)
+      {
+        const member_exprt member{
+          assign.lhs(), ops[i].get(ID_component_name), ops[i + 1].type()};
+        result +=
+          convert_assign_rec(identifier, code_assignt(member, ops[i + 1]));
+      }
+      else
+      {
+        const index_exprt index{assign.lhs(), ops[i]};
+        result +=
+          convert_assign_rec(identifier, code_assignt(index, ops[i + 1]));
+      }
+    }
+  }
   else
   {
     exprt clean_rhs=assign.rhs();
     remove_l0_l1(clean_rhs);
 
-    std::string lhs=from_expr(ns, identifier, assign.lhs());
-    if(lhs.find('$')!=std::string::npos)
+    exprt clean_lhs = assign.lhs();
+    remove_l0_l1(clean_lhs);
+    std::string lhs = expr_to_string(ns, identifier, clean_lhs);
+
+    if(
+      lhs.find("#return_value") != std::string::npos ||
+      (lhs.find('$') != std::string::npos &&
+       has_prefix(lhs, "return_value___VERIFIER_nondet_")))
+    {
       lhs="\\result";
+    }
 
-    result=lhs+" = "+from_expr(ns, identifier, clean_rhs)+";";
+    result = lhs + " = " + expr_to_string(ns, identifier, clean_rhs) + ";";
   }
 
+#ifdef USE_DSTRING
+  cache.insert({{identifier.get_no(), &assign.read()}, result});
+#else
+  cache.insert(
+    {{get_string_container()[id2string(identifier)], &assign.read()}, result});
+#endif
   return result;
 }
 
@@ -169,22 +246,93 @@ static bool filter_out(
      source_location.get_file().empty() ||
      source_location.is_built_in() ||
      source_location.get_line().empty())
+  {
+    const irep_idt id = source_location.get_function();
+    // Do not filter out assertions in functions the name of which starts with
+    // CPROVER_PREFIX, because we need to maintain those as violation nodes:
+    // these are assertions generated, for examples, for memory leaks.
+    if(!has_prefix(id2string(id), CPROVER_PREFIX) || !it->is_assert())
+      return true;
+  }
+
+  return false;
+}
+
+static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix)
+{
+  if(
+    expr.id() == ID_symbol &&
+    has_prefix(id2string(to_symbol_expr(expr).get_identifier()), prefix))
+  {
     return true;
+  }
 
+  forall_operands(it, expr)
+  {
+    if(contains_symbol_prefix(*it, prefix))
+      return true;
+  }
   return false;
 }
 
 /// counterexample witness
 void graphml_witnesst::operator()(const goto_tracet &goto_trace)
 {
+  unsigned int max_thread_idx = 0;
+  bool trace_has_violation = false;
+  for(goto_tracet::stepst::const_iterator it = goto_trace.steps.begin();
+      it != goto_trace.steps.end();
+      ++it)
+  {
+    if(it->thread_nr > max_thread_idx)
+      max_thread_idx = it->thread_nr;
+    if(it->is_assert() && !it->cond_value)
+      trace_has_violation = true;
+  }
+
   graphml.key_values["sourcecodelang"]="C";
 
   const graphmlt::node_indext sink=graphml.add_node();
   graphml[sink].node_name="sink";
-  graphml[sink].thread_nr=0;
   graphml[sink].is_violation=false;
   graphml[sink].has_invariant=false;
 
+  if(max_thread_idx > 0 && trace_has_violation)
+  {
+    std::vector<graphmlt::node_indext> nodes;
+
+    for(unsigned int i = 0; i <= max_thread_idx + 1; ++i)
+    {
+      nodes.push_back(graphml.add_node());
+      graphml[nodes.back()].node_name = "N" + std::to_string(i);
+      graphml[nodes.back()].is_violation = i == max_thread_idx + 1;
+      graphml[nodes.back()].has_invariant = false;
+    }
+
+    for(auto it = nodes.cbegin(); std::next(it) != nodes.cend(); ++it)
+    {
+      xmlt edge("edge");
+      edge.set_attribute("source", graphml[*it].node_name);
+      edge.set_attribute("target", graphml[*std::next(it)].node_name);
+      const auto thread_id = std::distance(nodes.cbegin(), it);
+      xmlt &data = edge.new_element("data");
+      data.set_attribute("key", "createThread");
+      data.data = std::to_string(thread_id);
+      if(thread_id == 0)
+      {
+        xmlt &data = edge.new_element("data");
+        data.set_attribute("key", "enterFunction");
+        data.data = "main";
+      }
+      graphml[*std::next(it)].in[*it].xml_node = edge;
+      graphml[*it].out[*std::next(it)].xml_node = edge;
+    }
+
+    // we do not provide any further details as CPAchecker does not seem to
+    // handle more detailed concurrency witnesses
+    return;
+  }
+
   // step numbers start at 1
   std::vector<std::size_t> step_to_node(goto_trace.steps.size()+1, 0);
 
@@ -223,7 +371,6 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
       std::to_string(it->pc->location_number)+"."+std::to_string(it->step_nr);
     graphml[node].file=source_location.get_file();
     graphml[node].line=source_location.get_line();
-    graphml[node].thread_nr=it->thread_nr;
     graphml[node].is_violation=
       it->type==goto_trace_stept::typet::ASSERT && !it->cond_value;
     graphml[node].has_invariant=false;
@@ -231,6 +378,8 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
     step_to_node[it->step_nr]=node;
   }
 
+  unsigned thread_id = 0;
+
   // build edges
   for(goto_tracet::stepst::const_iterator
       it=goto_trace.steps.begin();
@@ -239,7 +388,8 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
   {
     const std::size_t from=step_to_node[it->step_nr];
 
-    if(from==sink)
+    // no outgoing edges from sinks or violation nodes
+    if(from == sink || graphml[from].is_violation)
     {
       ++it;
       continue;
@@ -262,73 +412,85 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
     case goto_trace_stept::typet::ASSIGNMENT:
     case goto_trace_stept::typet::ASSERT:
     case goto_trace_stept::typet::GOTO:
+    case goto_trace_stept::typet::SPAWN:
+    {
+      xmlt edge(
+        "edge",
+        {{"source", graphml[from].node_name},
+         {"target", graphml[to].node_name}},
+        {});
+
       {
-        xmlt edge(
-          "edge",
-          {{"source", graphml[from].node_name},
-           {"target", graphml[to].node_name}},
-          {});
+        xmlt &data_f = edge.new_element("data");
+        data_f.set_attribute("key", "originfile");
+        data_f.data = id2string(graphml[from].file);
 
-        {
-          xmlt &data_f=edge.new_element("data");
-          data_f.set_attribute("key", "originfile");
-          data_f.data=id2string(graphml[from].file);
+        xmlt &data_l = edge.new_element("data");
+        data_l.set_attribute("key", "startline");
+        data_l.data = id2string(graphml[from].line);
 
-          xmlt &data_l=edge.new_element("data");
-          data_l.set_attribute("key", "startline");
-          data_l.data=id2string(graphml[from].line);
-        }
+        xmlt &data_t = edge.new_element("data");
+        data_t.set_attribute("key", "threadId");
+        data_t.data = std::to_string(it->thread_nr);
+      }
 
-        if(it->type==goto_trace_stept::typet::ASSIGNMENT &&
-           it->full_lhs_value.is_not_nil() &&
-           it->full_lhs.is_not_nil())
+      const auto lhs_object = it->get_lhs_object();
+      if(
+        it->type == goto_trace_stept::typet::ASSIGNMENT &&
+        lhs_object.has_value())
+      {
+        const std::string &lhs_id = id2string(lhs_object->get_identifier());
+        if(lhs_id.find("pthread_create::thread") != std::string::npos)
+        {
+          xmlt &data_t = edge.new_element("data");
+          data_t.set_attribute("key", "createThread");
+          data_t.data = std::to_string(++thread_id);
+        }
+        else if(
+          !contains_symbol_prefix(
+            it->full_lhs_value, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
+          !contains_symbol_prefix(
+            it->full_lhs, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
+          lhs_id.find("thread") == std::string::npos &&
+          lhs_id.find("mutex") == std::string::npos &&
+          (!it->full_lhs_value.is_constant() ||
+           !it->full_lhs_value.has_operands() ||
+           !has_prefix(
+             id2string(it->full_lhs_value.op0().get(ID_value)), "INVALID-")))
         {
-          xmlt &val=edge.new_element("data");
+          xmlt &val = edge.new_element("data");
           val.set_attribute("key", "assumption");
-          val.data = from_expr(ns, it->function_id, it->full_lhs) + " = " +
-                     from_expr(ns, it->function_id, it->full_lhs_value) + ";";
 
-          xmlt &val_s=edge.new_element("data");
+          code_assignt assign{it->full_lhs, it->full_lhs_value};
+          val.data = convert_assign_rec(lhs_id, assign);
+
+          xmlt &val_s = edge.new_element("data");
           val_s.set_attribute("key", "assumption.scope");
-          val_s.data = id2string(it->function_id);
-        }
-        else if(it->type==goto_trace_stept::typet::GOTO &&
-                it->pc->is_goto())
-        {
-          xmlt &val=edge.new_element("data");
-          val.set_attribute("key", "sourcecode");
-          const std::string cond =
-            from_expr(ns, it->function_id, it->cond_expr);
-          const std::string neg_cond =
-            from_expr(ns, it->function_id, not_exprt(it->cond_expr));
-          val.data="["+(it->cond_value ? cond : neg_cond)+"]";
-
-          #if 0
-          xmlt edge2("edge", {
-                     {"source", graphml[from].node_name},
-                     {"target", graphml[sink].node_name}}, {});
-
-          xmlt &data_f2=edge2.new_element("data");
-          data_f2.set_attribute("key", "originfile");
-          data_f2.data=id2string(graphml[from].file);
-
-          xmlt &data_l2=edge2.new_element("data");
-          data_l2.set_attribute("key", "startline");
-          data_l2.data=id2string(graphml[from].line);
-
-          xmlt &val2=edge2.new_element("data");
-          val2.set_attribute("key", "sourcecode");
-          val2.data="["+(it->cond_value ? neg_cond : cond)+"]";
-
-          graphml[sink].in[from].xml_node=edge2;
-          graphml[from].out[sink].xml_node=edge2;
-          #endif
+          irep_idt function_id = it->function_id;
+          const symbolt *symbol_ptr = nullptr;
+          if(!ns.lookup(lhs_id, symbol_ptr) && symbol_ptr->is_parameter)
+          {
+            function_id = lhs_id.substr(0, lhs_id.find("::"));
+          }
+          val_s.data = id2string(function_id);
+
+          if(has_prefix(val.data, "\\result ="))
+          {
+            xmlt &val_f = edge.new_element("data");
+            val_f.set_attribute("key", "assumption.resultfunction");
+            val_f.data = id2string(it->function_id);
+          }
         }
-
-        graphml[to].in[from].xml_node=edge;
-        graphml[from].out[to].xml_node=edge;
       }
+      else if(it->type == goto_trace_stept::typet::GOTO && it->pc->is_goto())
+      {
+      }
+
+      graphml[to].in[from].xml_node = edge;
+      graphml[from].out[to].xml_node = edge;
+
       break;
+    }
 
     case goto_trace_stept::typet::DECL:
     case goto_trace_stept::typet::FUNCTION_CALL:
@@ -339,7 +501,6 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
     case goto_trace_stept::typet::OUTPUT:
     case goto_trace_stept::typet::SHARED_READ:
     case goto_trace_stept::typet::SHARED_WRITE:
-    case goto_trace_stept::typet::SPAWN:
     case goto_trace_stept::typet::MEMORY_BARRIER:
     case goto_trace_stept::typet::ATOMIC_BEGIN:
     case goto_trace_stept::typet::ATOMIC_END:
@@ -361,7 +522,6 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
 
   const graphmlt::node_indext sink=graphml.add_node();
   graphml[sink].node_name="sink";
-  graphml[sink].thread_nr=0;
   graphml[sink].is_violation=false;
   graphml[sink].has_invariant=false;
 
@@ -407,7 +567,6 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
       std::to_string(step_nr);
     graphml[node].file=source_location.get_file();
     graphml[node].line=source_location.get_line();
-    graphml[node].thread_nr=it->source.thread_nr;
     graphml[node].is_violation=false;
     graphml[node].has_invariant=false;
 
@@ -448,49 +607,41 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
     case goto_trace_stept::typet::ASSIGNMENT:
     case goto_trace_stept::typet::ASSERT:
     case goto_trace_stept::typet::GOTO:
+    case goto_trace_stept::typet::SPAWN:
+    {
+      xmlt edge(
+        "edge",
+        {{"source", graphml[from].node_name},
+         {"target", graphml[to].node_name}},
+        {});
+
       {
-        xmlt edge(
-          "edge",
-          {{"source", graphml[from].node_name},
-           {"target", graphml[to].node_name}},
-          {});
+        xmlt &data_f = edge.new_element("data");
+        data_f.set_attribute("key", "originfile");
+        data_f.data = id2string(graphml[from].file);
 
-        {
-          xmlt &data_f=edge.new_element("data");
-          data_f.set_attribute("key", "originfile");
-          data_f.data=id2string(graphml[from].file);
+        xmlt &data_l = edge.new_element("data");
+        data_l.set_attribute("key", "startline");
+        data_l.data = id2string(graphml[from].line);
+      }
 
-          xmlt &data_l=edge.new_element("data");
-          data_l.set_attribute("key", "startline");
-          data_l.data=id2string(graphml[from].line);
-        }
+      if(
+        (it->is_assignment() || it->is_decl()) && it->ssa_rhs.is_not_nil() &&
+        it->ssa_full_lhs.is_not_nil())
+      {
+        irep_idt identifier = it->ssa_lhs.get_object_name();
 
-        if((it->is_assignment() ||
-            it->is_decl()) &&
-           it->ssa_rhs.is_not_nil() &&
-           it->ssa_full_lhs.is_not_nil())
-        {
-          irep_idt identifier=it->ssa_lhs.get_object_name();
+        graphml[to].has_invariant = true;
+        code_assignt assign(it->ssa_lhs, it->ssa_rhs);
+        graphml[to].invariant = convert_assign_rec(identifier, assign);
+        graphml[to].invariant_scope = id2string(it->source.function_id);
+      }
 
-          graphml[to].has_invariant=true;
-          code_assignt assign(it->ssa_full_lhs, it->ssa_rhs);
-          graphml[to].invariant=convert_assign_rec(identifier, assign);
-          graphml[to].invariant_scope = id2string(it->source.function_id);
-        }
-        else if(it->is_goto() &&
-                it->source.pc->is_goto())
-        {
-          xmlt &val=edge.new_element("data");
-          val.set_attribute("key", "sourcecode");
-          const std::string cond =
-            from_expr(ns, it->source.function_id, it->cond_expr);
-          val.data="["+cond+"]";
-        }
+      graphml[to].in[from].xml_node = edge;
+      graphml[from].out[to].xml_node = edge;
 
-        graphml[to].in[from].xml_node=edge;
-        graphml[from].out[to].xml_node=edge;
-      }
       break;
+    }
 
     case goto_trace_stept::typet::DECL:
     case goto_trace_stept::typet::FUNCTION_CALL:
@@ -501,7 +652,6 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
     case goto_trace_stept::typet::OUTPUT:
     case goto_trace_stept::typet::SHARED_READ:
     case goto_trace_stept::typet::SHARED_WRITE:
-    case goto_trace_stept::typet::SPAWN:
     case goto_trace_stept::typet::MEMORY_BARRIER:
     case goto_trace_stept::typet::ATOMIC_BEGIN:
     case goto_trace_stept::typet::ATOMIC_END:
diff --git a/src/goto-programs/graphml_witness.h b/src/goto-programs/graphml_witness.h
index 053eb801146..804dbf84a1a 100644
--- a/src/goto-programs/graphml_witness.h
+++ b/src/goto-programs/graphml_witness.h
@@ -42,6 +42,30 @@ class graphml_witnesst
   std::string convert_assign_rec(
     const irep_idt &identifier,
     const code_assignt &assign);
+
+  template <typename T>
+  static void hash_combine(std::size_t &seed, const T &v)
+  {
+    std::hash<T> hasher;
+    seed ^= hasher(v) + 0x9e3779b9 + (seed << 6) + (seed >> 2);
+  }
+
+  template <typename S, typename T>
+  struct pair_hash // NOLINT(readability/identifiers)
+  {
+    std::size_t operator()(const std::pair<S, T> &v) const
+    {
+      std::size_t seed = 0;
+      hash_combine(seed, v.first);
+      hash_combine(seed, v.second);
+      return seed;
+    }
+  };
+  std::unordered_map<
+    std::pair<unsigned int, const irept::dt *>,
+    std::string,
+    pair_hash<unsigned int, const irept::dt *>>
+    cache;
 };
 
 #endif // CPROVER_GOTO_PROGRAMS_GRAPHML_WITNESS_H
diff --git a/src/goto-programs/module_dependencies.txt b/src/goto-programs/module_dependencies.txt
index 817a766a240..b63faa217a6 100644
--- a/src/goto-programs/module_dependencies.txt
+++ b/src/goto-programs/module_dependencies.txt
@@ -1,4 +1,5 @@
 analyses # dubious - concerns call_graph and does_remove_const
+ansi-c # for GraphML witnesses
 goto-programs
 goto-symex # dubious - spurious inclusion of symex_target_equation in graphml_witness
 json
diff --git a/src/xmllang/graphml.cpp b/src/xmllang/graphml.cpp
index 17dc6fd9577..286912aa089 100644
--- a/src/xmllang/graphml.cpp
+++ b/src/xmllang/graphml.cpp
@@ -54,7 +54,6 @@ static bool build_graph_rec(
     node.node_name=node_name;
     node.is_violation=false;
     node.has_invariant=false;
-    node.thread_nr=0;
 
     for(xmlt::elementst::const_iterator
         e_it=xml.elements.begin();
@@ -66,8 +65,6 @@ static bool build_graph_rec(
       if(e_it->get_attribute("key")=="violation" &&
          e_it->data=="true")
         node.is_violation=e_it->data=="true";
-      else if(e_it->get_attribute("key")=="threadNumber")
-        node.thread_nr=safe_string2unsigned(e_it->data);
       else if(e_it->get_attribute("key")=="entry" &&
               e_it->data=="true")
         entrynode=node_name;
@@ -255,33 +252,6 @@ bool write_graphml(const graphmlt &src, std::ostream &os)
     key.set_attribute("id", "invariant.scope");
   }
 
-  // <key attr.name="nodeType" attr.type="string" for="node" id="nodetype">
-  //     <default>path</default>
-  // </key>
-  {
-    xmlt &key=graphml.new_element("key");
-    key.set_attribute("attr.name", "nodeType");
-    key.set_attribute("attr.type", "string");
-    key.set_attribute("for", "node");
-    key.set_attribute("id", "nodetype");
-
-    key.new_element("default").data="path";
-  }
-
-  // <key attr.name="isFrontierNode" attr.type="boolean" for="node"
-  //      id="frontier">
-  //     <default>false</default>
-  // </key>
-  {
-    xmlt &key=graphml.new_element("key");
-    key.set_attribute("attr.name", "isFrontierNode");
-    key.set_attribute("attr.type", "boolean");
-    key.set_attribute("for", "node");
-    key.set_attribute("id", "frontier");
-
-    key.new_element("default").data="false";
-  }
-
   // <key attr.name="isViolationNode" attr.type="boolean" for="node"
   //      id="violation">
   //     <default>false</default>
@@ -336,14 +306,39 @@ bool write_graphml(const graphmlt &src, std::ostream &os)
     key.new_element("default").data="false";
   }
 
+  // <key attr.name="cyclehead" attr.type="boolean" for="edge"
+  //      id="cyclehead">
+  //   <default>false</default>
+  // </key>
+  {
+    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("id", "cyclehead");
+
+    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.name", "threadId");
     key.set_attribute("attr.type", "int");
-    key.set_attribute("for", "node");
-    key.set_attribute("id", "thread");
+    key.set_attribute("for", "edge");
+    key.set_attribute("id", "threadId");
+
+    key.new_element("default").data = "0";
+  }
+
+  // <key attr.name="createThread" attr.type="string"
+  //      for="edge" id="createThread"/>
+  {
+    xmlt &key = graphml.new_element("key");
+    key.set_attribute("attr.name", "createThread");
+    key.set_attribute("attr.type", "int");
+    key.set_attribute("for", "edge");
+    key.set_attribute("id", "createThread");
 
     key.new_element("default").data="0";
   }
@@ -408,15 +403,6 @@ bool write_graphml(const graphmlt &src, std::ostream &os)
     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");
@@ -525,13 +511,6 @@ bool write_graphml(const graphmlt &src, std::ostream &os)
       entry_done=true;
     }
 
-    if(n.thread_nr!=0)
-    {
-      xmlt &entry=node.new_element("data");
-      entry.set_attribute("key", "threadNumber");
-      entry.data=std::to_string(n.thread_nr);
-    }
-
     // <node id="A14">
     //     <data key="violation">true</data>
     // </node>
diff --git a/src/xmllang/graphml.h b/src/xmllang/graphml.h
index f86dac5648e..cbdcd122828 100644
--- a/src/xmllang/graphml.h
+++ b/src/xmllang/graphml.h
@@ -32,7 +32,6 @@ struct xml_graph_nodet:public graph_nodet<xml_edget>
   std::string node_name;
   irep_idt file;
   irep_idt line;
-  unsigned thread_nr;
   bool is_violation;
   bool has_invariant;
   std::string invariant;