From 957881c613b52e5fac840da71b5433dc2de19c70 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Thu, 3 May 2018 22:38:02 +0100
Subject: [PATCH] format now prints type expressions and the values of named
 sub-ireps

---
 src/util/format_expr.cpp | 32 +++++++++++++++++++++-----------
 1 file changed, 21 insertions(+), 11 deletions(-)

diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp
index e7f91e43169..b552e538f45 100644
--- a/src/util/format_expr.cpp
+++ b/src/util/format_expr.cpp
@@ -165,6 +165,8 @@ std::ostream &format_rec(
               << to_member_expr(expr).get_component_name();
   else if(id == ID_symbol)
     return os << to_symbol_expr(expr).get_identifier();
+  else if(id == ID_type)
+    return format_rec(os, expr.type());
   else if(id == ID_forall || id == ID_exists)
     return os << id << ' ' << format(to_quantifier_expr(expr).symbol()) << " : "
               << format(to_quantifier_expr(expr).symbol().type()) << " . "
@@ -199,22 +201,30 @@ std::ostream &format_rec(
   }
   else
   {
-    if(!expr.has_operands())
-      return os << id;
+    os << id;
 
-    os << id << '(';
-    bool first = true;
+    for(const auto &s : expr.get_named_sub())
+      if(s.first!=ID_type)
+        os << ' ' << s.first << "=\"" << s.second.id() << '"';
 
-    for(const auto &op : expr.operands())
+    if(expr.has_operands())
     {
-      if(first)
-        first = false;
-      else
-        os << ", ";
+      os << id << '(';
+      bool first = true;
 
-      os << format(op);
+      for(const auto &op : expr.operands())
+      {
+        if(first)
+          first = false;
+        else
+          os << ", ";
+
+        os << format(op);
+      }
+
+      os << ')';
     }
 
-    return os << ')';
+    return os;
   }
 }