1 files changed, 16 insertions, 0 deletions
diff --git a/src/smt/dump.h b/src/smt/dump.h
index 050935422..4c0efeb6e 100644
--- a/src/smt/dump.h
+++ b/src/smt/dump.h
@@ -21,6 +21,7 @@
 
 #include "base/output.h"
 #include "smt/command.h"
+#include "smt/node_command.h"
 
 namespace CVC4 {
 
@@ -40,6 +41,20 @@ class CVC4_PUBLIC CVC4dumpstream
     return *this;
   }
 
+  /** A convenience function for dumping internal commands.
+   *
+   * Since Commands are now part of the public API, internal code should use
+   * NodeCommands and this function (instead of the one above) to dump them.
+   */
+  CVC4dumpstream& operator<<(const NodeCommand& nc)
+  {
+    if (d_os != nullptr)
+    {
+      (*d_os) << nc << std::endl;
+    }
+    return *this;
+  }
+
  private:
   std::ostream* d_os;
 }; /* class CVC4dumpstream */
@@ -56,6 +71,7 @@ class CVC4_PUBLIC CVC4dumpstream
   CVC4dumpstream() {}
   CVC4dumpstream(std::ostream& os) {}
   CVC4dumpstream& operator<<(const Command& c) { return *this; }
+  CVC4dumpstream& operator<<(const NodeCommand& nc) { return *this; }
 }; /* class CVC4dumpstream */
 
 #endif /* CVC4_DUMPING && !CVC4_MUZZLE */