1 files changed, 12 insertions, 1 deletions
diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt/smt_printer.cpp
index d03cfbbe0..de22a04c1 100644
--- a/src/printer/smt/smt_printer.cpp
+++ b/src/printer/smt/smt_printer.cpp
@@ -17,9 +17,15 @@
  **/
 
 #include "printer/smt/smt_printer.h"
-#include "util/language.h"
+#include "expr/expr.h" // for ExprSetDepth etc..
+#include "util/language.h" // for LANG_AST
+#include "expr/node_manager.h" // for VarNameAttr
+#include "expr/command.h"
 
 #include <iostream>
+#include <vector>
+#include <string>
+#include <typeinfo>
 
 using namespace std;
 
@@ -32,6 +38,11 @@ void SmtPrinter::toStream(std::ostream& out, TNode n,
   n.toStream(out, toDepth, types, language::output::LANG_SMTLIB_V2);
 }/* SmtPrinter::toStream() */
 
+void SmtPrinter::toStream(std::ostream& out, const Command* c,
+                          int toDepth, bool types) const {
+  c->toStream(out, toDepth, types, language::output::LANG_SMTLIB_V2);
+}/* SmtPrinter::toStream() */
+
 }/* CVC4::printer::smt namespace */
 }/* CVC4::printer namespace */
 }/* CVC4 namespace */