diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp
index 30ae4748ab9..177930598ec 100644
--- a/src/solvers/refinement/string_refinement_util.cpp
+++ b/src/solvers/refinement/string_refinement_util.cpp
@@ -497,7 +497,8 @@ void string_dependenciest::output_dot(std::ostream &stream) const
     return ostream.str();
   };
   stream << "digraph dependencies {\n";
-  output_dot_generic<nodet>(stream, for_each, for_each_succ, node_to_string);
+  output_dot_generic<nodet>(
+    stream, for_each, for_each_succ, node_to_string, node_to_string);
   stream << '}' << std::endl;
 }
 
diff --git a/src/util/graph.h b/src/util/graph.h
index e0c201c3177..c18622a054a 100644
--- a/src/util/graph.h
+++ b/src/util/graph.h
@@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <list>
 #include <map>
 #include <queue>
+#include <sstream>
 #include <stack>
 #include <vector>
 
@@ -60,6 +61,39 @@ class graph_nodet
   {
     out.erase(n);
   }
+
+private:
+  /// \brief Node with attributes suitable for Graphviz DOT format
+  ///
+  /// Derived types may override this function to produce more informative DOT
+  /// diagrams than the default implementation, which displays only the node
+  /// index. The return value should be a list of node attributes within square
+  /// brackets that can be parsed by `dot`. Here is a sample implementation for
+  /// a fictional node type with `is_evil()` and `is_pink()` functions:
+  ///
+  ///     std::stringstream ss;
+  ///     ss << "[shape=\"" << is_evil() ? "box" : "diamond"
+  ///        << "\", color=\"" << is_pink() ? "#e91e63" : "#9c27b0"
+  ///        << "\", label=\"this is node " << std::to_string(idx)
+  ///        << "\"]";
+  ///     return ss.str();
+  ///
+  virtual std::string dot_attributes(const node_indext &idx) const
+  {
+    return "";
+  }
+
+public:
+  std::string pretty(const node_indext &idx) const
+  {
+    std::stringstream ss;
+    ss << std::to_string(idx) << " " << dot_attributes(idx);
+    return ss.str();
+  }
+
+  virtual ~graph_nodet()
+  {
+  }
 };
 
 /// A node type with an extra bit
@@ -877,9 +911,11 @@ void output_dot_generic(
   const std::function<
     void(const node_index_type &, std::function<void(const node_index_type &)>)>
     &for_each_succ,
-  const std::function<std::string(const node_index_type &)> node_to_string)
+  const std::function<std::string(const node_index_type &)> node_to_string,
+  const std::function<std::string(const node_index_type &)> node_to_pretty)
 {
   for_each_node([&](const node_index_type &i) {
+    out << node_to_pretty(i) << ";\n";
     for_each_succ(i, [&](const node_index_type &n) {
       out << node_to_string(i) << " -> " << node_to_string(n) << '\n';
     });
@@ -914,7 +950,7 @@ template <class N>
 void grapht<N>::output_dot(std::ostream &out) const
 {
   const auto for_each_node =
-    [&](const std::function<void(const node_indext &)> &f) {
+    [this](const std::function<void(const node_indext &)> &f) {
       for(node_indext i = 0; i < nodes.size(); ++i)
         f(i);
     };
@@ -925,7 +961,11 @@ void grapht<N>::output_dot(std::ostream &out) const
   };
 
   const auto to_string = [](const node_indext &i) { return std::to_string(i); };
-  output_dot_generic<node_indext>(out, for_each_node, for_each_succ, to_string);
+  const auto to_pretty_string = [this](const node_indext &i) {
+    return nodes[i].pretty(i);
+  };
+  output_dot_generic<node_indext>(
+    out, for_each_node, for_each_succ, to_string, to_pretty_string);
 }
 
 #endif // CPROVER_UTIL_GRAPH_H