better traces in node converter (#7590)

diff --git a/src/expr/node_converter.cpp b/src/expr/node_converter.cpp
index eabe1d4f1346e9fa1cbf56ca37d1301d3907294e..b72aa99f66e436966fd960d262388d7450b29f2e 100644 (file)
--- a/src/expr/node_converter.cpp
+++ b/src/expr/node_converter.cpp
@@ -52,6 +52,8 @@ Node NodeConverter::convert(Node n)
       d_preCache[cur] = curp;
       if (!curp.isNull())
       {
+        Trace("nconv-debug2")
+            << "..pre-rewrite changed " << cur << " into " << curp << std::endl;
         visit.push_back(cur);
         visit.push_back(curp);
       }
@@ -74,6 +76,7 @@ Node NodeConverter::convert(Node n)
     }
     else if (it->second.isNull())
     {
+      Trace("nconv-debug2") << "..post-visit " << cur << std::endl;
       it = d_preCache.find(cur);
       Assert(it != d_preCache.end());
       if (!it->second.isNull())
@@ -82,6 +85,8 @@ Node NodeConverter::convert(Node n)
         Assert(d_cache.find(it->second) != d_cache.end());
         Node ret = d_cache[it->second];
         addToCache(cur, ret);
+        Trace("nconv-debug2")
+            << "..from cache changed " << cur << " into " << ret << std::endl;
       }
       else
       {
@@ -107,6 +112,8 @@ Node NodeConverter::convert(Node n)
         if (childChanged)
         {
           ret = nm->mkNode(ret.getKind(), children);
+          Trace("nconv-debug2") << "..from children changed " << cur << " into "
+                                << ret << std::endl;
         }
         // run the callback for the current application
         Node cret = postConvert(ret);
@@ -114,6 +121,8 @@ Node NodeConverter::convert(Node n)
         {
           AlwaysAssert(cret.getType().isComparableTo(ret.getType()))
               << "Converting " << ret << " to " << cret << " changes type";
+          Trace("nconv-debug2") << "..post-rewrite changed " << ret << " into "
+                                << cret << std::endl;
           ret = cret;
         }
         addToCache(cur, ret);