4 files changed, 11 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 */
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index aa566b307..6cb35e518 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -18,6 +18,7 @@ libarith_la_SOURCES = \
 	partial_model.h \
 	partial_model.cpp \
 	ordered_bounds_list.h \
+	ordered_set.h \
 	arithvar_dense_set.h \
 	tableau.h \
 	tableau.cpp \