3 files changed, 10 insertions, 5 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index aebaf7ae5..ab278e804 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -17,6 +17,7 @@
  **/
 
 #include "printer/cvc/cvc_printer.h"
+#include "util/language.h"
 
 #include <iostream>
 
@@ -28,7 +29,7 @@ namespace cvc {
 
 std::ostream& CvcPrinter::toStream(std::ostream& out, TNode n,
                                    int toDepth, bool types) const {
-  return out;
+  return n.toStream(out, toDepth, types, language::output::LANG_AST);
 }/* CvcPrinter::toStream() */
 
 }/* CVC4::printer::cvc namespace */
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index a2a9b3378..ca5935bec 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -34,17 +34,20 @@ Printer* Printer::makePrinter(OutputLanguage lang) {
 
   switch(lang) {
   case LANG_SMTLIB:
-    //return new printer::smt::SmtPrinter;
+    return new printer::smt::SmtPrinter;
+
   case LANG_SMTLIB_V2:
     return new printer::smt2::Smt2Printer;
+
   case LANG_CVC4:
-    //return new printer::cvc::CvcPrinter;
+    return new printer::cvc::CvcPrinter;
+
   case LANG_AST:
     return new printer::ast::AstPrinter;
+
   default:
     Unhandled(lang);
   }
 }/* Printer::makePrinter() */
 
 }/* CVC4 namespace */
-
diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt/smt_printer.cpp
index 6040c133b..4d8f4bcd4 100644
--- a/src/printer/smt/smt_printer.cpp
+++ b/src/printer/smt/smt_printer.cpp
@@ -17,6 +17,7 @@
  **/
 
 #include "printer/smt/smt_printer.h"
+#include "util/language.h"
 
 #include <iostream>
 
@@ -28,7 +29,7 @@ namespace smt {
 
 std::ostream& SmtPrinter::toStream(std::ostream& out, TNode n,
                                    int toDepth, bool types) const {
-  return out;
+  return n.toStream(out, toDepth, types, language::output::LANG_SMTLIB_V2);
 }/* SmtPrinter::toStream() */
 
 }/* CVC4::printer::smt namespace */