Dump commands in internal code using command printing functions. (#5040)

This is work towards migrating commands to the new API. Internal code that creates command objects just for dumping is replaced with direct calls to functions that print the those commands.

53 files changed, 593 insertions, 501 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 3b0794a8f..e6cb97894 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -216,6 +216,8 @@ libcvc4_add_sources(
   smt/node_command.h
   smt/options_manager.cpp
   smt/options_manager.h
+  smt/output_manager.cpp
+  smt/output_manager.h
   smt/quant_elim_solver.cpp
   smt/quant_elim_solver.h
   smt/preprocessor.cpp
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index de21db74d..1c10aa09f 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -21,12 +21,13 @@
 #include "api/cvc4cpp.h"
 #include "expr/expr_manager.h"
 #include "options/options.h"
-#include "smt/command.h"
 #include "smt/smt_engine.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
 
+class Command;
+
 namespace api {
 class Solver;
 }
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 9cf168392..7b72ae249 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -32,7 +32,6 @@
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "parser/parser_exception.h"
-#include "smt/command.h"
 #include "smt/smt_engine.h"
 #include "util/result.h"
 #include "util/statistics.h"
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index bf5e8824a..54165feb7 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -33,7 +33,6 @@
 #include "parser/smt2/smt2_input.h"
 #include "parser/smt2/sygus_input.h"
 #include "parser/tptp/tptp_input.h"
-#include "smt/command.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/parser/cvc/cvc.cpp b/src/parser/cvc/cvc.cpp
index 4d409a0b4..7caa35dd6 100644
--- a/src/parser/cvc/cvc.cpp
+++ b/src/parser/cvc/cvc.cpp
@@ -15,6 +15,7 @@
  **/
 
 #include "parser/cvc/cvc.h"
+#include "smt/command.h"
 
 namespace CVC4 {
 namespace parser {
diff --git a/src/parser/cvc/cvc.h b/src/parser/cvc/cvc.h
index 7c226168f..3930a02f5 100644
--- a/src/parser/cvc/cvc.h
+++ b/src/parser/cvc/cvc.h
@@ -21,7 +21,6 @@
 
 #include "api/cvc4cpp.h"
 #include "parser/parser.h"
-#include "smt/command.h"
 
 namespace CVC4 {
 
diff --git a/src/parser/input.cpp b/src/parser/input.cpp
index 13903eaf5..8d5057151 100644
--- a/src/parser/input.cpp
+++ b/src/parser/input.cpp
@@ -23,7 +23,6 @@
 #include "expr/type.h"
 #include "parser/parser.h"
 #include "parser/parser_exception.h"
-#include "smt/command.h"
 
 
 using namespace std;
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 2e725f9bf..ebf3811c4 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -28,12 +28,12 @@
 #include "api/cvc4cpp.h"
 #include "parser/parse_op.h"
 #include "parser/parser.h"
-#include "smt/command.h"
 #include "theory/logic_info.h"
 #include "util/abstract_value.h"
 
 namespace CVC4 {
 
+class Command;
 class SExpr;
 
 namespace api {
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index cb4d3fd9e..ab6a4c5eb 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -24,6 +24,7 @@
 #include "expr/type.h"
 #include "options/options.h"
 #include "parser/parser.h"
+#include "smt/command.h"
 
 // ANTLR defines these, which is really bad!
 #undef true
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index 3d5419be9..40dd85f63 100644
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -28,11 +28,12 @@
 #include "api/cvc4cpp.h"
 #include "parser/parse_op.h"
 #include "parser/parser.h"
-#include "smt/command.h"
 #include "util/hash.h"
 
 namespace CVC4 {
 
+class Command;
+
 namespace api {
 class Solver;
 }
diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp
index 965edcd2f..cd2a51c45 100644
--- a/src/preprocessing/preprocessing_pass.cpp
+++ b/src/preprocessing/preprocessing_pass.cpp
@@ -18,6 +18,7 @@
 
 #include "smt/dump.h"
 #include "smt/smt_statistics_registry.h"
+#include "printer/printer.h"
 
 namespace CVC4 {
 namespace preprocessing {
@@ -39,8 +40,13 @@ void PreprocessingPass::dumpAssertions(const char* key,
   if (Dump.isOn("assertions") && Dump.isOn(std::string("assertions:") + key))
   {
     // Push the simplified assertions to the dump output stream
-    for (const auto& n : assertionList) {
-      Dump("assertions") << AssertCommand(Expr(n.toExpr()));
+    OutputManager& outMgr = d_preprocContext->getSmt()->getOutputManager();
+    const Printer& printer = outMgr.getPrinter();
+    std::ostream& out = outMgr.getDumpOut();
+
+    for (const auto& n : assertionList)
+    {
+      printer.toStreamCmdAssert(out, n);
     }
   }
 }
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index f776d07db..e179b7ffd 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -166,23 +166,28 @@ void AstPrinter::toStream(std::ostream& out,
 void AstPrinter::toStreamCmdEmpty(std::ostream& out,
                                   const std::string& name) const
 {
-  out << "EmptyCommand(" << name << ')';
+  out << "EmptyCommand(" << name << ')' << std::endl;
 }
 
 void AstPrinter::toStreamCmdEcho(std::ostream& out,
                                  const std::string& output) const
 {
-  out << "EchoCommand(" << output << ')';
+  out << "EchoCommand(" << output << ')' << std::endl;
 }
 
 void AstPrinter::toStreamCmdAssert(std::ostream& out, Node n) const
 {
-  out << "Assert(" << n << ')';
+  out << "Assert(" << n << ')' << std::endl;
 }
 
-void AstPrinter::toStreamCmdPush(std::ostream& out) const { out << "Push()"; }
+void AstPrinter::toStreamCmdPush(std::ostream& out) const
+{
+  out << "Push()" << std::endl;
+}
 
-void AstPrinter::toStreamCmdPop(std::ostream& out) const { out << "Pop()"; }
+void AstPrinter::toStreamCmdPop(std::ostream& out) const {
+  out << "Pop()" << std::endl;
+}
 
 void AstPrinter::toStreamCmdCheckSat(std::ostream& out, Node n) const
 {
@@ -194,6 +199,7 @@ void AstPrinter::toStreamCmdCheckSat(std::ostream& out, Node n) const
   {
     out << "CheckSat(" << n << ')';
   }
+  out << std::endl;
 }
 
 void AstPrinter::toStreamCmdCheckSatAssuming(
@@ -201,22 +207,28 @@ void AstPrinter::toStreamCmdCheckSatAssuming(
 {
   out << "CheckSatAssuming( << ";
   copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, ", "));
-  out << ">> )";
+  out << ">> )" << std::endl;
 }
 
 void AstPrinter::toStreamCmdQuery(std::ostream& out, Node n) const
 {
-  out << "Query(" << n << ')';
+  out << "Query(" << n << ')' << std::endl;
 }
 
-void AstPrinter::toStreamCmdReset(std::ostream& out) const { out << "Reset()"; }
+void AstPrinter::toStreamCmdReset(std::ostream& out) const
+{
+  out << "Reset()" << std::endl;
+}
 
 void AstPrinter::toStreamCmdResetAssertions(std::ostream& out) const
 {
-  out << "ResetAssertions()";
+  out << "ResetAssertions()" << std::endl;
 }
 
-void AstPrinter::toStreamCmdQuit(std::ostream& out) const { out << "Quit()"; }
+void AstPrinter::toStreamCmdQuit(std::ostream& out) const
+{
+  out << "Quit()" << std::endl;
+}
 
 void AstPrinter::toStreamCmdDeclarationSequence(
     std::ostream& out, const std::vector<Command*>& sequence) const
@@ -228,7 +240,7 @@ void AstPrinter::toStreamCmdDeclarationSequence(
   {
     out << *i << endl;
   }
-  out << "]";
+  out << "]" << std::endl;
 }
 
 void AstPrinter::toStreamCmdCommandSequence(
@@ -241,14 +253,14 @@ void AstPrinter::toStreamCmdCommandSequence(
   {
     out << *i << endl;
   }
-  out << "]";
+  out << "]" << std::endl;
 }
 
 void AstPrinter::toStreamCmdDeclareFunction(std::ostream& out,
                                             const std::string& id,
                                             TypeNode type) const
 {
-  out << "Declare(" << id << "," << type << ')';
+  out << "Declare(" << id << "," << type << ')' << std::endl;
 }
 
 void AstPrinter::toStreamCmdDefineFunction(std::ostream& out,
@@ -263,7 +275,7 @@ void AstPrinter::toStreamCmdDefineFunction(std::ostream& out,
     copy(formals.begin(), formals.end() - 1, ostream_iterator<Node>(out, ", "));
     out << formals.back();
   }
-  out << "], << " << formula << " >> )";
+  out << "], << " << formula << " >> )" << std::endl;
 }
 
 void AstPrinter::toStreamCmdDeclareType(std::ostream& out,
@@ -271,7 +283,8 @@ void AstPrinter::toStreamCmdDeclareType(std::ostream& out,
                                         size_t arity,
                                         TypeNode type) const
 {
-  out << "DeclareType(" << id << "," << arity << "," << type << ')';
+  out << "DeclareType(" << id << "," << arity << "," << type << ')'
+      << std::endl;
 }
 
 void AstPrinter::toStreamCmdDefineType(std::ostream& out,
@@ -287,7 +300,7 @@ void AstPrinter::toStreamCmdDefineType(std::ostream& out,
          ostream_iterator<TypeNode>(out, ", "));
     out << params.back();
   }
-  out << "]," << t << ')';
+  out << "]," << t << ')' << std::endl;
 }
 
 void AstPrinter::toStreamCmdDefineNamedFunction(
@@ -304,7 +317,7 @@ void AstPrinter::toStreamCmdDefineNamedFunction(
 
 void AstPrinter::toStreamCmdSimplify(std::ostream& out, Node n) const
 {
-  out << "Simplify( << " << n << " >> )";
+  out << "Simplify( << " << n << " >> )" << std::endl;
 }
 
 void AstPrinter::toStreamCmdGetValue(std::ostream& out,
@@ -312,70 +325,70 @@ void AstPrinter::toStreamCmdGetValue(std::ostream& out,
 {
   out << "GetValue( << ";
   copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, ", "));
-  out << ">> )";
+  out << ">> )" << std::endl;
 }
 
 void AstPrinter::toStreamCmdGetModel(std::ostream& out) const
 {
-  out << "GetModel()";
+  out << "GetModel()" << std::endl;
 }
 
 void AstPrinter::toStreamCmdGetAssignment(std::ostream& out) const
 {
-  out << "GetAssignment()";
+  out << "GetAssignment()" << std::endl;
 }
 
 void AstPrinter::toStreamCmdGetAssertions(std::ostream& out) const
 {
-  out << "GetAssertions()";
+  out << "GetAssertions()" << std::endl;
 }
 
 void AstPrinter::toStreamCmdGetProof(std::ostream& out) const
 {
-  out << "GetProof()";
+  out << "GetProof()" << std::endl;
 }
 
 void AstPrinter::toStreamCmdGetUnsatCore(std::ostream& out) const
 {
-  out << "GetUnsatCore()";
+  out << "GetUnsatCore()" << std::endl;
 }
 
 void AstPrinter::toStreamCmdSetBenchmarkStatus(std::ostream& out,
                                                Result::Sat status) const
 {
-  out << "SetBenchmarkStatus(" << status << ')';
+  out << "SetBenchmarkStatus(" << status << ')' << std::endl;
 }
 
 void AstPrinter::toStreamCmdSetBenchmarkLogic(std::ostream& out,
                                               const std::string& logic) const
 {
-  out << "SetBenchmarkLogic(" << logic << ')';
+  out << "SetBenchmarkLogic(" << logic << ')' << std::endl;
 }
 
 void AstPrinter::toStreamCmdSetInfo(std::ostream& out,
                                     const std::string& flag,
                                     SExpr sexpr) const
 {
-  out << "SetInfo(" << flag << ", " << sexpr << ')';
+  out << "SetInfo(" << flag << ", " << sexpr << ')' << std::endl;
 }
 
 void AstPrinter::toStreamCmdGetInfo(std::ostream& out,
                                     const std::string& flag) const
 {
-  out << "GetInfo(" << flag << ')';
+  out << "GetInfo(" << flag << ')' << std::endl;
 }
 
 void AstPrinter::toStreamCmdSetOption(std::ostream& out,
                                       const std::string& flag,
                                       SExpr sexpr) const
 {
-  out << "SetOption(" << flag << ", " << sexpr << ')';
+  out << "SetOption(" << flag << ", " << sexpr << ')' << std::endl;
 }
 
 void AstPrinter::toStreamCmdGetOption(std::ostream& out,
                                       const std::string& flag) const
 {
-  out << "GetOption(" << flag << ')';
+  out << "GetOption(" << flag << ')' << std::endl;
 }
 
 void AstPrinter::toStreamCmdDatatypeDeclaration(
@@ -386,13 +399,13 @@ void AstPrinter::toStreamCmdDatatypeDeclaration(
   {
     out << t << ";" << endl;
   }
-  out << "])";
+  out << "])" << std::endl;
 }
 
 void AstPrinter::toStreamCmdComment(std::ostream& out,
                                     const std::string& comment) const
 {
-  out << "CommentCommand([" << comment << "])";
+  out << "CommentCommand([" << comment << "])" << std::endl;
 }
 
 template <class T>
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 02afa715d..46b509388 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -1203,12 +1203,18 @@ void CvcPrinter::toStream(std::ostream& out,
 
 void CvcPrinter::toStreamCmdAssert(std::ostream& out, Node n) const
 {
-  out << "ASSERT " << n << ';';
+  out << "ASSERT " << n << ';' << std::endl;
 }
 
-void CvcPrinter::toStreamCmdPush(std::ostream& out) const { out << "PUSH;"; }
+void CvcPrinter::toStreamCmdPush(std::ostream& out) const
+{
+  out << "PUSH;" << std::endl;
+}
 
-void CvcPrinter::toStreamCmdPop(std::ostream& out) const { out << "POP;"; }
+void CvcPrinter::toStreamCmdPop(std::ostream& out) const
+{
+  out << "POP;" << std::endl;
+}
 
 void CvcPrinter::toStreamCmdCheckSat(std::ostream& out, Node n) const
 {
@@ -1228,6 +1234,7 @@ void CvcPrinter::toStreamCmdCheckSat(std::ostream& out, Node n) const
   {
     out << " POP;";
   }
+  out << std::endl;
 }
 
 void CvcPrinter::toStreamCmdCheckSatAssuming(
@@ -1251,6 +1258,7 @@ void CvcPrinter::toStreamCmdCheckSatAssuming(
   {
     out << " POP;";
   }
+  out << std::endl;
 }
 
 void CvcPrinter::toStreamCmdQuery(std::ostream& out, Node n) const
@@ -1271,18 +1279,22 @@ void CvcPrinter::toStreamCmdQuery(std::ostream& out, Node n) const
   {
     out << " POP;";
   }
+  out << std::endl;
 }
 
-void CvcPrinter::toStreamCmdReset(std::ostream& out) const { out << "RESET;"; }
+void CvcPrinter::toStreamCmdReset(std::ostream& out) const
+{
+  out << "RESET;" << std::endl;
+}
 
 void CvcPrinter::toStreamCmdResetAssertions(std::ostream& out) const
 {
-  out << "RESET ASSERTIONS;";
+  out << "RESET ASSERTIONS;" << std::endl;
 }
 
 void CvcPrinter::toStreamCmdQuit(std::ostream& out) const
 {
-  // out << "EXIT;";
+  // out << "EXIT;" << std::endl;
 }
 
 void CvcPrinter::toStreamCmdCommandSequence(
@@ -1292,7 +1304,7 @@ void CvcPrinter::toStreamCmdCommandSequence(
        i != sequence.cend();
        ++i)
   {
-    out << *i << endl;
+    out << *i;
   }
 }
 
@@ -1314,13 +1326,14 @@ void CvcPrinter::toStreamCmdDeclarationSequence(
       break;
     }
   }
+  out << std::endl;
 }
 
 void CvcPrinter::toStreamCmdDeclareFunction(std::ostream& out,
                                             const std::string& id,
                                             TypeNode type) const
 {
-  out << id << " : " << type << ';';
+  out << id << " : " << type << ';' << std::endl;
 }
 
 void CvcPrinter::toStreamCmdDefineFunction(std::ostream& out,
@@ -1353,7 +1366,7 @@ void CvcPrinter::toStreamCmdDefineFunction(std::ostream& out,
     }
     out << "): ";
   }
-  out << formula << ';';
+  out << formula << ';' << std::endl;
 }
 
 void CvcPrinter::toStreamCmdDeclareType(std::ostream& out,
@@ -1370,7 +1383,7 @@ void CvcPrinter::toStreamCmdDeclareType(std::ostream& out,
   }
   else
   {
-    out << id << " : TYPE;";
+    out << id << " : TYPE;" << std::endl;
   }
 }
 
@@ -1387,7 +1400,7 @@ void CvcPrinter::toStreamCmdDefineType(std::ostream& out,
   }
   else
   {
-    out << id << " : TYPE = " << t << ';';
+    out << id << " : TYPE = " << t << ';' << std::endl;
   }
 }
 
@@ -1403,7 +1416,7 @@ void CvcPrinter::toStreamCmdDefineNamedFunction(
 
 void CvcPrinter::toStreamCmdSimplify(std::ostream& out, Node n) const
 {
-  out << "TRANSFORM " << n << ';';
+  out << "TRANSFORM " << n << ';' << std::endl;
 }
 
 void CvcPrinter::toStreamCmdGetValue(std::ostream& out,
@@ -1414,44 +1427,44 @@ void CvcPrinter::toStreamCmdGetValue(std::ostream& out,
   copy(nodes.begin(),
        nodes.end() - 1,
        ostream_iterator<Node>(out, ";\nGET_VALUE "));
-  out << nodes.back() << ';';
+  out << nodes.back() << ';' << std::endl;
 }
 
 void CvcPrinter::toStreamCmdGetModel(std::ostream& out) const
 {
-  out << "COUNTERMODEL;";
+  out << "COUNTERMODEL;" << std::endl;
 }
 
 void CvcPrinter::toStreamCmdGetAssignment(std::ostream& out) const
 {
-  out << "% (get-assignment)";
+  out << "% (get-assignment)" << std::endl;
 }
 
 void CvcPrinter::toStreamCmdGetAssertions(std::ostream& out) const
 {
-  out << "WHERE;";
+  out << "WHERE;" << std::endl;
 }
 
 void CvcPrinter::toStreamCmdGetProof(std::ostream& out) const
 {
-  out << "DUMP_PROOF;";
+  out << "DUMP_PROOF;" << std::endl;
 }
 
 void CvcPrinter::toStreamCmdGetUnsatCore(std::ostream& out) const
 {
-  out << "DUMP_UNSAT_CORE;";
+  out << "DUMP_UNSAT_CORE;" << std::endl;
 }
 
 void CvcPrinter::toStreamCmdSetBenchmarkStatus(std::ostream& out,
                                                Result::Sat status) const
 {
-  out << "% (set-info :status " << status << ')';
+  out << "% (set-info :status " << status << ')' << std::endl;
 }
 
 void CvcPrinter::toStreamCmdSetBenchmarkLogic(std::ostream& out,
                                               const std::string& logic) const
 {
-  out << "OPTION \"logic\" \"" << logic << "\";";
+  out << "OPTION \"logic\" \"" << logic << "\";" << std::endl;
 }
 
 void CvcPrinter::toStreamCmdSetInfo(std::ostream& out,
@@ -1462,13 +1475,13 @@ void CvcPrinter::toStreamCmdSetInfo(std::ostream& out,
   OutputLanguage language =
       d_cvc3Mode ? language::output::LANG_CVC3 : language::output::LANG_CVC4;
   SExpr::toStream(out, sexpr, language);
-  out << ')';
+  out << ')' << std::endl;
 }
 
 void CvcPrinter::toStreamCmdGetInfo(std::ostream& out,
                                     const std::string& flag) const
 {
-  out << "% (get-info " << flag << ')';
+  out << "% (get-info " << flag << ')' << std::endl;
 }
 
 void CvcPrinter::toStreamCmdSetOption(std::ostream& out,
@@ -1477,13 +1490,13 @@ void CvcPrinter::toStreamCmdSetOption(std::ostream& out,
 {
   out << "OPTION \"" << flag << "\" ";
   SExpr::toStream(out, sexpr, language::output::LANG_CVC4);
-  out << ';';
+  out << ';' << std::endl;
 }
 
 void CvcPrinter::toStreamCmdGetOption(std::ostream& out,
                                       const std::string& flag) const
 {
-  out << "% (get-option " << flag << ')';
+  out << "% (get-option " << flag << ')' << std::endl;
 }
 
 void CvcPrinter::toStreamCmdDatatypeDeclaration(
@@ -1552,25 +1565,26 @@ void CvcPrinter::toStreamCmdDatatypeDeclaration(
       }
       firstDatatype = false;
     }
-    out << endl << "END;";
+    out << endl << "END;" << std::endl;
   }
 }
 
 void CvcPrinter::toStreamCmdComment(std::ostream& out,
                                     const std::string& comment) const
 {
-  out << "% " << comment;
+  out << "% " << comment << std::endl;
 }
 
 void CvcPrinter::toStreamCmdEmpty(std::ostream& out,
                                   const std::string& name) const
 {
+  out << std::endl;
 }
 
 void CvcPrinter::toStreamCmdEcho(std::ostream& out,
                                  const std::string& output) const
 {
-  out << "ECHO \"" << output << "\";";
+  out << "ECHO \"" << output << "\";" << std::endl;
 }
 
 template <class T>
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 2cc6c8973..7ef02c576 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1451,15 +1451,18 @@ void Smt2Printer::toStream(std::ostream& out,
 
 void Smt2Printer::toStreamCmdAssert(std::ostream& out, Node n) const
 {
-  out << "(assert " << n << ')';
+  out << "(assert " << n << ')' << std::endl;
 }
 
 void Smt2Printer::toStreamCmdPush(std::ostream& out) const
 {
-  out << "(push 1)";
+  out << "(push 1)" << std::endl;
 }
 
-void Smt2Printer::toStreamCmdPop(std::ostream& out) const { out << "(pop 1)"; }
+void Smt2Printer::toStreamCmdPop(std::ostream& out) const
+{
+  out << "(pop 1)" << std::endl;
+}
 
 void Smt2Printer::toStreamCmdCheckSat(std::ostream& out, Node n) const
 {
@@ -1477,6 +1480,7 @@ void Smt2Printer::toStreamCmdCheckSat(std::ostream& out, Node n) const
   {
     out << "(check-sat)";
   }
+  out << std::endl;
 }
 
 void Smt2Printer::toStreamCmdCheckSatAssuming(
@@ -1484,7 +1488,7 @@ void Smt2Printer::toStreamCmdCheckSatAssuming(
 {
   out << "(check-sat-assuming ( ";
   copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, " "));
-  out << "))";
+  out << "))" << std::endl;
 }
 
 void Smt2Printer::toStreamCmdQuery(std::ostream& out, Node n) const
@@ -1508,34 +1512,25 @@ void Smt2Printer::toStreamCmdQuery(std::ostream& out, Node n) const
 
 void Smt2Printer::toStreamCmdReset(std::ostream& out) const
 {
-  out << "(reset)";
+  out << "(reset)" << std::endl;
 }
 
 void Smt2Printer::toStreamCmdResetAssertions(std::ostream& out) const
 {
-  out << "(reset-assertions)";
+  out << "(reset-assertions)" << std::endl;
 }
 
-void Smt2Printer::toStreamCmdQuit(std::ostream& out) const { out << "(exit)"; }
+void Smt2Printer::toStreamCmdQuit(std::ostream& out) const
+{
+  out << "(exit)" << std::endl;
+}
 
 void Smt2Printer::toStreamCmdCommandSequence(
     std::ostream& out, const std::vector<Command*>& sequence) const
 {
-  CommandSequence::const_iterator i = sequence.cbegin();
-  if (i != sequence.cend())
+  for (Command* i : sequence)
   {
-    for (;;)
-    {
-      out << *i;
-      if (++i != sequence.cend())
-      {
-        out << endl;
-      }
-      else
-      {
-        break;
-      }
-    }
+    out << *i;
   }
 }
 
@@ -1563,7 +1558,7 @@ void Smt2Printer::toStreamCmdDeclareFunction(std::ostream& out,
     type = type.getRangeType();
   }
 
-  out << ") " << type << ')';
+  out << ") " << type << ')' << std::endl;
 }
 
 void Smt2Printer::toStreamCmdDefineFunction(std::ostream& out,
@@ -1590,7 +1585,7 @@ void Smt2Printer::toStreamCmdDefineFunction(std::ostream& out,
       }
     }
   }
-  out << ") " << range << ' ' << formula << ')';
+  out << ") " << range << ' ' << formula << ')' << std::endl;
 }
 
 void Smt2Printer::toStreamCmdDefineFunctionRec(
@@ -1659,7 +1654,7 @@ void Smt2Printer::toStreamCmdDefineFunctionRec(
   {
     out << ")";
   }
-  out << ")";
+  out << ")" << std::endl;
 }
 
 static void toStreamRational(std::ostream& out,
@@ -1704,7 +1699,8 @@ void Smt2Printer::toStreamCmdDeclareType(std::ostream& out,
                                          size_t arity,
                                          TypeNode type) const
 {
-  out << "(declare-sort " << CVC4::quoteSymbol(id) << " " << arity << ")";
+  out << "(declare-sort " << CVC4::quoteSymbol(id) << " " << arity << ")"
+      << std::endl;
 }
 
 void Smt2Printer::toStreamCmdDefineType(std::ostream& out,
@@ -1719,7 +1715,7 @@ void Smt2Printer::toStreamCmdDefineType(std::ostream& out,
         params.begin(), params.end() - 1, ostream_iterator<TypeNode>(out, " "));
     out << params.back();
   }
-  out << ") " << t << ")";
+  out << ") " << t << ")" << std::endl;
 }
 
 void Smt2Printer::toStreamCmdDefineNamedFunction(
@@ -1738,7 +1734,7 @@ void Smt2Printer::toStreamCmdDefineNamedFunction(
 
 void Smt2Printer::toStreamCmdSimplify(std::ostream& out, Node n) const
 {
-  out << "(simplify " << n << ')';
+  out << "(simplify " << n << ')' << std::endl;
 }
 
 void Smt2Printer::toStreamCmdGetValue(std::ostream& out,
@@ -1746,49 +1742,49 @@ void Smt2Printer::toStreamCmdGetValue(std::ostream& out,
 {
   out << "(get-value ( ";
   copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, " "));
-  out << "))";
+  out << "))" << std::endl;
 }
 
 void Smt2Printer::toStreamCmdGetModel(std::ostream& out) const
 {
-  out << "(get-model)";
+  out << "(get-model)" << std::endl;
 }
 
 void Smt2Printer::toStreamCmdGetAssignment(std::ostream& out) const
 {
-  out << "(get-assignment)";
+  out << "(get-assignment)" << std::endl;
 }
 
 void Smt2Printer::toStreamCmdGetAssertions(std::ostream& out) const
 {
-  out << "(get-assertions)";
+  out << "(get-assertions)" << std::endl;
 }
 
 void Smt2Printer::toStreamCmdGetProof(std::ostream& out) const
 {
-  out << "(get-proof)";
+  out << "(get-proof)" << std::endl;
 }
 
 void Smt2Printer::toStreamCmdGetUnsatAssumptions(std::ostream& out) const
 {
-  out << "(get-unsat-assumptions)";
+  out << "(get-unsat-assumptions)" << std::endl;
 }
 
 void Smt2Printer::toStreamCmdGetUnsatCore(std::ostream& out) const
 {
-  out << "(get-unsat-core)";
+  out << "(get-unsat-core)" << std::endl;
 }
 
 void Smt2Printer::toStreamCmdSetBenchmarkStatus(std::ostream& out,
                                                 Result::Sat status) const
 {
-  out << "(set-info :status " << status << ')';
+  out << "(set-info :status " << status << ')' << std::endl;
 }
 
 void Smt2Printer::toStreamCmdSetBenchmarkLogic(std::ostream& out,
                                                const std::string& logic) const
 {
-  out << "(set-logic " << logic << ')';
+  out << "(set-logic " << logic << ')' << std::endl;
 }
 
 void Smt2Printer::toStreamCmdSetInfo(std::ostream& out,
@@ -1797,13 +1793,13 @@ void Smt2Printer::toStreamCmdSetInfo(std::ostream& out,
 {
   out << "(set-info :" << flag << ' ';
   SExpr::toStream(out, sexpr, variantToLanguage(d_variant));
-  out << ')';
+  out << ')' << std::endl;
 }
 
 void Smt2Printer::toStreamCmdGetInfo(std::ostream& out,
                                      const std::string& flag) const
 {
-  out << "(get-info :" << flag << ')';
+  out << "(get-info :" << flag << ')' << std::endl;
 }
 
 void Smt2Printer::toStreamCmdSetOption(std::ostream& out,
@@ -1812,13 +1808,13 @@ void Smt2Printer::toStreamCmdSetOption(std::ostream& out,
 {
   out << "(set-option :" << flag << ' ';
   SExpr::toStream(out, sexpr, language::output::LANG_SMTLIB_V2_5);
-  out << ')';
+  out << ')' << std::endl;
 }
 
 void Smt2Printer::toStreamCmdGetOption(std::ostream& out,
                                        const std::string& flag) const
 {
-  out << "(get-option :" << flag << ')';
+  out << "(get-option :" << flag << ')' << std::endl;
 }
 
 void Smt2Printer::toStream(std::ostream& out, const DType& dt) const
@@ -1951,7 +1947,7 @@ void Smt2Printer::toStreamCmdDatatypeDeclaration(
     }
     out << ")";
   }
-  out << ")" << endl;
+  out << ")" << std::endl;
 }
 
 void Smt2Printer::toStreamCmdComment(std::ostream& out,
@@ -1964,12 +1960,13 @@ void Smt2Printer::toStreamCmdComment(std::ostream& out,
     s.replace(pos, 1, d_variant == smt2_0_variant ? "\\\"" : "\"\"");
     pos += 2;
   }
-  out << "(set-info :notes \"" << s << "\")";
+  out << "(set-info :notes \"" << s << "\")" << std::endl;
 }
 
 void Smt2Printer::toStreamCmdEmpty(std::ostream& out,
                                    const std::string& name) const
 {
+  out << std::endl;
 }
 
 void Smt2Printer::toStreamCmdEcho(std::ostream& out,
@@ -1983,7 +1980,7 @@ void Smt2Printer::toStreamCmdEcho(std::ostream& out,
     s.replace(pos, 1, d_variant == smt2_0_variant ? "\\\"" : "\"\"");
     pos += 2;
   }
-  out << "(echo \"" << s << "\")";
+  out << "(echo \"" << s << "\")" << std::endl;
 }
 
 /*
@@ -2084,31 +2081,31 @@ void Smt2Printer::toStreamCmdSynthFun(std::ostream& out,
   {
     toStreamSygusGrammar(out, sygusType);
   }
-  out << ')';
+  out << ')' << std::endl;
 }
 
 void Smt2Printer::toStreamCmdDeclareVar(std::ostream& out,
                                         Node var,
                                         TypeNode type) const
 {
-  out << "(declare-var " << var << ' ' << type << ')';
+  out << "(declare-var " << var << ' ' << type << ')' << std::endl;
 }
 
 void Smt2Printer::toStreamCmdConstraint(std::ostream& out, Node n) const
 {
-  out << "(constraint " << n << ')';
+  out << "(constraint " << n << ')' << std::endl;
 }
 
 void Smt2Printer::toStreamCmdInvConstraint(
     std::ostream& out, Node inv, Node pre, Node trans, Node post) const
 {
   out << "(inv-constraint " << inv << ' ' << pre << ' ' << trans << ' ' << post
-      << ')';
+      << ')' << std::endl;
 }
 
 void Smt2Printer::toStreamCmdCheckSynth(std::ostream& out) const
 {
-  out << "(check-synth)";
+  out << "(check-synth)" << std::endl;
 }
 
 void Smt2Printer::toStreamCmdGetAbduct(std::ostream& out,
@@ -2125,7 +2122,7 @@ void Smt2Printer::toStreamCmdGetAbduct(std::ostream& out,
   {
     toStreamSygusGrammar(out, sygusType);
   }
-  out << ')';
+  out << ')' << std::endl;
 }
 
 /*
diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp
index e54d976c9..03d614433 100644
--- a/src/proof/unsat_core.cpp
+++ b/src/proof/unsat_core.cpp
@@ -20,7 +20,6 @@
 #include "expr/expr_iomanip.h"
 #include "options/base_options.h"
 #include "printer/printer.h"
-#include "smt/command.h"
 #include "smt/smt_engine_scope.h"
 
 namespace CVC4 {
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index c46cd5136..203ed34e9 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -31,7 +31,9 @@
 #include "prop/minisat/minisat.h"
 #include "prop/prop_engine.h"
 #include "prop/theory_proxy.h"
-#include "smt/command.h"
+#include "smt/dump.h"
+#include "smt/smt_engine.h"
+#include "printer/printer.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
@@ -42,10 +44,14 @@ using namespace CVC4::kind;
 namespace CVC4 {
 namespace prop {
 
-CnfStream::CnfStream(SatSolver* satSolver, Registrar* registrar,
-                     context::Context* context, bool fullLitToNodeMap,
+CnfStream::CnfStream(SatSolver* satSolver,
+                     Registrar* registrar,
+                     context::Context* context,
+                     OutputManager* outMgr,
+                     bool fullLitToNodeMap,
                      std::string name)
     : d_satSolver(satSolver),
+      d_outMgr(outMgr),
       d_booleanVariables(context),
       d_nodeToLiteralMap(context),
       d_literalToNodeMap(context),
@@ -54,32 +60,41 @@ CnfStream::CnfStream(SatSolver* satSolver, Registrar* registrar,
       d_registrar(registrar),
       d_name(name),
       d_cnfProof(NULL),
-      d_removable(false) {
+      d_removable(false)
+{
 }
 
 TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver,
                                    Registrar* registrar,
                                    context::Context* context,
+                                   OutputManager* outMgr,
                                    ResourceManager* rm,
                                    bool fullLitToNodeMap,
                                    std::string name)
-    : CnfStream(satSolver, registrar, context, fullLitToNodeMap, name),
+    : CnfStream(satSolver, registrar, context, outMgr, fullLitToNodeMap, name),
       d_resourceManager(rm)
 {}
 
 void CnfStream::assertClause(TNode node, SatClause& c) {
   Debug("cnf") << "Inserting into stream " << c << " node = " << node << endl;
-  if(Dump.isOn("clauses")) {
-    if(c.size() == 1) {
-      Dump("clauses") << AssertCommand(Expr(getNode(c[0]).toExpr()));
-    } else {
+  if (Dump.isOn("clauses") && d_outMgr != nullptr)
+  {
+    const Printer& printer = d_outMgr->getPrinter();
+    std::ostream& out = d_outMgr->getDumpOut();
+    if (c.size() == 1)
+    {
+      printer.toStreamCmdAssert(out, getNode(c[0]));
+    }
+    else
+    {
       Assert(c.size() > 1);
       NodeBuilder<> b(kind::OR);
-      for(unsigned i = 0; i < c.size(); ++i) {
+      for (unsigned i = 0; i < c.size(); ++i)
+      {
         b << getNode(c[i]);
       }
       Node n = b;
-      Dump("clauses") << AssertCommand(Expr(n.toExpr()));
+      printer.toStreamCmdAssert(out, n);
     }
   }
 
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index aec4257f2..f538a60a1 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -34,6 +34,8 @@
 
 namespace CVC4 {
 
+class OutputManager;
+
 namespace prop {
 
 class PropEngine;
@@ -56,6 +58,9 @@ class CnfStream {
   /** The SAT solver we will be using */
   SatSolver* d_satSolver;
 
+  /** Reference to the output manager of the smt engine */
+  OutputManager* d_outMgr;
+
   /** Boolean variables that we translated */
   context::CDList<TNode> d_booleanVariables;
 
@@ -166,12 +171,17 @@ class CnfStream {
    * @param satSolver the sat solver to use.
    * @param registrar the entity that takes care of preregistration of Nodes.
    * @param context the context that the CNF should respect.
+   * @param outMgr Reference to the output manager of the smt engine. Assertions
+   * will not be dumped if outMgr == nullptr.
    * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping.
    * @param name string identifier to distinguish between different instances
    * even for non-theory literals.
    */
-  CnfStream(SatSolver* satSolver, Registrar* registrar,
-            context::Context* context, bool fullLitToNodeMap = false,
+  CnfStream(SatSolver* satSolver,
+            Registrar* registrar,
+            context::Context* context,
+            OutputManager* outMgr = nullptr,
+            bool fullLitToNodeMap = false,
             std::string name = "");
 
   /**
@@ -256,6 +266,8 @@ class TseitinCnfStream : public CnfStream {
    * @param satSolver the sat solver to use
    * @param registrar the entity that takes care of pre-registration of Nodes
    * @param context the context that the CNF should respect.
+   * @param outMgr reference to the output manager of the smt engine. Assertions
+   * will not be dumped if outMgr == nullptr.
    * @param rm the resource manager of the CNF stream
    * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping,
    * even for non-theory literals
@@ -263,6 +275,7 @@ class TseitinCnfStream : public CnfStream {
   TseitinCnfStream(SatSolver* satSolver,
                    Registrar* registrar,
                    context::Context* context,
+                   OutputManager* outMgr,
                    ResourceManager* rm,
                    bool fullLitToNodeMap = false,
                    std::string name = "");
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 311224a03..e769ba6cc 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -669,9 +669,6 @@ void Solver::cancelUntil(int level) {
         // Pop the SMT context
         for (int l = trail_lim.size() - level; l > 0; --l) {
           d_context->pop();
-          if(Dump.isOn("state")) {
-            d_proxy->dumpStatePop();
-          }
         }
         for (int c = trail.size()-1; c >= trail_lim[level]; c--){
             Var      x  = var(trail[c]);
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index a5f3664e8..0630df1b7 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -572,10 +572,6 @@ inline void Solver::newDecisionLevel()
   trail_lim.push(trail.size());
   flipped.push(false);
   d_context->push();
-  if (Dump.isOn("state"))
-  {
-    Dump("state") << CVC4::PushCommand();
-  }
 }
 
 inline int      Solver::decisionLevel ()      const   { return trail_lim.size(); }
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index e71e681e5..4b114aa2c 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -34,7 +34,6 @@
 #include "prop/sat_solver.h"
 #include "prop/sat_solver_factory.h"
 #include "prop/theory_proxy.h"
-#include "smt/command.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_registrar.h"
@@ -70,7 +69,8 @@ public:
 PropEngine::PropEngine(TheoryEngine* te,
                        Context* satContext,
                        UserContext* userContext,
-                       ResourceManager* rm)
+                       ResourceManager* rm,
+                       OutputManager& outMgr)
     : d_inCheckSat(false),
       d_theoryEngine(te),
       d_context(satContext),
@@ -79,7 +79,8 @@ PropEngine::PropEngine(TheoryEngine* te,
       d_registrar(NULL),
       d_cnfStream(NULL),
       d_interrupted(false),
-      d_resourceManager(rm)
+      d_resourceManager(rm),
+      d_outMgr(outMgr)
 {
 
   Debug("prop") << "Constructing the PropEngine" << endl;
@@ -91,7 +92,7 @@ PropEngine::PropEngine(TheoryEngine* te,
 
   d_registrar = new theory::TheoryRegistrar(d_theoryEngine);
   d_cnfStream = new CVC4::prop::TseitinCnfStream(
-      d_satSolver, d_registrar, userContext, rm, true);
+      d_satSolver, d_registrar, userContext, &d_outMgr, rm, true);
 
   d_theoryProxy = new TheoryProxy(
       this, d_theoryEngine, d_decisionEngine.get(), d_context, d_cnfStream);
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 1df862568..75f628d9a 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -36,6 +36,7 @@ namespace CVC4 {
 
 class ResourceManager;
 class DecisionEngine;
+class OutputManager;
 class TheoryEngine;
 
 namespace theory {
@@ -62,7 +63,8 @@ class PropEngine
   PropEngine(TheoryEngine*,
              context::Context* satContext,
              context::UserContext* userContext,
-             ResourceManager* rm);
+             ResourceManager* rm,
+             OutputManager& outMgr);
 
   /**
    * Destructor.
@@ -255,6 +257,8 @@ class PropEngine
   /** Pointer to resource manager for associated SmtEngine */
   ResourceManager* d_resourceManager;
 
+  /** Reference to the output manager of the smt engine */
+  OutputManager& d_outMgr;
 };
 
 }  // namespace prop
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 8165c5d8a..a89c8799f 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -22,7 +22,6 @@
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"
 #include "proof/cnf_proof.h"
-#include "smt/command.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
@@ -150,11 +149,5 @@ SatValue TheoryProxy::getDecisionPolarity(SatVariable var) {
   return d_decisionEngine->getPolarity(var);
 }
 
-void TheoryProxy::dumpStatePop() {
-  if(Dump.isOn("state")) {
-    Dump("state") << PopCommand();
-  }
-}
-
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 7fd735bf2..688bd4e1c 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -88,9 +88,6 @@ class TheoryProxy
 
   SatValue getDecisionPolarity(SatVariable var);
 
-  /** Shorthand for Dump("state") << PopCommand() */
-  void dumpStatePop();
-
  private:
   /** The prop engine we are using. */
   PropEngine* d_propEngine;
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 64ef60906..38c799fca 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -106,20 +106,6 @@ std::ostream& operator<<(std::ostream& out, BenchmarkStatus status)
 }
 
 // !!! Temporary until commands are migrated to the new API !!!
-std::vector<Node> exprVectorToNodes(const std::vector<Expr>& exprs)
-{
-  std::vector<Node> nodes;
-  nodes.reserve(exprs.size());
-
-  for (Expr e : exprs)
-  {
-    nodes.push_back(Node::fromExpr(e));
-  }
-
-  return nodes;
-}
-
-// !!! Temporary until commands are migrated to the new API !!!
 std::vector<TypeNode> typeVectorToTypeNodes(const std::vector<Type>& types)
 {
   std::vector<TypeNode> typeNodes;
@@ -2977,7 +2963,7 @@ void SetBenchmarkStatusCommand::toStream(std::ostream& out,
                                          size_t dag,
                                          OutputLanguage language) const
 {
-  Result::Sat status;
+  Result::Sat status = Result::SAT_UNKNOWN;
   switch (d_status)
   {
     case BenchmarkStatus::SMT_SATISFIABLE: status = Result::SAT; break;
diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp
index d8d486e12..28cf8a34f 100644
--- a/src/smt/dump.cpp
+++ b/src/smt/dump.cpp
@@ -19,9 +19,29 @@
 #include "base/output.h"
 #include "lib/strtok_r.h"
 #include "preprocessing/preprocessing_pass_registry.h"
+#include "smt/command.h"
+#include "smt/node_command.h"
 
 namespace CVC4 {
 
+CVC4dumpstream& CVC4dumpstream::operator<<(const Command& c)
+{
+  if (d_os != nullptr)
+  {
+    (*d_os) << c;
+  }
+  return *this;
+}
+
+CVC4dumpstream& CVC4dumpstream::operator<<(const NodeCommand& nc)
+{
+  if (d_os != nullptr)
+  {
+    (*d_os) << nc;
+  }
+  return *this;
+}
+
 DumpC DumpChannel CVC4_PUBLIC;
 
 std::ostream& DumpC::setStream(std::ostream* os) {
@@ -100,42 +120,6 @@ void DumpC::setDumpFromString(const std::string& optarg) {
                || !strcmp(optargPtr, "bv-rewrites")
                || !strcmp(optargPtr, "theory::fullcheck"))
       {
-        // These are "non-state-dumping" modes.  If state (SAT decisions,
-        // propagations, etc.) is dumped, it will interfere with the validity
-        // of these generated queries.
-        if (Dump.isOn("state"))
-        {
-          throw OptionException(std::string("dump option `") + optargPtr +
-                              "' conflicts with a previous, "
-                              "state-dumping dump option.  You cannot "
-                              "mix stateful and non-stateful dumping modes; "
-                              "see --dump help.");
-        }
-        else
-        {
-          Dump.on("no-permit-state");
-        }
-      }
-      else if (!strcmp(optargPtr, "state")
-               || !strcmp(optargPtr, "missed-t-conflicts")
-               || !strcmp(optargPtr, "t-propagations")
-               || !strcmp(optargPtr, "missed-t-propagations"))
-      {
-        // These are "state-dumping" modes.  If state (SAT decisions,
-        // propagations, etc.) is not dumped, it will interfere with the
-        // validity of these generated queries.
-        if (Dump.isOn("no-permit-state"))
-        {
-          throw OptionException(std::string("dump option `") + optargPtr +
-                              "' conflicts with a previous, "
-                              "non-state-dumping dump option.  You cannot "
-                              "mix stateful and non-stateful dumping modes; "
-                              "see --dump help.");
-        }
-        else
-        {
-          Dump.on("state");
-        }
       }
       else if (!strcmp(optargPtr, "help"))
       {
@@ -152,14 +136,6 @@ void DumpC::setDumpFromString(const std::string& optarg) {
         puts(ss.str().c_str());
         exit(1);
       }
-      else if (!strcmp(optargPtr, "bv-abstraction"))
-      {
-        Dump.on("bv-abstraction");
-      }
-      else if (!strcmp(optargPtr, "bv-algebraic"))
-      {
-        Dump.on("bv-algebraic");
-      }
       else
       {
         throw OptionException(std::string("unknown option for --dump: `")
@@ -222,49 +198,25 @@ clauses\n\
 + Do all the preprocessing outlined above, and dump the CNF-converted\n\
   output\n\
 \n\
-state\n\
-+ Dump all contextual assertions (e.g., SAT decisions, propagations..).\n\
-  Implied by all \"stateful\" modes below and conflicts with all\n\
-  non-stateful modes below.\n\
-\n\
-t-conflicts [non-stateful]\n\
+t-conflicts\n\
 + Output correctness queries for all theory conflicts\n\
 \n\
-missed-t-conflicts [stateful]\n\
-+ Output completeness queries for theory conflicts\n\
-\n\
-t-propagations [stateful]\n\
-+ Output correctness queries for all theory propagations\n\
-\n\
-missed-t-propagations [stateful]\n\
-+ Output completeness queries for theory propagations (LARGE and EXPENSIVE)\n\
-\n\
-t-lemmas [non-stateful]\n\
+t-lemmas\n\
 + Output correctness queries for all theory lemmas\n\
 \n\
-t-explanations [non-stateful]\n\
+t-explanations\n\
 + Output correctness queries for all theory explanations\n\
 \n\
-bv-rewrites [non-stateful]\n\
+bv-rewrites\n\
 + Output correctness queries for all bitvector rewrites\n\
 \n\
-bv-abstraction [non-stateful]\n\
-+ Output correctness queries for all bv abstraction \n\
-\n\
-bv-algebraic [non-stateful]\n\
-+ Output correctness queries for bv algebraic solver. \n\
-\n\
-theory::fullcheck [non-stateful]\n\
+theory::fullcheck\n\
 + Output completeness queries for all full-check effort-level theory checks\n\
 \n\
 Dump modes can be combined with multiple uses of --dump.  Generally you want\n\
 raw-benchmark or, alternatively, one from the assertions category (either\n\
-assertions or clauses), and perhaps one or more stateful or non-stateful modes\n\
+assertions or clauses), and perhaps one or more other modes\n\
 for checking correctness and completeness of decision procedure implementations.\n\
-Stateful modes dump the contextual assertions made by the core solver (all\n\
-decisions and propagations as assertions); this affects the validity of the\n\
-resulting correctness and completeness queries, so of course stateful and\n\
-non-stateful modes cannot be mixed in the same run.\n\
 \n\
 The --output-language option controls the language used for dumping, and\n\
 this allows you to connect CVC4 to another solver implementation via a UNIX\n\
diff --git a/src/smt/dump.h b/src/smt/dump.h
index 4c0efeb6e..ec13a9ae9 100644
--- a/src/smt/dump.h
+++ b/src/smt/dump.h
@@ -20,11 +20,12 @@
 #define CVC4__DUMP_H
 
 #include "base/output.h"
-#include "smt/command.h"
-#include "smt/node_command.h"
 
 namespace CVC4 {
 
+class Command;
+class NodeCommand;
+
 #if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
 
 class CVC4_PUBLIC CVC4dumpstream
@@ -33,27 +34,14 @@ class CVC4_PUBLIC CVC4dumpstream
   CVC4dumpstream() : d_os(nullptr) {}
   CVC4dumpstream(std::ostream& os) : d_os(&os) {}
 
-  CVC4dumpstream& operator<<(const Command& c) {
-    if (d_os != nullptr)
-    {
-      (*d_os) << c << std::endl;
-    }
-    return *this;
-  }
+  CVC4dumpstream& operator<<(const Command& c);
 
   /** 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;
-  }
+  CVC4dumpstream& operator<<(const NodeCommand& nc);
 
  private:
   std::ostream* d_os;
diff --git a/src/smt/dump_manager.cpp b/src/smt/dump_manager.cpp
index 033be405f..849339106 100644
--- a/src/smt/dump_manager.cpp
+++ b/src/smt/dump_manager.cpp
@@ -17,6 +17,7 @@
 #include "expr/expr_manager.h"
 #include "options/smt_options.h"
 #include "smt/dump.h"
+#include "smt/node_command.h"
 
 namespace CVC4 {
 namespace smt {
@@ -98,11 +99,11 @@ void DumpManager::setPrintFuncInModel(Node f, bool p)
   Trace("setp-model") << "Set printInModel " << f << " to " << p << std::endl;
   for (std::unique_ptr<NodeCommand>& c : d_modelGlobalCommands)
   {
-    DeclareFunctionCommand* dfc =
-        dynamic_cast<DeclareFunctionCommand*>(c.get());
+    DeclareFunctionNodeCommand* dfc =
+        dynamic_cast<DeclareFunctionNodeCommand*>(c.get());
     if (dfc != NULL)
     {
-      Node df = Node::fromExpr(dfc->getFunction());
+      Node df = dfc->getFunction();
       if (df == f)
       {
         dfc->setPrintInModel(p);
@@ -111,10 +112,11 @@ void DumpManager::setPrintFuncInModel(Node f, bool p)
   }
   for (NodeCommand* c : d_modelCommands)
   {
-    DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(c);
+    DeclareFunctionNodeCommand* dfc =
+        dynamic_cast<DeclareFunctionNodeCommand*>(c);
     if (dfc != NULL)
     {
-      Node df = Node::fromExpr(dfc->getFunction());
+      Node df = dfc->getFunction();
       if (df == f)
       {
         dfc->setPrintInModel(p);
diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h
index 2ce0570e4..5954817bd 100644
--- a/src/smt/dump_manager.h
+++ b/src/smt/dump_manager.h
@@ -22,9 +22,11 @@
 
 #include "context/cdlist.h"
 #include "expr/node.h"
-#include "smt/node_command.h"
 
 namespace CVC4 {
+
+class NodeCommand;
+
 namespace smt {
 
 /**
diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp
index 52ddcf156..fdf32fa41 100644
--- a/src/smt/listeners.cpp
+++ b/src/smt/listeners.cpp
@@ -18,9 +18,10 @@
 #include "expr/expr.h"
 #include "expr/node_manager_attributes.h"
 #include "options/smt_options.h"
-#include "smt/node_command.h"
+#include "printer/printer.h"
 #include "smt/dump.h"
 #include "smt/dump_manager.h"
+#include "smt/node_command.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 
@@ -36,7 +37,11 @@ void ResourceOutListener::notify()
   d_smt.interrupt();
 }
 
-SmtNodeManagerListener::SmtNodeManagerListener(DumpManager& dm) : d_dm(dm) {}
+SmtNodeManagerListener::SmtNodeManagerListener(DumpManager& dm,
+                                               OutputManager& outMgr)
+    : d_dm(dm), d_outMgr(outMgr)
+{
+}
 
 void SmtNodeManagerListener::nmNotifyNewSort(TypeNode tn, uint32_t flags)
 {
@@ -92,7 +97,8 @@ void SmtNodeManagerListener::nmNotifyNewSkolem(TNode n,
   DeclareFunctionNodeCommand c(id, n, n.getType());
   if (Dump.isOn("skolems") && comment != "")
   {
-    Dump("skolems") << CommentCommand(id + " is " + comment);
+    d_outMgr.getPrinter().toStreamCmdComment(d_outMgr.getDumpOut(),
+                                             id + " is " + comment);
   }
   if ((flags & ExprManager::VAR_FLAG_DEFINED) == 0)
   {
diff --git a/src/smt/listeners.h b/src/smt/listeners.h
index 77d6d257f..0efbed096 100644
--- a/src/smt/listeners.h
+++ b/src/smt/listeners.h
@@ -24,6 +24,7 @@
 
 namespace CVC4 {
 
+class OutputManager;
 class SmtEngine;
 
 namespace smt {
@@ -49,7 +50,7 @@ class DumpManager;
 class SmtNodeManagerListener : public NodeManagerListener
 {
  public:
-  SmtNodeManagerListener(DumpManager& dm);
+  SmtNodeManagerListener(DumpManager& dm, OutputManager& outMgr);
   /** Notify when new sort is created */
   void nmNotifyNewSort(TypeNode tn, uint32_t flags) override;
   /** Notify when new sort constructor is created */
@@ -69,6 +70,8 @@ class SmtNodeManagerListener : public NodeManagerListener
  private:
   /** Reference to the dump manager of smt engine */
   DumpManager& d_dm;
+  /** Reference to the output manager of the smt engine */
+  OutputManager& d_outMgr;
 };
 
 }  // namespace smt
diff --git a/src/smt/output_manager.cpp b/src/smt/output_manager.cpp
new file mode 100644
index 000000000..a801b7527
--- /dev/null
+++ b/src/smt/output_manager.cpp
@@ -0,0 +1,35 @@
+/*********************                                                        */
+/*! \file output_manager.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Abdalrhman Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of OutputManager functions.
+ **
+ ** Implementation of OutputManager functions.
+ **/
+
+#include "smt/output_manager.h"
+
+#include "smt/smt_engine.h"
+
+namespace CVC4 {
+
+OutputManager::OutputManager(SmtEngine* smt) : d_smt(smt) {}
+
+const Printer& OutputManager::getPrinter() const
+{
+  return *d_smt->getPrinter();
+}
+
+std::ostream& OutputManager::getDumpOut() const
+{
+  return *d_smt->getOptions().getOut();
+}
+
+}  // namespace CVC4
diff --git a/src/smt/output_manager.h b/src/smt/output_manager.h
new file mode 100644
index 000000000..5ffd6b964
--- /dev/null
+++ b/src/smt/output_manager.h
@@ -0,0 +1,57 @@
+/*********************                                                        */
+/*! \file output_manager.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Abdalrhman Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The output manager for the SmtEngine.
+ **
+ ** The output manager provides helper functions for printing commands
+ ** internally.
+ **/
+
+#ifndef CVC4__SMT__OUTPUT_MANAGER_H
+#define CVC4__SMT__OUTPUT_MANAGER_H
+
+#include <ostream>
+
+namespace CVC4 {
+
+class Printer;
+class SmtEngine;
+
+/** This utility class provides helper functions for printing commands
+ * internally */
+class OutputManager
+{
+ public:
+  /** Constructor
+   *
+   * @param smt SMT engine to manage output for
+   */
+  explicit OutputManager(SmtEngine* smt);
+
+  /** Get the current printer based on the current options
+   *
+   * @return the current printer
+   */
+  const Printer& getPrinter() const;
+
+  /** Get the output stream that --dump=X should print to
+   *
+   * @return the output stream
+   */
+  std::ostream& getDumpOut() const;
+
+ private:
+  SmtEngine* d_smt;
+};
+
+}  // namespace CVC4
+
+#endif  // CVC4__SMT__OUTPUT_MANAGER_H
diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index ea5ef2bad..c376c99ba 100644
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -15,9 +15,10 @@
 #include "smt/preprocessor.h"
 
 #include "options/smt_options.h"
+#include "printer/printer.h"
 #include "smt/abstract_values.h"
 #include "smt/assertions.h"
-#include "smt/command.h"
+#include "smt/dump.h"
 #include "smt/smt_engine.h"
 
 using namespace CVC4::theory;
@@ -128,7 +129,8 @@ Node Preprocessor::simplify(const Node& node, bool removeItes)
   Trace("smt") << "SMT simplify(" << node << ")" << endl;
   if (Dump.isOn("benchmark"))
   {
-    Dump("benchmark") << SimplifyCommand(node.toExpr());
+    d_smt.getOutputManager().getPrinter().toStreamCmdSimplify(
+        d_smt.getOutputManager().getDumpOut(), node);
   }
   Node nas = d_absValues.substituteAbstractValues(node);
   if (options::typeChecking())
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 33d092def..944f35593 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -27,7 +27,9 @@
 #include "options/uf_options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_registry.h"
+#include "printer/printer.h"
 #include "smt/defined_function.h"
+#include "smt/dump.h"
 #include "smt/smt_engine.h"
 #include "theory/logic_info.h"
 #include "theory/quantifiers/fun_def_process.h"
@@ -562,7 +564,8 @@ void ProcessAssertions::dumpAssertions(const char* key,
     for (unsigned i = 0; i < assertionList.size(); ++i)
     {
       TNode n = assertionList[i];
-      Dump("assertions") << AssertCommand(Expr(n.toExpr()));
+      d_smt.getOutputManager().getPrinter().toStreamCmdAssert(
+          d_smt.getOutputManager().getDumpOut(), n);
     }
   }
 }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d271ca05d..d520d664c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -71,7 +71,7 @@
 #include "smt/abduction_solver.h"
 #include "smt/abstract_values.h"
 #include "smt/assertions.h"
-#include "smt/command.h"
+#include "smt/node_command.h"
 #include "smt/defined_function.h"
 #include "smt/dump_manager.h"
 #include "smt/expr_names.h"
@@ -114,9 +114,19 @@ using namespace CVC4::theory;
 
 namespace CVC4 {
 
-namespace smt {
+// !!! Temporary until commands are migrated to the new API !!!
+std::vector<Node> exprVectorToNodes(const std::vector<Expr>& exprs)
+{
+  std::vector<Node> nodes;
+  nodes.reserve(exprs.size());
 
-}/* namespace CVC4::smt */
+  for (Expr e : exprs)
+  {
+    nodes.push_back(Node::fromExpr(e));
+  }
+
+  return nodes;
+}
 
 SmtEngine::SmtEngine(ExprManager* em, Options* optr)
     : d_state(new SmtEngineState(*this)),
@@ -127,7 +137,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       d_exprNames(new ExprNames(getUserContext())),
       d_dumpm(new DumpManager(getUserContext())),
       d_routListener(new ResourceOutListener(*this)),
-      d_snmListener(new SmtNodeManagerListener(*d_dumpm.get())),
+      d_snmListener(new SmtNodeManagerListener(*d_dumpm.get(), d_outMgr)),
       d_smtSolver(nullptr),
       d_proofManager(nullptr),
       d_pfManager(nullptr),
@@ -143,6 +153,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       d_isInternalSubsolver(false),
       d_statisticsRegistry(nullptr),
       d_stats(nullptr),
+      d_outMgr(this),
       d_resourceManager(nullptr),
       d_optm(nullptr),
       d_pp(nullptr),
@@ -183,7 +194,8 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
   d_smtSolver.reset(
       new SmtSolver(*this, *d_state, d_resourceManager.get(), *d_pp, *d_stats));
   // make the SyGuS solver
-  d_sygusSolver.reset(new SygusSolver(*d_smtSolver, *d_pp, getUserContext()));
+  d_sygusSolver.reset(
+      new SygusSolver(*d_smtSolver, *d_pp, getUserContext(), d_outMgr));
   // make the quantifier elimination solver
   d_quantElimSolver.reset(new QuantElimSolver(*d_smtSolver));
 
@@ -285,12 +297,13 @@ void SmtEngine::finishInit()
   {
       LogicInfo everything;
       everything.lock();
-      Dump("benchmark") << CommentCommand(
+      getOutputManager().getPrinter().toStreamCmdComment(
+          getOutputManager().getDumpOut(),
           "CVC4 always dumps the most general, all-supported logic (below), as "
           "some internals might require the use of a logic more general than "
-          "the input.")
-                        << SetBenchmarkLogicCommand(
-                               everything.getLogicString());
+          "the input.");
+      getOutputManager().getPrinter().toStreamCmdSetBenchmarkLogic(
+          getOutputManager().getDumpOut(), everything.getLogicString());
   }
 
   // initialize the dump manager
@@ -404,8 +417,8 @@ void SmtEngine::setLogic(const std::string& s)
     // dump out a set-logic command
     if (Dump.isOn("raw-benchmark"))
     {
-      Dump("raw-benchmark")
-          << SetBenchmarkLogicCommand(d_logic.getLogicString());
+      getOutputManager().getPrinter().toStreamCmdSetBenchmarkLogic(
+          getOutputManager().getDumpOut(), d_logic.getLogicString());
     }
   }
   catch (IllegalArgumentException& e)
@@ -459,12 +472,14 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
   if(Dump.isOn("benchmark")) {
     if(key == "status") {
       string s = value.getValue();
-      BenchmarkStatus status =
-        (s == "sat") ? SMT_SATISFIABLE :
-          ((s == "unsat") ? SMT_UNSATISFIABLE : SMT_UNKNOWN);
-      Dump("benchmark") << SetBenchmarkStatusCommand(status);
+      Result::Sat status =
+          (s == "sat") ? Result::SAT
+                       : ((s == "unsat") ? Result::UNSAT : Result::SAT_UNKNOWN);
+      getOutputManager().getPrinter().toStreamCmdSetBenchmarkStatus(
+          getOutputManager().getDumpOut(), status);
     } else {
-      Dump("benchmark") << SetInfoCommand(key, value);
+      getOutputManager().getPrinter().toStreamCmdSetInfo(
+          getOutputManager().getDumpOut(), key, value);
     }
   }
 
@@ -774,16 +789,15 @@ void SmtEngine::defineFunctionsRec(
 
   if (Dump.isOn("raw-benchmark"))
   {
-    std::vector<api::Term> tFuncs = api::exprVectorToTerms(d_solver, funcs);
-    std::vector<std::vector<api::Term>> tFormals;
+    std::vector<Node> nFuncs = exprVectorToNodes(funcs);
+    std::vector<std::vector<Node>> nFormals;
     for (const std::vector<Expr>& formal : formals)
     {
-      tFormals.emplace_back(api::exprVectorToTerms(d_solver, formal));
+      nFormals.emplace_back(exprVectorToNodes(formal));
     }
-    std::vector<api::Term> tFormulas =
-        api::exprVectorToTerms(d_solver, formulas);
-    Dump("raw-benchmark") << DefineFunctionRecCommand(
-        d_solver, tFuncs, tFormals, tFormulas, global);
+    std::vector<Node> nFormulas = exprVectorToNodes(formulas);
+    getOutputManager().getPrinter().toStreamCmdDefineFunctionRec(
+        getOutputManager().getDumpOut(), nFuncs, nFormals, nFormulas);
   }
 
   ExprManager* em = getExprManager();
@@ -930,7 +944,11 @@ void SmtEngine::notifyPostSolvePost()
 
 Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore)
 {
-  Dump("benchmark") << CheckSatCommand(assumption);
+  if (Dump.isOn("benchmark"))
+  {
+    getOutputManager().getPrinter().toStreamCmdCheckSat(
+        getOutputManager().getDumpOut(), assumption);
+  }
   std::vector<Node> assump;
   if (!assumption.isNull())
   {
@@ -941,13 +959,18 @@ Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore)
 
 Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore)
 {
-  if (assumptions.empty())
-  {
-    Dump("benchmark") << CheckSatCommand();
-  }
-  else
+  if (Dump.isOn("benchmark"))
   {
-    Dump("benchmark") << CheckSatAssumingCommand(assumptions);
+    if (assumptions.empty())
+    {
+      getOutputManager().getPrinter().toStreamCmdCheckSat(
+          getOutputManager().getDumpOut());
+    }
+    else
+    {
+      getOutputManager().getPrinter().toStreamCmdCheckSatAssuming(
+          getOutputManager().getDumpOut(), exprVectorToNodes(assumptions));
+    }
   }
   std::vector<Node> assumps;
   for (const Expr& e : assumptions)
@@ -959,7 +982,11 @@ Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore)
 
 Result SmtEngine::checkEntailed(const Expr& node, bool inUnsatCore)
 {
-  Dump("benchmark") << QueryCommand(node, inUnsatCore);
+  if (Dump.isOn("benchmark"))
+  {
+    getOutputManager().getPrinter().toStreamCmdQuery(
+        getOutputManager().getDumpOut(), node.getNode());
+  }
   return checkSatInternal(node.isNull()
                               ? std::vector<Node>()
                               : std::vector<Node>{Node::fromExpr(node)},
@@ -1045,7 +1072,8 @@ std::vector<Node> SmtEngine::getUnsatAssumptions(void)
   finishInit();
   if (Dump.isOn("benchmark"))
   {
-    Dump("benchmark") << GetUnsatAssumptionsCommand();
+    getOutputManager().getPrinter().toStreamCmdGetUnsatAssumptions(
+        getOutputManager().getDumpOut());
   }
   UnsatCore core = getUnsatCoreInternal();
   std::vector<Node> res;
@@ -1069,7 +1097,8 @@ Result SmtEngine::assertFormula(const Node& formula, bool inUnsatCore)
   Trace("smt") << "SmtEngine::assertFormula(" << formula << ")" << endl;
 
   if (Dump.isOn("raw-benchmark")) {
-    Dump("raw-benchmark") << AssertCommand(formula.toExpr());
+    getOutputManager().getPrinter().toStreamCmdAssert(
+        getOutputManager().getDumpOut(), formula);
   }
 
   // Substitute out any abstract values in ex
@@ -1090,8 +1119,11 @@ void SmtEngine::declareSygusVar(const std::string& id, Node var, TypeNode type)
   SmtScope smts(this);
   finishInit();
   d_sygusSolver->declareSygusVar(id, var, type);
-  Dump("raw-benchmark") << DeclareSygusVarCommand(
-      id, var.toExpr(), type.toType());
+  if (Dump.isOn("raw-benchmark"))
+  {
+    getOutputManager().getPrinter().toStreamCmdDeclareVar(
+        getOutputManager().getDumpOut(), var, type);
+  }
   // don't need to set that the conjecture is stale
 }
 
@@ -1112,22 +1144,14 @@ void SmtEngine::declareSynthFun(const std::string& id,
 
   if (Dump.isOn("raw-benchmark"))
   {
-    std::stringstream ss;
-
-    Printer::getPrinter(options::outputLanguage())
-        ->toStreamCmdSynthFun(ss,
-                              id,
-                              vars,
-                              func.getType().isFunction()
-                                  ? func.getType().getRangeType()
-                                  : func.getType(),
-                              isInv,
-                              sygusType);
-
-    // must print it on the standard output channel since it is not possible
-    // to print anything except for commands with Dump.
-    std::ostream& out = *d_options.getOut();
-    out << ss.str() << std::endl;
+    getOutputManager().getPrinter().toStreamCmdSynthFun(
+        getOutputManager().getDumpOut(),
+        id,
+        vars,
+        func.getType().isFunction() ? func.getType().getRangeType()
+                                    : func.getType(),
+        isInv,
+        sygusType);
   }
 }
 
@@ -1136,7 +1160,11 @@ void SmtEngine::assertSygusConstraint(Node constraint)
   SmtScope smts(this);
   finishInit();
   d_sygusSolver->assertSygusConstraint(constraint);
-  Dump("raw-benchmark") << SygusConstraintCommand(constraint.toExpr());
+  if (Dump.isOn("raw-benchmark"))
+  {
+    getOutputManager().getPrinter().toStreamCmdConstraint(
+        getOutputManager().getDumpOut(), constraint);
+  }
 }
 
 void SmtEngine::assertSygusInvConstraint(Node inv,
@@ -1147,8 +1175,11 @@ void SmtEngine::assertSygusInvConstraint(Node inv,
   SmtScope smts(this);
   finishInit();
   d_sygusSolver->assertSygusInvConstraint(inv, pre, trans, post);
-  Dump("raw-benchmark") << SygusInvConstraintCommand(
-      inv.toExpr(), pre.toExpr(), trans.toExpr(), post.toExpr());
+  if (Dump.isOn("raw-benchmark"))
+  {
+    getOutputManager().getPrinter().toStreamCmdInvConstraint(
+        getOutputManager().getDumpOut(), inv, pre, trans, post);
+  }
 }
 
 Result SmtEngine::checkSynth()
@@ -1192,7 +1223,7 @@ Node SmtEngine::getValue(const Node& ex) const
 
   Trace("smt") << "SMT getValue(" << ex << ")" << endl;
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << GetValueCommand(ex.toExpr());
+    d_outMgr.getPrinter().toStreamCmdGetValue(d_outMgr.getDumpOut(), {ex});
   }
   TypeNode expectedType = ex.getType();
 
@@ -1290,7 +1321,8 @@ vector<pair<Expr, Expr>> SmtEngine::getAssignment()
   SmtScope smts(this);
   finishInit();
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << GetAssignmentCommand();
+    getOutputManager().getPrinter().toStreamCmdGetAssignment(
+        getOutputManager().getDumpOut());
   }
   if(!options::produceAssignments()) {
     const char* msg =
@@ -1351,7 +1383,8 @@ Model* SmtEngine::getModel() {
   finishInit();
 
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << GetModelCommand();
+    getOutputManager().getPrinter().toStreamCmdGetModel(
+        getOutputManager().getDumpOut());
   }
 
   TheoryModel* m = getAvailableModel("get model");
@@ -1384,7 +1417,8 @@ Result SmtEngine::blockModel()
 
   if (Dump.isOn("benchmark"))
   {
-    Dump("benchmark") << BlockModelCommand();
+    getOutputManager().getPrinter().toStreamCmdBlockModel(
+        getOutputManager().getDumpOut());
   }
 
   TheoryModel* m = getAvailableModel("block model");
@@ -1415,7 +1449,8 @@ Result SmtEngine::blockModelValues(const std::vector<Expr>& exprs)
       "block model values must be called on non-empty set of terms");
   if (Dump.isOn("benchmark"))
   {
-    Dump("benchmark") << BlockModelValuesCommand(exprs);
+    getOutputManager().getPrinter().toStreamCmdBlockModelValues(
+        getOutputManager().getDumpOut(), exprVectorToNodes(exprs));
   }
 
   TheoryModel* m = getAvailableModel("block model values");
@@ -1573,7 +1608,8 @@ void SmtEngine::checkModel(bool hardFailure) {
   SubstitutionMap substitutions(&fakeContext, /* substituteUnderQuantifiers = */ false);
 
   for(size_t k = 0; k < m->getNumCommands(); ++k) {
-    const DeclareFunctionCommand* c = dynamic_cast<const DeclareFunctionCommand*>(m->getCommand(k));
+    const DeclareFunctionNodeCommand* c =
+        dynamic_cast<const DeclareFunctionNodeCommand*>(m->getCommand(k));
     Notice() << "SmtEngine::checkModel(): model command " << k << " : " << m->getCommand(k) << endl;
     if(c == NULL) {
       // we don't care about DECLARE-DATATYPES, DECLARE-SORT, ...
@@ -1584,7 +1620,7 @@ void SmtEngine::checkModel(bool hardFailure) {
       // We'll first do some checks, then add to our substitution map
       // the mapping: function symbol |-> value
 
-      Expr func = c->getFunction();
+      Expr func = c->getFunction().toExpr();
       Node val = m->getValue(func);
 
       Notice() << "SmtEngine::checkModel(): adding substitution: " << func << " |-> " << val << endl;
@@ -1767,7 +1803,8 @@ UnsatCore SmtEngine::getUnsatCore() {
   SmtScope smts(this);
   finishInit();
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << GetUnsatCoreCommand();
+    getOutputManager().getPrinter().toStreamCmdGetUnsatCore(
+        getOutputManager().getDumpOut());
   }
   return getUnsatCoreInternal();
 }
@@ -1896,7 +1933,8 @@ std::vector<Expr> SmtEngine::getAssertions()
   finishInit();
   d_state->doPendingPops();
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << GetAssertionsCommand();
+    getOutputManager().getPrinter().toStreamCmdGetAssertions(
+        getOutputManager().getDumpOut());
   }
   Trace("smt") << "SMT getAssertions()" << endl;
   if(!options::produceAssertions()) {
@@ -1923,7 +1961,8 @@ void SmtEngine::push()
   Trace("smt") << "SMT push()" << endl;
   d_smtSolver->processAssertions(*d_asserts);
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << PushCommand();
+    getOutputManager().getPrinter().toStreamCmdPush(
+        getOutputManager().getDumpOut());
   }
   d_state->userPush();
 }
@@ -1933,7 +1972,8 @@ void SmtEngine::pop() {
   finishInit();
   Trace("smt") << "SMT pop()" << endl;
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << PopCommand();
+    getOutputManager().getPrinter().toStreamCmdPop(
+        getOutputManager().getDumpOut());
   }
   d_state->userPop();
 
@@ -1954,7 +1994,8 @@ void SmtEngine::reset()
   ExprManager *em = d_exprManager;
   Trace("smt") << "SMT reset()" << endl;
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << ResetCommand();
+    getOutputManager().getPrinter().toStreamCmdReset(
+        getOutputManager().getDumpOut());
   }
   std::string filename = d_state->getFilename();
   Options opts;
@@ -1983,7 +2024,8 @@ void SmtEngine::resetAssertions()
   Trace("smt") << "SMT resetAssertions()" << endl;
   if (Dump.isOn("benchmark"))
   {
-    Dump("benchmark") << ResetAssertionsCommand();
+    getOutputManager().getPrinter().toStreamCmdResetAssertions(
+        getOutputManager().getDumpOut());
   }
 
   d_state->notifyResetAssertions();
@@ -2073,7 +2115,8 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
   Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
 
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << SetOptionCommand(key, value);
+    getOutputManager().getPrinter().toStreamCmdSetOption(
+        getOutputManager().getDumpOut(), key, value);
   }
 
   if(key == "command-verbosity") {
@@ -2126,7 +2169,7 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const
   }
 
   if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << GetOptionCommand(key);
+    d_outMgr.getPrinter().toStreamCmdGetOption(d_outMgr.getDumpOut(), key);
   }
 
   if(key == "command-verbosity") {
@@ -2181,4 +2224,11 @@ ResourceManager* SmtEngine::getResourceManager()
 
 DumpManager* SmtEngine::getDumpManager() { return d_dumpm.get(); }
 
+const Printer* SmtEngine::getPrinter() const
+{
+  return Printer::getPrinter(d_options[options::outputLanguage]);
+}
+
+OutputManager& SmtEngine::getOutputManager() { return d_outMgr; }
+
 }/* CVC4 namespace */
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index eec17a5f8..d855e3181 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -31,6 +31,7 @@
 #include "options/options.h"
 #include "proof/unsat_core.h"
 #include "smt/logic_exception.h"
+#include "smt/output_manager.h"
 #include "smt/smt_mode.h"
 #include "theory/logic_info.h"
 #include "util/hash.h"
@@ -63,6 +64,8 @@ class Model;
 class LogicRequest;
 class StatisticsRegistry;
 
+class Printer;
+
 /* -------------------------------------------------------------------------- */
 
 namespace api {
@@ -130,6 +133,8 @@ namespace theory {
   class Rewriter;
 }/* CVC4::theory namespace */
 
+std::vector<Node> exprVectorToNodes(const std::vector<Expr>& exprs);
+
 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
 // hood): use a type parameter and have check() delegate, or subclass
 // SmtEngine and override check()?
@@ -862,6 +867,12 @@ class CVC4_PUBLIC SmtEngine
   /** Permit access to the underlying dump manager. */
   smt::DumpManager* getDumpManager();
 
+  /** Get the printer used by this SMT engine */
+  const Printer* getPrinter() const;
+
+  /** Get the output manager for this SMT engine */
+  OutputManager& getOutputManager();
+
   /** Get a pointer to the Rewriter owned by this SmtEngine. */
   theory::Rewriter* getRewriter() { return d_rewriter.get(); }
 
@@ -1139,6 +1150,10 @@ class CVC4_PUBLIC SmtEngine
 
   /** The options object */
   Options d_options;
+
+  /** the output manager for commands */
+  mutable OutputManager d_outMgr;
+
   /**
    * Manager for limiting time and abstract resource usage.
    */
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index c64689be6..922831106 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -51,7 +51,8 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo)
                                         d_smt.getUserContext(),
                                         d_rm,
                                         d_pp.getTermFormulaRemover(),
-                                        logicInfo));
+                                        logicInfo,
+                                        d_smt.getOutputManager()));
 
   // Add the theories
   for (theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST;
@@ -65,8 +66,11 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo)
    * are unregistered by the obsolete PropEngine object before registered
    * again by the new PropEngine object */
   d_propEngine.reset(nullptr);
-  d_propEngine.reset(new PropEngine(
-      d_theoryEngine.get(), d_smt.getContext(), d_smt.getUserContext(), d_rm));
+  d_propEngine.reset(new PropEngine(d_theoryEngine.get(),
+                                    d_smt.getContext(),
+                                    d_smt.getUserContext(),
+                                    d_rm,
+                                    d_smt.getOutputManager()));
 
   Trace("smt-debug") << "Setting up theory engine..." << std::endl;
   d_theoryEngine->setPropEngine(getPropEngine());
@@ -82,8 +86,11 @@ void SmtSolver::resetAssertions()
    * statistics are unregistered by the obsolete PropEngine object before
    * registered again by the new PropEngine object */
   d_propEngine.reset(nullptr);
-  d_propEngine.reset(new PropEngine(
-      d_theoryEngine.get(), d_smt.getContext(), d_smt.getUserContext(), d_rm));
+  d_propEngine.reset(new PropEngine(d_theoryEngine.get(),
+                                    d_smt.getContext(),
+                                    d_smt.getUserContext(),
+                                    d_rm,
+                                    d_smt.getOutputManager()));
   d_theoryEngine->setPropEngine(getPropEngine());
   // Notice that we do not reset TheoryEngine, nor does it require calling
   // finishInit again. In particular, TheoryEngine::finishInit does not
diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 0fc63d198..979eaec6d 100644
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -17,6 +17,8 @@
 #include "expr/dtype.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
+#include "printer/printer.h"
+#include "smt/dump.h"
 #include "smt/preprocessor.h"
 #include "smt/smt_solver.h"
 #include "theory/smt_engine_subsolver.h"
@@ -30,8 +32,12 @@ namespace smt {
 
 SygusSolver::SygusSolver(SmtSolver& sms,
                          Preprocessor& pp,
-                         context::UserContext* u)
-    : d_smtSolver(sms), d_pp(pp), d_sygusConjectureStale(u, true)
+                         context::UserContext* u,
+                         OutputManager& outMgr)
+    : d_smtSolver(sms),
+      d_pp(pp),
+      d_sygusConjectureStale(u, true),
+      d_outMgr(outMgr)
 {
 }
 
@@ -205,7 +211,10 @@ Result SygusSolver::checkSynth(Assertions& as)
     te->setUserAttribute("sygus", sygusVar, {}, "");
 
     Trace("smt") << "Check synthesis conjecture: " << body << std::endl;
-    Dump("raw-benchmark") << CheckSynthCommand();
+    if (Dump.isOn("raw-benchmark"))
+    {
+      d_outMgr.getPrinter().toStreamCmdCheckSynth(d_outMgr.getDumpOut());
+    }
 
     d_sygusConjectureStale = false;
 
diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h
index 621bea9f3..deb253142 100644
--- a/src/smt/sygus_solver.h
+++ b/src/smt/sygus_solver.h
@@ -24,6 +24,9 @@
 #include "util/result.h"
 
 namespace CVC4 {
+
+class OutputManager;
+
 namespace smt {
 
 class Preprocessor;
@@ -41,7 +44,10 @@ class SmtSolver;
 class SygusSolver
 {
  public:
-  SygusSolver(SmtSolver& sms, Preprocessor& pp, context::UserContext* u);
+  SygusSolver(SmtSolver& sms,
+              Preprocessor& pp,
+              context::UserContext* u,
+              OutputManager& outMgr);
   ~SygusSolver();
 
   /**
@@ -174,6 +180,8 @@ class SygusSolver
    * Whether we need to reconstruct the sygus conjecture.
    */
   context::CDO<bool> d_sygusConjectureStale;
+  /** Reference to the output manager of the smt engine */
+  OutputManager& d_outMgr;
 };
 
 }  // namespace smt
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index 85f0c30d7..00bf74360 100644
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -27,7 +27,6 @@
 #include "expr/node.h"
 #include "expr/term_context_stack.h"
 #include "expr/term_conversion_proof_generator.h"
-#include "smt/dump.h"
 #include "theory/eager_proof_generator.h"
 #include "theory/trust_node.h"
 #include "util/bool.h"
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 408f4c682..3dc19d39b 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -23,7 +23,6 @@
 #include "expr/node_algorithm.h"
 #include "options/arrays_options.h"
 #include "options/smt_options.h"
-#include "smt/command.h"
 #include "smt/logic_exception.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arrays/theory_arrays_rewriter.h"
diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index a9ec7aa53..d7899f010 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -15,12 +15,14 @@
 #include "theory/bv/abstraction.h"
 
 #include "options/bv_options.h"
+#include "printer/printer.h"
 #include "smt/dump.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 
-
 using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
@@ -691,15 +693,6 @@ Node AbstractionModule::substituteArguments(TNode signature, TNode apply, unsign
 }
 
 Node AbstractionModule::simplifyConflict(TNode conflict) {
-  if (Dump.isOn("bv-abstraction")) {
-    NodeNodeMap seen;
-    Node c = reverseAbstraction(conflict, seen);
-    Dump("bv-abstraction") << PushCommand();
-    Dump("bv-abstraction") << AssertCommand(c.toExpr());
-    Dump("bv-abstraction") << CheckSatCommand();
-    Dump("bv-abstraction") << PopCommand();
-  }
-
   Debug("bv-abstraction-dbg") << "AbstractionModule::simplifyConflict " << conflict << "\n";
   if (conflict.getKind() != kind::AND)
     return conflict;
@@ -742,16 +735,6 @@ Node AbstractionModule::simplifyConflict(TNode conflict) {
   Debug("bv-abstraction") << "AbstractionModule::simplifyConflict conflict " << conflict <<"\n";
   Debug("bv-abstraction") << "   => " << new_conflict <<"\n";
 
-  if (Dump.isOn("bv-abstraction")) {
-
-    NodeNodeMap seen;
-    Node nc = reverseAbstraction(new_conflict, seen);
-    Dump("bv-abstraction") << PushCommand();
-    Dump("bv-abstraction") << AssertCommand(nc.toExpr());
-    Dump("bv-abstraction") << CheckSatCommand();
-    Dump("bv-abstraction") << PopCommand();
-  }
-
   return new_conflict;
 }
 
@@ -836,15 +819,6 @@ void AbstractionModule::generalizeConflict(TNode conflict, std::vector<Node>& le
       lemmas.push_back(lemma);
       Debug("bv-abstraction-gen") << "adding lemma " << lemma << "\n";
       storeLemma(lemma);
-
-      if (Dump.isOn("bv-abstraction")) {
-        NodeNodeMap seen;
-        Node l = reverseAbstraction(lemma, seen);
-        Dump("bv-abstraction") << PushCommand();
-        Dump("bv-abstraction") << AssertCommand(l.toExpr());
-        Dump("bv-abstraction") << CheckSatCommand();
-        Dump("bv-abstraction") << PopCommand();
-      }
     }
   }
 }
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index 6417740fd..48aa0fbd6 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -20,6 +20,7 @@
 #include "options/bv_options.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver_factory.h"
+#include "smt/smt_engine.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/bv/bv_solver_lazy.h"
 #include "theory/bv/theory_bv.h"
@@ -71,6 +72,7 @@ EagerBitblaster::EagerBitblaster(BVSolverLazy* theory_bv, context::Context* c)
   d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(),
                                                d_bitblastingRegistrar.get(),
                                                d_nullContext.get(),
+                                               nullptr,
                                                rm,
                                                false,
                                                "EagerBitblaster"));
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index 1813784d7..93c91719b 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -21,6 +21,7 @@
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver.h"
 #include "prop/sat_solver_factory.h"
+#include "smt/smt_engine.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/bv/abstraction.h"
 #include "theory/bv/bv_solver_lazy.h"
@@ -82,6 +83,7 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c,
   d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(),
                                                d_nullRegistrar.get(),
                                                d_nullContext.get(),
+                                               nullptr,
                                                rm,
                                                false,
                                                "LazyBitblaster"));
@@ -573,8 +575,11 @@ void TLazyBitblaster::clearSolver() {
   d_satSolver.reset(
       prop::SatSolverFactory::createMinisat(d_ctx, smtStatisticsRegistry()));
   ResourceManager* rm = smt::currentResourceManager();
-  d_cnfStream.reset(new prop::TseitinCnfStream(
-      d_satSolver.get(), d_nullRegistrar.get(), d_nullContext.get(), rm));
+  d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(),
+                                               d_nullRegistrar.get(),
+                                               d_nullContext.get(),
+                                               nullptr,
+                                               rm));
   d_satSolverNotify.reset(
       d_emptyNotify
           ? (prop::BVSatSolverNotify*)new MinisatEmptyNotify()
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index e900566f9..52f68c6ef 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -19,6 +19,10 @@
 
 #include "expr/node_algorithm.h"
 #include "options/bv_options.h"
+#include "printer/printer.h"
+#include "smt/dump.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
 #include "smt_util/boolean_simplification.h"
 #include "theory/bv/bv_quick_check.h"
@@ -321,16 +325,6 @@ bool AlgebraicSolver::check(Theory::Effort e)
     TNode fact = worklist[r].node;
     unsigned id = worklist[r].id;
 
-    if (Dump.isOn("bv-algebraic")) {
-      Node expl = d_explanations[id];
-      Node query = utils::mkNot(nm->mkNode(kind::IMPLIES, expl, fact));
-      Dump("bv-algebraic") << EchoCommand("ThoeryBV::AlgebraicSolver::substitution explanation");
-      Dump("bv-algebraic") << PushCommand();
-      Dump("bv-algebraic") << AssertCommand(query.toExpr());
-      Dump("bv-algebraic") << CheckSatCommand();
-      Dump("bv-algebraic") << PopCommand();
-    }
-
     if (fact.isConst() &&
         fact.getConst<bool>() == true) {
       continue;
@@ -344,16 +338,6 @@ bool AlgebraicSolver::check(Theory::Effort e)
       d_isComplete.set(true);
       Debug("bv-subtheory-algebraic") << " UNSAT: assertion simplfies to false with conflict: "<< conflict << "\n";
 
-      if (Dump.isOn("bv-algebraic")) {
-        Dump("bv-algebraic")
-            << EchoCommand("BVSolverLazy::AlgebraicSolver::conflict");
-        Dump("bv-algebraic") << PushCommand();
-        Dump("bv-algebraic") << AssertCommand(conflict.toExpr());
-        Dump("bv-algebraic") << CheckSatCommand();
-        Dump("bv-algebraic") << PopCommand();
-      }
-
-
       ++(d_statistics.d_numSimplifiesToFalse);
       ++(d_numSolved);
       return false;
@@ -536,17 +520,6 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) {
     Node new_right = nm->mkNode(kind::BITVECTOR_XOR, right, inverse);
     bool changed = subst.addSubstitution(var, new_right, reason);
 
-    if (Dump.isOn("bv-algebraic")) {
-      Node query = utils::mkNot(nm->mkNode(
-          kind::EQUAL, fact, nm->mkNode(kind::EQUAL, var, new_right)));
-      Dump("bv-algebraic") << EchoCommand("ThoeryBV::AlgebraicSolver::substitution explanation");
-      Dump("bv-algebraic") << PushCommand();
-      Dump("bv-algebraic") << AssertCommand(query.toExpr());
-      Dump("bv-algebraic") << CheckSatCommand();
-      Dump("bv-algebraic") << PopCommand();
-    }
-
-
     return changed;
   }
 
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 0dbb51753..549843421 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -22,7 +22,10 @@
 #include <sstream>
 
 #include "context/context.h"
-#include "smt/command.h"
+#include "printer/printer.h"
+#include "smt/dump.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory.h"
 #include "util/statistics_registry.h"
@@ -449,9 +452,13 @@ public:
 
           Node condition = node.eqNode(result).notNode();
 
-          Dump("bv-rewrites")
-            << CommentCommand(os.str())
-            << CheckSatCommand(condition.toExpr());
+          const Printer& printer =
+              smt::currentSmtEngine()->getOutputManager().getPrinter();
+          std::ostream& out =
+              smt::currentSmtEngine()->getOutputManager().getDumpOut();
+
+          printer.toStreamCmdComment(out, os.str());
+          printer.toStreamCmdCheckSat(out, condition);
         }
       }
       Debug("theory::bv::rewrite") << "RewriteRule<" << rule << ">(" << node << ") => " << result << std::endl;
diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h
index f5c13b183..0e1c5f6ce 100644
--- a/src/theory/quantifiers/skolemize.h
+++ b/src/theory/quantifiers/skolemize.h
@@ -26,6 +26,9 @@
 #include "theory/quantifiers/quant_util.h"
 
 namespace CVC4 {
+
+class DTypeConstructor;
+
 namespace theory {
 namespace quantifiers {
 
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
index b89015b00..bd9697084 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -17,6 +17,7 @@
 #include "expr/dtype.h"
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
+#include "smt/command.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/first_order_model.h"
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 77652f874..da651d259 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -32,8 +32,6 @@
 #include "expr/node.h"
 #include "options/options.h"
 #include "options/theory_options.h"
-#include "smt/command.h"
-#include "smt/dump.h"
 #include "smt/logic_request.h"
 #include "theory/assertion.h"
 #include "theory/care_graph.h"
@@ -911,10 +909,6 @@ inline theory::Assertion Theory::get() {
 
   Trace("theory") << "Theory::get() => " << fact << " (" << d_facts.size() - d_factsHead << " left)" << std::endl;
 
-  if(Dump.isOn("state")) {
-    Dump("state") << AssertCommand(fact.d_assertion.toExpr());
-  }
-
   return fact;
 }
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 7ff073cf3..b5167ffe4 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -31,6 +31,8 @@
 #include "options/quantifiers_options.h"
 #include "options/theory_options.h"
 #include "preprocessing/assertion_pipeline.h"
+#include "printer/printer.h"
+#include "smt/dump.h"
 #include "smt/logic_exception.h"
 #include "smt/term_formula_removal.h"
 #include "theory/arith/arith_ite_utils.h"
@@ -211,17 +213,18 @@ TheoryEngine::TheoryEngine(context::Context* context,
                            context::UserContext* userContext,
                            ResourceManager* rm,
                            RemoveTermFormulas& iteRemover,
-                           const LogicInfo& logicInfo)
+                           const LogicInfo& logicInfo,
+                           OutputManager& outMgr)
     : d_propEngine(nullptr),
       d_context(context),
       d_userContext(userContext),
       d_logicInfo(logicInfo),
+      d_outMgr(outMgr),
       d_pnm(nullptr),
       d_lazyProof(
-          d_pnm != nullptr
-              ? new LazyCDProof(
-                    d_pnm, nullptr, d_userContext, "TheoryEngine::LazyCDProof")
-              : nullptr),
+          d_pnm != nullptr ? new LazyCDProof(
+              d_pnm, nullptr, d_userContext, "TheoryEngine::LazyCDProof")
+                           : nullptr),
       d_tepg(new TheoryEngineProofGenerator(d_pnm, d_userContext)),
       d_sharedTerms(this, context),
       d_tc(nullptr),
@@ -231,8 +234,6 @@ TheoryEngine::TheoryEngine(context::Context* context,
       d_preRegistrationVisitor(this, context),
       d_sharedTermsVisitor(d_sharedTerms),
       d_eager_model_building(false),
-      d_possiblePropagations(context),
-      d_hasPropagated(context),
       d_inConflict(context, false),
       d_inSatMode(false),
       d_hasShutDown(false),
@@ -285,11 +286,8 @@ TheoryEngine::~TheoryEngine() {
 
 void TheoryEngine::interrupt() { d_interrupted = true; }
 void TheoryEngine::preRegister(TNode preprocessed) {
-
-  Debug("theory") << "TheoryEngine::preRegister( " << preprocessed << ")" << std::endl;
-  if(Dump.isOn("missed-t-propagations")) {
-    d_possiblePropagations.push_back(preprocessed);
-  }
+  Debug("theory") << "TheoryEngine::preRegister( " << preprocessed << ")"
+                  << std::endl;
   d_preregisterQueue.push(preprocessed);
 
   if (!d_inPreregister) {
@@ -400,26 +398,28 @@ void TheoryEngine::printAssertions(const char* tag) {
 
 void TheoryEngine::dumpAssertions(const char* tag) {
   if (Dump.isOn(tag)) {
-    Dump(tag) << CommentCommand("Starting completeness check");
+    const Printer& printer = d_outMgr.getPrinter();
+    std::ostream& out = d_outMgr.getDumpOut();
+    printer.toStreamCmdComment(out, "Starting completeness check");
     for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
       Theory* theory = d_theoryTable[theoryId];
       if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
-        Dump(tag) << CommentCommand("Completeness check");
-        Dump(tag) << PushCommand();
+        printer.toStreamCmdComment(out, "Completeness check");
+        printer.toStreamCmdPush(out);
 
         // Dump the shared terms
         if (d_logicInfo.isSharingEnabled()) {
-          Dump(tag) << CommentCommand("Shared terms");
+          printer.toStreamCmdComment(out, "Shared terms");
           context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end();
           for (unsigned i = 0; it != it_end; ++ it, ++i) {
               stringstream ss;
               ss << (*it);
-              Dump(tag) << CommentCommand(ss.str());
+              printer.toStreamCmdComment(out, ss.str());
           }
         }
 
         // Dump the assertions
-        Dump(tag) << CommentCommand("Assertions");
+        printer.toStreamCmdComment(out, "Assertions");
         context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
         for (; it != it_end; ++ it) {
           // Get the assertion
@@ -428,17 +428,17 @@ void TheoryEngine::dumpAssertions(const char* tag) {
 
           if ((*it).d_isPreregistered)
           {
-            Dump(tag) << CommentCommand("Preregistered");
+            printer.toStreamCmdComment(out, "Preregistered");
           }
           else
           {
-            Dump(tag) << CommentCommand("Shared assertion");
+            printer.toStreamCmdComment(out, "Shared assertion");
           }
-          Dump(tag) << AssertCommand(assertionNode.toExpr());
+          printer.toStreamCmdAssert(out, assertionNode);
         }
-        Dump(tag) << CheckSatCommand();
+        printer.toStreamCmdCheckSat(out);
 
-        Dump(tag) << PopCommand();
+        printer.toStreamCmdPop(out);
       }
     }
   }
@@ -516,12 +516,6 @@ void TheoryEngine::check(Theory::Effort effort) {
       // Do the checking
       CVC4_FOR_EACH_THEORY;
 
-      if(Dump.isOn("missed-t-conflicts")) {
-        Dump("missed-t-conflicts")
-            << CommentCommand("Completeness check for T-conflicts; expect sat")
-            << CheckSatCommand();
-      }
-
       Debug("theory") << "TheoryEngine::check(" << effort << "): running propagation after the initial check" << endl;
 
       // We are still satisfiable, propagate as much as possible
@@ -622,25 +616,6 @@ void TheoryEngine::propagate(Theory::Effort effort)
 
   // Propagate for each theory using the statement above
   CVC4_FOR_EACH_THEORY;
-
-  if(Dump.isOn("missed-t-propagations")) {
-    for(unsigned i = 0; i < d_possiblePropagations.size(); ++i) {
-      Node atom = d_possiblePropagations[i];
-      bool value;
-      if(d_propEngine->hasValue(atom, value)) {
-        continue;
-      }
-      // Doesn't have a value, check it (and the negation)
-      if(d_hasPropagated.find(atom) == d_hasPropagated.end()) {
-        Dump("missed-t-propagations")
-          << CommentCommand("Completeness check for T-propagations; expect invalid")
-          << EchoCommand(atom.toString())
-          << QueryCommand(atom.toExpr())
-          << EchoCommand(atom.notNode().toString())
-          << QueryCommand(atom.notNode().toExpr());
-      }
-    }
-  }
 }
 
 Node TheoryEngine::getNextDecisionRequest()
@@ -1134,14 +1109,6 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
 
   // spendResource();
 
-  if(Dump.isOn("t-propagations")) {
-    Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid")
-                           << QueryCommand(literal.toExpr());
-  }
-  if(Dump.isOn("missed-t-propagations")) {
-    d_hasPropagated.insert(literal);
-  }
-
   // Get the atom
   bool polarity = literal.getKind() != kind::NOT;
   TNode atom = polarity ? literal : literal[0];
@@ -1484,8 +1451,10 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma,
   if(Dump.isOn("t-lemmas")) {
     // we dump the negation of the lemma, to show validity of the lemma
     Node n = lemma.negate();
-    Dump("t-lemmas") << CommentCommand("theory lemma: expect valid")
-                     << CheckSatCommand(n.toExpr());
+    const Printer& printer = d_outMgr.getPrinter();
+    std::ostream& out = d_outMgr.getDumpOut();
+    printer.toStreamCmdComment(out, "theory lemma: expect valid");
+    printer.toStreamCmdCheckSat(out, n);
   }
   bool removable = isLemmaPropertyRemovable(p);
   bool preprocess = isLemmaPropertyPreprocess(p);
@@ -1621,8 +1590,10 @@ void TheoryEngine::conflict(theory::TrustNode tconflict, TheoryId theoryId)
   d_inConflict = true;
 
   if(Dump.isOn("t-conflicts")) {
-    Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat")
-                        << CheckSatCommand(conflict.toExpr());
+    const Printer& printer = d_outMgr.getPrinter();
+    std::ostream& out = d_outMgr.getDumpOut();
+    printer.toStreamCmdComment(out, "theory conflict: expect unsat");
+    printer.toStreamCmdCheckSat(out, conflict);
   }
 
   // In the multiple-theories case, we need to reconstruct the conflict
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 550a4f496..a6258b7d6 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -33,7 +33,6 @@
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "prop/prop_engine.h"
-#include "smt/command.h"
 #include "theory/atom_requests.h"
 #include "theory/engine_output_channel.h"
 #include "theory/interrupted.h"
@@ -139,6 +138,9 @@ class TheoryEngine {
    */
   const LogicInfo& d_logicInfo;
 
+  /** Reference to the output manager of the smt engine */
+  OutputManager& d_outMgr;
+
   //--------------------------------- new proofs
   /** Proof node manager used by this theory engine, if proofs are enabled */
   ProofNodeManager* d_pnm;
@@ -182,19 +184,6 @@ class TheoryEngine {
   typedef std::unordered_map<TNode, Node, TNodeHashFunction> TNodeMap;
 
   /**
-   * Used for "missed-t-propagations" dumping mode only.  A set of all
-   * theory-propagable literals.
-   */
-  context::CDList<TNode> d_possiblePropagations;
-
-  /**
-   * Used for "missed-t-propagations" dumping mode only.  A
-   * context-dependent set of those theory-propagable literals that
-   * have been propagated.
-   */
-  context::CDHashSet<Node, NodeHashFunction> d_hasPropagated;
-
-  /**
    * Output channels for individual theories.
    */
   theory::EngineOutputChannel* d_theoryOut[theory::THEORY_LAST];
@@ -330,7 +319,8 @@ class TheoryEngine {
                context::UserContext* userContext,
                ResourceManager* rm,
                RemoveTermFormulas& iteRemover,
-               const LogicInfo& logic);
+               const LogicInfo& logic,
+               OutputManager& outMgr);
 
   /** Destroys a theory engine */
   ~TheoryEngine();
diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h
index ed00a3b8f..04e852408 100644
--- a/test/unit/parser/parser_builder_black.h
+++ b/test/unit/parser/parser_builder_black.h
@@ -28,7 +28,6 @@
 #include "options/language.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
-#include "smt/command.h"
 
 using namespace CVC4;
 using namespace CVC4::parser;
diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h
index 33fc15674..7fa429054 100644
--- a/test/unit/prop/cnf_stream_white.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -146,8 +146,11 @@ class CnfStreamWhite : public CxxTest::TestSuite {
     d_cnfContext = new context::Context();
     d_cnfRegistrar = new theory::TheoryRegistrar(d_theoryEngine);
     ResourceManager* rm = d_smt->getResourceManager();
-    d_cnfStream = new CVC4::prop::TseitinCnfStream(
-        d_satSolver, d_cnfRegistrar, d_cnfContext, rm);
+    d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver,
+                                                   d_cnfRegistrar,
+                                                   d_cnfContext,
+                                                   &d_smt->getOutputManager(),
+                                                   rm);
   }
 
   void tearDown() override