Merge branch 'master' into fixIssue5074fixIssue5074

69 files changed, 1405 insertions, 750 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/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 3e3b569af..7fa8b12e7 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -17,6 +17,8 @@ libcvc4_add_sources(
   kind_map.h
   lazy_proof.cpp
   lazy_proof.h
+  lazy_proof_chain.cpp
+  lazy_proof_chain.h
   match_trie.cpp
   match_trie.h
   node.cpp
diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp
new file mode 100644
index 000000000..a01d541eb
--- /dev/null
+++ b/src/expr/lazy_proof_chain.cpp
@@ -0,0 +1,239 @@
+/*********************                                                        */
+/*! \file lazy_proof_chain.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** 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 lazy proof utility
+ **/
+
+#include "expr/lazy_proof_chain.h"
+
+#include "expr/proof.h"
+#include "expr/proof_node_algorithm.h"
+#include "options/smt_options.h"
+
+namespace CVC4 {
+
+LazyCDProofChain::LazyCDProofChain(ProofNodeManager* pnm,
+                                   bool cyclic,
+                                   context::Context* c)
+    : d_manager(pnm), d_cyclic(cyclic), d_context(), d_gens(c ? c : &d_context)
+{
+}
+
+LazyCDProofChain::~LazyCDProofChain() {}
+
+std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact)
+{
+  Trace("lazy-cdproofchain")
+      << "LazyCDProofChain::getProofFor " << fact << "\n";
+  // which facts have had proofs retrieved for. This is maintained to avoid
+  // cycles. It also saves the proof node of the fact
+  std::unordered_map<Node, std::shared_ptr<ProofNode>, NodeHashFunction>
+      toConnect;
+  // leaves of proof node links in the chain, i.e. assumptions, yet to be
+  // expanded
+  std::unordered_map<Node,
+                     std::vector<std::shared_ptr<ProofNode>>,
+                     NodeHashFunction>
+      assumptionsToExpand;
+  // invariant of the loop below, the first iteration notwhistanding:
+  //   visit = domain(assumptionsToExpand) \ domain(toConnect)
+  std::vector<Node> visit{fact};
+  std::unordered_map<Node, bool, NodeHashFunction> visited;
+  Node cur;
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    auto itVisited = visited.find(cur);
+    // pre-traversal
+    if (itVisited == visited.end())
+    {
+      Trace("lazy-cdproofchain")
+          << "LazyCDProofChain::getProofFor: check " << cur << "\n";
+      ProofGenerator* pg = getGeneratorFor(cur);
+      if (!pg)
+      {
+        Trace("lazy-cdproofchain")
+            << "LazyCDProofChain::getProofFor: nothing to do\n";
+        // nothing to do for this fact, it'll be a leaf in the final proof node,
+        // don't post-traverse.
+        visited[cur] = true;
+        continue;
+      }
+      Trace("lazy-cdproofchain")
+          << "LazyCDProofChain::getProofFor: Call generator " << pg->identify()
+          << " for chain link " << cur << "\n";
+      std::shared_ptr<ProofNode> curPfn = pg->getProofFor(cur);
+      Trace("lazy-cdproofchain-debug")
+          << "LazyCDProofChain::getProofFor: stored proof: " << *curPfn.get()
+          << "\n";
+      // retrieve free assumptions and their respective proof nodes
+      std::map<Node, std::vector<std::shared_ptr<ProofNode>>> famap;
+      expr::getFreeAssumptionsMap(curPfn, famap);
+      if (Trace.isOn("lazy-cdproofchain"))
+      {
+        Trace("lazy-cdproofchain")
+            << "LazyCDProofChain::getProofFor: free assumptions:\n";
+        for (auto fap : famap)
+        {
+          Trace("lazy-cdproofchain")
+              << "LazyCDProofChain::getProofFor:  - " << fap.first << "\n";
+        }
+      }
+      // map node whose proof node must be expanded to the respective poof node
+      toConnect[cur] = curPfn;
+      // mark for post-traversal if we are controlling cycles
+      if (d_cyclic)
+      {
+        visit.push_back(cur);
+        visited[cur] = false;
+        Trace("lazy-cdproofchain") << push;
+        Trace("lazy-cdproofchain-debug") << push;
+      }
+      else
+      {
+        visited[cur] = true;
+      }
+      // enqueue free assumptions to process
+      for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>&
+               fap : famap)
+      {
+        // check cycles, which are cases in which the assumption has already
+        // been marked to be connected but we have not finished processing the
+        // nodes it depends on
+        if (d_cyclic && toConnect.find(fap.first) != toConnect.end()
+            && std::find(visit.begin(), visit.end(), fap.first) != visit.end())
+        {
+          // Since we have a cycle with an assumption, this fact will be an
+          // assumption in the final proof node produced by this method. This we
+          // mark the proof node it results on, i.e. its value in the toConnect
+          // map, as an assumption proof node. Note that we don't assign
+          // visited[fap.first] to true so that we properly pop the traces
+          // previously pushed.
+          Trace("lazy-cdproofchain")
+              << "LazyCDProofChain::getProofFor: removing cyclic assumption "
+              << fap.first << " from expansion\n";
+          toConnect[fap.first] = fap.second[0];
+          continue;
+        }
+        // only process further the assumptions not already in the map
+        auto it = assumptionsToExpand.find(fap.first);
+        if (it == assumptionsToExpand.end())
+        {
+          visit.push_back(fap.first);
+        }
+        // add assumption proof nodes to be updated
+        assumptionsToExpand[fap.first].insert(
+            assumptionsToExpand[fap.first].end(),
+            fap.second.begin(),
+            fap.second.end());
+      }
+    }
+    else if (!itVisited->second)
+    {
+      visited[cur] = true;
+      Trace("lazy-cdproofchain") << pop;
+      Trace("lazy-cdproofchain-debug") << pop;
+    }
+  } while (!visit.empty());
+  // expand all assumptions marked to be connected
+  for (const std::pair<const Node, std::shared_ptr<ProofNode>>& npfn :
+       toConnect)
+  {
+    auto it = assumptionsToExpand.find(npfn.first);
+    if (it == assumptionsToExpand.end())
+    {
+      Assert(npfn.first == fact);
+      continue;
+    }
+    Trace("lazy-cdproofchain")
+        << "LazyCDProofChain::getProofFor: expand assumption " << npfn.first
+        << "\n";
+    Trace("lazy-cdproofchain-debug")
+        << "LazyCDProofChain::getProofFor: ...expand to " << *npfn.second.get()
+        << "\n";
+    // update each assumption proof node
+    for (std::shared_ptr<ProofNode> pfn : it->second)
+    {
+      d_manager->updateNode(pfn.get(), npfn.second.get());
+    }
+  }
+  // final proof of fact
+  auto it = toConnect.find(fact);
+  if (it == toConnect.end())
+  {
+    return nullptr;
+  }
+  return it->second;
+}
+
+void LazyCDProofChain::addLazyStep(Node expected, ProofGenerator* pg)
+{
+  Assert(pg != nullptr);
+  Trace("lazy-cdproofchain") << "LazyCDProofChain::addLazyStep: " << expected
+                             << " set to generator " << pg->identify() << "\n";
+  // note this will replace the generator for expected, if any
+  d_gens.insert(expected, pg);
+}
+
+void LazyCDProofChain::addLazyStep(Node expected,
+                                   ProofGenerator* pg,
+                                   const std::vector<Node>& assumptions,
+                                   const char* ctx)
+{
+  Assert(pg != nullptr);
+  Trace("lazy-cdproofchain") << "LazyCDProofChain::addLazyStep: " << expected
+                             << " set to generator " << pg->identify() << "\n";
+  // note this will rewrite the generator for expected, if any
+  d_gens.insert(expected, pg);
+  // check if chain is closed if options::proofNewEagerChecking() is on
+  if (options::proofNewEagerChecking())
+  {
+    Trace("lazy-cdproofchain")
+        << "LazyCDProofChain::addLazyStep: Checking closed proof...\n";
+    std::shared_ptr<ProofNode> pfn = pg->getProofFor(expected);
+    std::vector<Node> allowedLeaves{assumptions.begin(), assumptions.end()};
+    // add all current links in the chain
+    for (const std::pair<const Node, ProofGenerator*>& link : d_gens)
+    {
+      allowedLeaves.push_back(link.first);
+    }
+    if (Trace.isOn("lazy-cdproofchain"))
+    {
+      Trace("lazy-cdproofchain") << "Checking relative to leaves...\n";
+      for (const Node& n : allowedLeaves)
+      {
+        Trace("lazy-cdproofchain") << "  - " << n << "\n";
+      }
+      Trace("lazy-cdproofchain") << "\n";
+    }
+    pfnEnsureClosedWrt(pfn.get(), allowedLeaves, "lazy-cdproofchain", ctx);
+  }
+}
+
+bool LazyCDProofChain::hasGenerator(Node fact) const
+{
+  return d_gens.find(fact) != d_gens.end();
+}
+
+ProofGenerator* LazyCDProofChain::getGeneratorFor(Node fact)
+{
+  auto it = d_gens.find(fact);
+  if (it != d_gens.end())
+  {
+    return (*it).second;
+  }
+  return nullptr;
+}
+
+std::string LazyCDProofChain::identify() const { return "LazyCDProofChain"; }
+
+}  // namespace CVC4
diff --git a/src/expr/lazy_proof_chain.h b/src/expr/lazy_proof_chain.h
new file mode 100644
index 000000000..7fa49bccc
--- /dev/null
+++ b/src/expr/lazy_proof_chain.h
@@ -0,0 +1,135 @@
+/*********************                                                        */
+/*! \file lazy_proof_chain.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** 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 Lazy proof chain utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__LAZY_PROOF_CHAIN_H
+#define CVC4__EXPR__LAZY_PROOF_CHAIN_H
+
+#include <unordered_map>
+#include <vector>
+
+#include "context/cdhashmap.h"
+#include "expr/proof_generator.h"
+#include "expr/proof_node_manager.h"
+
+namespace CVC4 {
+
+/**
+ * A (context-dependent) lazy generator for proof chains. This class is an
+ * extension of ProofGenerator that additionally that maps facts to proof
+ * generators in a context-dependent manner. The map is built with the addition
+ * of lazy steps mapping facts to proof generators. More importantly, its
+ * getProofFor method expands the proof generators registered to this class by
+ * connecting, for the proof generated to one fact, assumptions to the proofs
+ * generated for those assumptinos that are registered in the chain.
+ */
+class LazyCDProofChain : public ProofGenerator
+{
+ public:
+  /** Constructor
+   *
+   * @param pnm The proof node manager for constructing ProofNode objects.
+   * @param cyclic Whether this instance is robust to cycles in the cahin.
+   * @param c The context that this class depends on. If none is provided,
+   * this class is context-independent.
+   */
+  LazyCDProofChain(ProofNodeManager* pnm,
+                   bool cyclic = true,
+                   context::Context* c = nullptr);
+  ~LazyCDProofChain();
+  /**
+   * Get lazy proof for fact, or nullptr if it does not exist, by connecting the
+   * proof nodes generated for each intermediate relevant fact registered in the
+   * chain (i.e., in the domain of d_gens).
+   *
+   * For example, if d_gens consists of the following pairs
+   *
+   * --- (A, PG1)
+   * --- (B, PG2)
+   * --- (C, PG3)
+   *
+   * and getProofFor(A) is called, with PG1 generating a proof with assumptions
+   * B and D, then B is expanded, with its assumption proof node being updated
+   * to the expanded proof node, while D is not. Assuming PG2 provides a proof
+   * with assumptions C and E, then C is expanded and E is not. Suppose PG3
+   * gives a closed proof, thus the call getProofFor(A) produces a proof node
+   *
+   *  A : ( ... B : ( ... C : (...), ... ASSUME( E ) ), ... ASSUME( D ) )
+   *
+   * Note that the expansions are done directly on the proof nodes produced by
+   * the generators.
+   *
+   * If this instance has been set to be robust to cyclic proofs (i.e., d_cyclic
+   * is true), then the construction of the proof chain checks that there are no
+   * cycles, i.e., a given fact would have itself as an assumption when
+   * connecting the chain links. If such a cycle were to be detected then the
+   * fact will be marked as an assumption and not expanded in the final proof
+   * node. The method does not fail.
+   */
+  std::shared_ptr<ProofNode> getProofFor(Node fact) override;
+  /** Add step by generator
+   *
+   * This method stores that expected can be proven by proof generator pg if
+   * it is required to do so. This mapping is maintained in the remainder of
+   * the current context (according to the context c provided to this class).
+   *
+   * Moreover the lazy steps of this class are expected to fulfill the
+   * requirement that pg.getProofFor(expected) generates a proof node closed
+   * with relation to
+   *  (1) a fixed set F1, ..., Fn,
+   *  (2) formulas in the current domain of d_gens.
+   *
+   * This is so that we only add links to the chain that depend on a fixed set
+   * of assumptions or in other links.
+   *
+   * @param expected The fact that can be proven.
+   * @param pg The generator that can proof expected.
+   * @param assumptions The fixed set of assumptions with relation to which the
+   * chain, now augmented with expect, must be closed.
+   * @param ctx The context we are in (for debugging).
+   */
+  void addLazyStep(Node expected,
+                   ProofGenerator* pg,
+                   const std::vector<Node>& assumptions,
+                   const char* ctx = "LazyCDProofChain::addLazyStep");
+
+  /** As above but does not do the closedness check. */
+  void addLazyStep(Node expected, ProofGenerator* pg);
+
+  /** Does the given fact have an explicitly provided generator? */
+  bool hasGenerator(Node fact) const;
+
+  /**
+   * Get generator for fact, or nullptr if it doesnt exist.
+   */
+  ProofGenerator* getGeneratorFor(Node fact);
+
+  /** identify */
+  std::string identify() const override;
+
+ private:
+  /** The proof manager, used for allocating new ProofNode objects */
+  ProofNodeManager* d_manager;
+  /** Whether this instance is robust to cycles in the chain. */
+  bool d_cyclic;
+  /** A dummy context used by this class if none is provided */
+  context::Context d_context;
+  /** Maps facts that can be proven to generators */
+  context::CDHashMap<Node, ProofGenerator*, NodeHashFunction> d_gens;
+};
+
+}  // namespace CVC4
+
+#endif /* CVC4__EXPR__LAZY_PROOF_CHAIN_H */
diff --git a/src/expr/proof_node_algorithm.cpp b/src/expr/proof_node_algorithm.cpp
index 9e1018024..984379d54 100644
--- a/src/expr/proof_node_algorithm.cpp
+++ b/src/expr/proof_node_algorithm.cpp
@@ -19,22 +19,26 @@ namespace expr {
 
 void getFreeAssumptions(ProofNode* pn, std::vector<Node>& assump)
 {
-  std::map<Node, std::vector<ProofNode*>> amap;
-  getFreeAssumptionsMap(pn, amap);
-  for (const std::pair<const Node, std::vector<ProofNode*>>& p : amap)
+  std::map<Node, std::vector<std::shared_ptr<ProofNode>>> amap;
+  std::shared_ptr<ProofNode> spn = std::make_shared<ProofNode>(
+      pn->getRule(), pn->getChildren(), pn->getArguments());
+  getFreeAssumptionsMap(spn, amap);
+  for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>& p :
+       amap)
   {
     assump.push_back(p.first);
   }
 }
 
-void getFreeAssumptionsMap(ProofNode* pn,
-                           std::map<Node, std::vector<ProofNode*>>& amap)
+void getFreeAssumptionsMap(
+    std::shared_ptr<ProofNode> pn,
+    std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& amap)
 {
   // proof should not be cyclic
   // visited set false after preorder traversal, true after postorder traversal
   std::unordered_map<ProofNode*, bool> visited;
   std::unordered_map<ProofNode*, bool>::iterator it;
-  std::vector<ProofNode*> visit;
+  std::vector<std::shared_ptr<ProofNode>> visit;
   // Maps a bound assumption to the number of bindings it is under
   // e.g. in (SCOPE (SCOPE (ASSUME x) (x y)) (y)), y would be mapped to 2 at
   // (ASSUME x), and x would be mapped to 1.
@@ -54,17 +58,17 @@ void getFreeAssumptionsMap(ProofNode* pn,
   //   after postvisiting SCOPE2: {}
   //
   std::unordered_map<Node, uint32_t, NodeHashFunction> scopeDepth;
-  ProofNode* cur;
+  std::shared_ptr<ProofNode> cur;
   visit.push_back(pn);
   do
   {
     cur = visit.back();
     visit.pop_back();
-    it = visited.find(cur);
+    it = visited.find(cur.get());
     const std::vector<Node>& cargs = cur->getArguments();
     if (it == visited.end())
     {
-      visited[cur] = true;
+      visited[cur.get()] = true;
       PfRule id = cur->getRule();
       if (id == PfRule::ASSUME)
       {
@@ -85,7 +89,7 @@ void getFreeAssumptionsMap(ProofNode* pn,
             scopeDepth[a] += 1;
           }
           // will need to unbind the variables below
-          visited[cur] = false;
+          visited[cur.get()] = false;
           visit.push_back(cur);
         }
         // The following loop cannot be merged with the loop above because the
@@ -93,13 +97,13 @@ void getFreeAssumptionsMap(ProofNode* pn,
         const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
         for (const std::shared_ptr<ProofNode>& cp : cs)
         {
-          visit.push_back(cp.get());
+          visit.push_back(cp);
         }
       }
     }
     else if (!it->second)
     {
-      visited[cur] = true;
+      visited[cur.get()] = true;
       Assert(cur->getRule() == PfRule::SCOPE);
       // unbind its assumptions
       for (const Node& a : cargs)
diff --git a/src/expr/proof_node_algorithm.h b/src/expr/proof_node_algorithm.h
index bc44d7314..aec098e17 100644
--- a/src/expr/proof_node_algorithm.h
+++ b/src/expr/proof_node_algorithm.h
@@ -49,8 +49,9 @@ void getFreeAssumptions(ProofNode* pn, std::vector<Node>& assump);
  * @param amap The mapping to add the free asumptions of pn and their
  * corresponding proof nodes to.
  */
-void getFreeAssumptionsMap(ProofNode* pn,
-                           std::map<Node, std::vector<ProofNode*>>& amap);
+void getFreeAssumptionsMap(
+    std::shared_ptr<ProofNode> pn,
+    std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& amap);
 
 }  // namespace expr
 }  // namespace CVC4
diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp
index 0d13531a5..54315ee05 100644
--- a/src/expr/proof_node_manager.cpp
+++ b/src/expr/proof_node_manager.cpp
@@ -75,10 +75,11 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
   bool computedAcr = false;
 
   // The free assumptions of the proof
-  std::map<Node, std::vector<ProofNode*>> famap;
-  expr::getFreeAssumptionsMap(pf.get(), famap);
+  std::map<Node, std::vector<std::shared_ptr<ProofNode>>> famap;
+  expr::getFreeAssumptionsMap(pf, famap);
   std::unordered_set<Node, NodeHashFunction> acu;
-  for (const std::pair<const Node, std::vector<ProofNode*>>& fa : famap)
+  for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>&
+           fa : famap)
   {
     Node a = fa.first;
     if (ac.find(a) != ac.end())
@@ -135,10 +136,10 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
       children.push_back(pfaa);
       std::vector<Node> args;
       args.push_back(a);
-      for (ProofNode* pfs : fa.second)
+      for (std::shared_ptr<ProofNode> pfs : fa.second)
       {
         Assert(pfs->getResult() == a);
-        updateNode(pfs, PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
+        updateNode(pfs.get(), PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
       }
       Trace("pnm-scope") << "...finished" << std::endl;
       acu.insert(aMatch);
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index 1d46b183f..57dd3e0bd 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -42,6 +42,10 @@ const char* toString(PfRule id)
     case PfRule::THEORY_PREPROCESS_LEMMA: return "THEORY_PREPROCESS_LEMMA";
     case PfRule::WITNESS_AXIOM: return "WITNESS_AXIOM";
     //================================================= Boolean rules
+    case PfRule::RESOLUTION: return "RESOLUTION";
+    case PfRule::CHAIN_RESOLUTION: return "CHAIN_RESOLUTION";
+    case PfRule::FACTORING: return "FACTORING";
+    case PfRule::REORDERING: return "REORDERING";
     case PfRule::SPLIT: return "SPLIT";
     case PfRule::EQ_RESOLVE: return "EQ_RESOLVE";
     case PfRule::AND_ELIM: return "AND_ELIM";
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 825503d5d..c02292dab 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -226,6 +226,45 @@ enum class PfRule : uint32_t
   WITNESS_AXIOM,
 
   //================================================= Boolean rules
+  // ======== Resolution
+  // Children:
+  //  (P1:(or F_1 ... F_i-1 F_i F_i+1 ... F_n),
+  //   P2:(or G_1 ... G_j-1 G_j G_j+1 ... G_m))
+  //
+  // Arguments: (F_i)
+  // ---------------------
+  // Conclusion: (or F_1 ... F_i-1 F_i+1 ... F_n G_1 ... G_j-1 G_j+1 ... G_m)
+  // where
+  //   G_j = (not F_i)
+  RESOLUTION,
+  // ======== Chain Resolution
+  // Children: (P1:(or F_{1,1} ... F_{1,n1}), ..., Pm:(or F_{m,1} ... F_{m,nm}))
+  // Arguments: (L_1, ..., L_{m-1})
+  // ---------------------
+  // Conclusion: C_m'
+  // where
+  //   let "C_1 <>_l C_2" represent the resolution of C_1 with C_2 with pivot l,
+  //   let C_1' = C_1 (from P_1),
+  //   for each i > 1, C_i' = C_i <>_L_i C_{i-1}'
+  CHAIN_RESOLUTION,
+  // ======== Factoring
+  // Children: (P:C1)
+  // Arguments: ()
+  // ---------------------
+  // Conclusion: C2
+  // where
+  //  Set representations of C1 and C2 is the same and the number of literals in
+  //  C2 is smaller than that of C1
+  FACTORING,
+  // ======== Reordering
+  // Children: (P:C1)
+  // Arguments: (C2)
+  // ---------------------
+  // Conclusion: C2
+  // where
+  //  Set representations of C1 and C2 is the same but the number of literals in
+  //  C2 is the same of that of C1
+  REORDERING,
   // ======== Split
   // Children: none
   // Arguments: (F)
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/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index e40b828b5..13ad086e8 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -687,11 +687,7 @@ Node BVToInt::translateNoChildren(Node original)
         uint64_t bvsize = original.getType().getBitVectorSize();
         translation = newVar;
         d_rangeAssertions.insert(mkRangeConstraint(newVar, bvsize));
-        std::vector<Expr> args;
-        Node intToBVOp = d_nm->mkConst<IntToBitVector>(IntToBitVector(bvsize));
-        Node newNode = d_nm->mkNode(intToBVOp, newVar);
-        smt::currentSmtEngine()->defineFunction(
-            original.toExpr(), args, newNode.toExpr(), true);
+        defineBVUFAsIntUF(original, newVar);
     }
     else if (original.getType().isFunction())
     {
@@ -756,41 +752,49 @@ Node BVToInt::translateFunctionSymbol(Node bvUF)
 
 void BVToInt::defineBVUFAsIntUF(Node bvUF, Node intUF)
 {
-  // This function should only be called after translating
-  // the function symbol to a new function symbol
-  // with the right domain and range.
-
-  // get domain and range of the original function
-  TypeNode tn = bvUF.getType();
-  vector<TypeNode> bvDomain = tn.getArgTypes();
-  TypeNode bvRange = tn.getRangeType();
-
+  // The resulting term
+  Node result;
+  // The type of the resulting term
+  TypeNode resultType;
   // symbolic arguments of original function
   vector<Expr> args;
-  // children of the new symbolic application
-  vector<Node> achildren;
-  achildren.push_back(intUF);
-  int i = 0;
-  for (TypeNode d : bvDomain)
-  {
-    // Each bit-vector argument is casted to a natural number
-    // Other arguments are left intact.
-    Node fresh_bound_var = d_nm->mkBoundVar(d);
-    args.push_back(fresh_bound_var.toExpr());
-    Node castedArg = args[i];
-    if (d.isBitVector())
+  if (!bvUF.getType().isFunction()) {
+    // bvUF is a variable.
+    // in this case, the result is just the original term
+    // (it will be casted later if needed)
+    result = intUF;
+    resultType = bvUF.getType();
+  } else {
+    // bvUF is a function with arguments
+    // The arguments need to be casted as well.
+    TypeNode tn = bvUF.getType();
+    resultType = tn.getRangeType();
+    vector<TypeNode> bvDomain = tn.getArgTypes();
+    // children of the new symbolic application
+    vector<Node> achildren;
+    achildren.push_back(intUF);
+    int i = 0;
+    for (const TypeNode& d : bvDomain)
     {
-      castedArg = castToType(castedArg, d_nm->integerType());
+      // Each bit-vector argument is casted to a natural number
+      // Other arguments are left intact.
+      Node fresh_bound_var = d_nm->mkBoundVar(d);
+      args.push_back(fresh_bound_var.toExpr());
+      Node castedArg = args[i];
+      if (d.isBitVector())
+      {
+        castedArg = castToType(castedArg, d_nm->integerType());
+      }
+      achildren.push_back(castedArg);
+      i++;
     }
-    achildren.push_back(castedArg);
-    i++;
+    result = d_nm->mkNode(kind::APPLY_UF, achildren);
   }
-  Node intApplication = d_nm->mkNode(kind::APPLY_UF, achildren);
-  // If the range is BV, the application needs to be casted back.
-  intApplication = castToType(intApplication, bvRange);
+  // If the result is BV, it needs to be casted back.
+  result = castToType(result, resultType);
   // add the function definition to the smt engine.
   smt::currentSmtEngine()->defineFunction(
-      bvUF.toExpr(), args, intApplication.toExpr(), true);
+      bvUF.toExpr(), args, result.toExpr(), true);
 }
 
 bool BVToInt::childrenTypesChanged(Node n)
diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h
index db2d08b7d..b84726878 100644
--- a/src/preprocessing/passes/bv_to_int.h
+++ b/src/preprocessing/passes/bv_to_int.h
@@ -289,11 +289,12 @@ class BVToInt : public PreprocessingPass
    * When a UF f is translated to a UF g,
    * we add a define-fun command to the smt-engine
    * to relate between f and g.
+   * We do the same when f and g are just variables.
    * This is useful, for example, when asking
    * for a model-value of a term that includes the
    * original UF f.
-   * @param bvUF the original function
-   * @param intUF the translated function
+   * @param bvUF the original function or variable
+   * @param intUF the translated function or variable
    */
   void defineBVUFAsIntUF(Node bvUF, Node intUF);
 
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/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 1436198a8..4884d8484 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -21,6 +21,7 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/arith_rewriter.h"
 #include "theory/arith/infer_bounds.h"
+#include "theory/arith/nl/nonlinear_extension.h"
 #include "theory/arith/theory_arith_private.h"
 #include "theory/ext_theory.h"
 
@@ -42,7 +43,8 @@ TheoryArith::TheoryArith(context::Context* c,
           new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo, pnm)),
       d_ppRewriteTimer("theory::arith::ppRewriteTimer"),
       d_astate(*d_internal, c, u, valuation),
-      d_inferenceManager(*this, d_astate, pnm)
+      d_inferenceManager(*this, d_astate, pnm),
+      d_nonlinearExtension(nullptr)
 {
   smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer);
 
@@ -76,6 +78,13 @@ void TheoryArith::finishInit()
     d_valuation.setUnevaluatedKind(kind::SINE);
     d_valuation.setUnevaluatedKind(kind::PI);
   }
+  // only need to create nonlinear extension if non-linear logic
+  const LogicInfo& logicInfo = getLogicInfo();
+  if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear())
+  {
+    d_nonlinearExtension.reset(
+        new nl::NonlinearExtension(*this, d_equalityEngine));
+  }
   // finish initialize internally
   d_internal->finishInit();
 }
@@ -123,7 +132,53 @@ void TheoryArith::propagate(Effort e) {
 }
 bool TheoryArith::collectModelInfo(TheoryModel* m)
 {
-  return d_internal->collectModelInfo(m);
+  std::set<Node> termSet;
+  // Work out which variables are needed
+  const std::set<Kind>& irrKinds = m->getIrrelevantKinds();
+  computeAssertedTerms(termSet, irrKinds);
+  // this overrides behavior to not assert equality engine
+  return collectModelValues(m, termSet);
+}
+
+bool TheoryArith::collectModelValues(TheoryModel* m,
+                                     const std::set<Node>& termSet)
+{
+  // get the model from the linear solver
+  std::map<Node, Node> arithModel;
+  d_internal->collectModelValues(termSet, arithModel);
+  // if non-linear is enabled, intercept the model, which may repair its values
+  if (d_nonlinearExtension != nullptr)
+  {
+    // Non-linear may repair values to satisfy non-linear constraints (see
+    // documentation for NonlinearExtension::interceptModel).
+    d_nonlinearExtension->interceptModel(arithModel);
+  }
+  // We are now ready to assert the model.
+  for (const std::pair<const Node, Node>& p : arithModel)
+  {
+    // maps to constant of comparable type
+    Assert(p.first.getType().isComparableTo(p.second.getType()));
+    Assert(p.second.isConst());
+    if (m->assertEquality(p.first, p.second, true))
+    {
+      continue;
+    }
+    // If we failed to assert an equality, it is likely due to theory
+    // combination, namely the repaired model for non-linear changed
+    // an equality status that was agreed upon by both (linear) arithmetic
+    // and another theory. In this case, we must add a lemma, or otherwise
+    // we would terminate with an invalid model. Thus, we add a splitting
+    // lemma of the form ( x = v V x != v ) where v is the model value
+    // assigned by the non-linear solver to x.
+    if (d_nonlinearExtension != nullptr)
+    {
+      Node eq = p.first.eqNode(p.second);
+      Node lem = NodeManager::currentNM()->mkNode(kind::OR, eq, eq.negate());
+      d_out->lemma(lem);
+    }
+    return false;
+  }
+  return true;
 }
 
 void TheoryArith::notifyRestart(){
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 4851f1c5d..30ad724cc 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -25,12 +25,15 @@
 
 namespace CVC4 {
 namespace theory {
-
 namespace arith {
 
+namespace nl {
+class NonlinearExtension;
+}
+
 /**
- * Implementation of QF_LRA.
- * Based upon:
+ * Implementation of linear and non-linear integer and real arithmetic.
+ * The linear arithmetic solver is based upon:
  * http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf
  */
 class TheoryArith : public Theory {
@@ -78,6 +81,11 @@ class TheoryArith : public Theory {
   TrustNode explain(TNode n) override;
 
   bool collectModelInfo(TheoryModel* m) override;
+  /**
+   * Collect model values in m based on the relevant terms given by termSet.
+   */
+  bool collectModelValues(TheoryModel* m,
+                          const std::set<Node>& termSet) override;
 
   void shutdown() override {}
 
@@ -110,6 +118,11 @@ class TheoryArith : public Theory {
   /** The arith::InferenceManager. */
   InferenceManager d_inferenceManager;
 
+  /**
+   * The non-linear extension, responsible for all approaches for non-linear
+   * arithmetic.
+   */
+  std::unique_ptr<nl::NonlinearExtension> d_nonlinearExtension;
 };/* class TheoryArith */
 
 }/* CVC4::theory::arith namespace */
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 1b49b7350..8595e26b5 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -164,7 +164,6 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
 TheoryArithPrivate::~TheoryArithPrivate(){
   if(d_treeLog != NULL){ delete d_treeLog; }
   if(d_approxStats != NULL) { delete d_approxStats; }
-  if(d_nonlinearExtension != NULL) { delete d_nonlinearExtension; }
 }
 
 TheoryRewriter* TheoryArithPrivate::getTheoryRewriter() { return &d_rewriter; }
@@ -177,12 +176,7 @@ void TheoryArithPrivate::finishInit()
   eq::EqualityEngine* ee = d_containing.getEqualityEngine();
   Assert(ee != nullptr);
   d_congruenceManager.finishInit(ee);
-  const LogicInfo& logicInfo = getLogicInfo();
-  // only need to create nonlinear extension if non-linear logic
-  if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear())
-  {
-    d_nonlinearExtension = new nl::NonlinearExtension(d_containing, ee);
-  }
+  d_nonlinearExtension = d_containing.d_nonlinearExtension.get();
 }
 
 static bool contains(const ConstraintCPVec& v, ConstraintP con){
@@ -4074,7 +4068,8 @@ Rational TheoryArithPrivate::deltaValueForTotalOrder() const{
   return belowMin;
 }
 
-bool TheoryArithPrivate::collectModelInfo(TheoryModel* m)
+void TheoryArithPrivate::collectModelValues(const std::set<Node>& termSet,
+                                            std::map<Node, Node>& arithModel)
 {
   AlwaysAssert(d_qflraStatus == Result::SAT);
   //AlwaysAssert(!d_nlIncomplete, "Arithmetic solver cannot currently produce models for input with nonlinear arithmetic constraints");
@@ -4085,10 +4080,6 @@ bool TheoryArithPrivate::collectModelInfo(TheoryModel* m)
 
   Debug("arith::collectModelInfo") << "collectModelInfo() begin " << endl;
 
-  std::set<Node> termSet;
-  const std::set<Kind>& irrKinds = m->getIrrelevantKinds();
-  d_containing.computeAssertedTerms(termSet, irrKinds, true);
-
   // Delta lasts at least the duration of the function call
   const Rational& delta = d_partialModel.getDelta();
   std::unordered_set<TNode, TNodeHashFunction> shared = d_containing.currentlySharedTerms();
@@ -4096,8 +4087,6 @@ bool TheoryArithPrivate::collectModelInfo(TheoryModel* m)
   // TODO:
   // This is not very good for user push/pop....
   // Revisit when implementing push/pop
-  // Map of terms to values, constructed when non-linear arithmetic is active.
-  std::map<Node, Node> arithModel;
   for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){
     ArithVar v = *vi;
 
@@ -4112,56 +4101,20 @@ bool TheoryArithPrivate::collectModelInfo(TheoryModel* m)
 
         Node qNode = mkRationalNode(qmodel);
         Debug("arith::collectModelInfo") << "m->assertEquality(" << term << ", " << qmodel << ", true)" << endl;
-        if (d_nonlinearExtension != nullptr)
-        {
-          // Let non-linear extension inspect the values before they are sent
-          // to the theory model.
-          arithModel[term] = qNode;
-        }
-        else
-        {
-          if (!m->assertEquality(term, qNode, true))
-          {
-            return false;
-          }
-        }
+        // Add to the map
+        arithModel[term] = qNode;
       }else{
         Debug("arith::collectModelInfo") << "Skipping m->assertEquality(" << term << ", true)" << endl;
 
       }
     }
   }
-  if (d_nonlinearExtension != nullptr)
-  {
-    // Non-linear may repair values to satisfy non-linear constraints (see
-    // documentation for NonlinearExtension::interceptModel).
-    d_nonlinearExtension->interceptModel(arithModel);
-    // We are now ready to assert the model.
-    for (std::pair<const Node, Node>& p : arithModel)
-    {
-      if (!m->assertEquality(p.first, p.second, true))
-      {
-        // If we failed to assert an equality, it is likely due to theory
-        // combination, namely the repaired model for non-linear changed
-        // an equality status that was agreed upon by both (linear) arithmetic
-        // and another theory. In this case, we must add a lemma, or otherwise
-        // we would terminate with an invalid model. Thus, we add a splitting
-        // lemma of the form ( x = v V x != v ) where v is the model value
-        // assigned by the non-linear solver to x.
-        Node eq = p.first.eqNode(p.second);
-        Node lem = NodeManager::currentNM()->mkNode(kind::OR, eq, eq.negate());
-        d_containing.d_out->lemma(lem);
-        return false;
-      }
-    }
-  }
 
   // Iterate over equivalence classes in LinearEqualityModule
   // const eq::EqualityEngine& ee = d_congruenceManager.getEqualityEngine();
   // m->assertEqualityEngine(&ee);
 
   Debug("arith::collectModelInfo") << "collectModelInfo() end " << endl;
-  return true;
 }
 
 bool TheoryArithPrivate::safeToReset() const {
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index d0428f2ef..6d030dece 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -371,7 +371,7 @@ public:
   FCSimplexDecisionProcedure d_fcSimplex;
   SumOfInfeasibilitiesSPD d_soiSimplex;
   AttemptSolutionSDP d_attemptSolSimplex;
-  
+
   /** non-linear algebraic approach */
   nl::NonlinearExtension* d_nonlinearExtension;
 
@@ -456,6 +456,18 @@ public:
   Rational deltaValueForTotalOrder() const;
 
   bool collectModelInfo(TheoryModel* m);
+  /**
+   * Collect model values. This is the main method for extracting information
+   * about how to construct the model. This method relies on the caller for
+   * processing the map, which is done so that other modules (e.g. the
+   * non-linear extension) can modify arithModel before it is sent to the model.
+   *
+   * @param termSet The set of relevant terms
+   * @param arithModel Mapping from terms (of real type) to their values. The
+   * caller should assert equalities to the model for each entry in this map.
+   */
+  void collectModelValues(const std::set<Node>& termSet,
+                          std::map<Node, Node>& arithModel);
 
   void shutdown(){ }
 
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/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp
index 6a8244ce0..e9dafdad6 100644
--- a/src/theory/booleans/proof_checker.cpp
+++ b/src/theory/booleans/proof_checker.cpp
@@ -21,6 +21,10 @@ namespace booleans {
 void BoolProofRuleChecker::registerTo(ProofChecker* pc)
 {
   pc->registerChecker(PfRule::SPLIT, this);
+  pc->registerChecker(PfRule::RESOLUTION, this);
+  pc->registerChecker(PfRule::CHAIN_RESOLUTION, this);
+  pc->registerChecker(PfRule::FACTORING, this);
+  pc->registerChecker(PfRule::REORDERING, this);
   pc->registerChecker(PfRule::EQ_RESOLVE, this);
   pc->registerChecker(PfRule::AND_ELIM, this);
   pc->registerChecker(PfRule::AND_INTRO, this);
@@ -68,6 +72,139 @@ Node BoolProofRuleChecker::checkInternal(PfRule id,
                                          const std::vector<Node>& children,
                                          const std::vector<Node>& args)
 {
+  if (id == PfRule::RESOLUTION)
+  {
+    Assert(children.size() == 2);
+    Assert(args.size() == 1);
+    std::vector<Node> disjuncts;
+    for (unsigned i = 0; i < 2; ++i)
+    {
+      // if first clause, eliminate pivot, otherwise its negation
+      Node elim = i == 0 ? args[0] : args[0].notNode();
+      for (unsigned j = 0, size = children[i].getNumChildren(); j < size; ++j)
+      {
+        if (elim != children[i][j])
+        {
+          disjuncts.push_back(children[i][j]);
+        }
+      }
+    }
+    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
+  }
+  if (id == PfRule::FACTORING)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    if (children[0].getKind() != kind::OR)
+    {
+      return Node::null();
+    }
+    // remove duplicates while keeping the order of children
+    std::unordered_set<TNode, TNodeHashFunction> clauseSet;
+    std::vector<Node> disjuncts;
+    unsigned size = children[0].getNumChildren();
+    for (unsigned i = 0; i < size; ++i)
+    {
+      if (clauseSet.count(children[0][i]))
+      {
+        continue;
+      }
+      disjuncts.push_back(children[0][i]);
+      clauseSet.insert(children[0][i]);
+    }
+    if (disjuncts.size() == size)
+    {
+      return Node::null();
+    }
+    NodeManager* nm = NodeManager::currentNM();
+    return disjuncts.empty()
+               ? nm->mkConst<bool>(false)
+               : disjuncts.size() == 1 ? disjuncts[0]
+                                       : nm->mkNode(kind::OR, disjuncts);
+  }
+  if (id == PfRule::REORDERING)
+  {
+    Assert(children.size() == 1);
+    Assert(args.size() == 1);
+    std::unordered_set<Node, NodeHashFunction> clauseSet1, clauseSet2;
+    if (children[0].getKind() == kind::OR)
+    {
+      clauseSet1.insert(children[0].begin(), children[0].end());
+    }
+    else
+    {
+      clauseSet1.insert(children[0]);
+    }
+    if (args[0].getKind() == kind::OR)
+    {
+      clauseSet2.insert(args[0].begin(), args[0].end());
+    }
+    else
+    {
+      clauseSet2.insert(args[0]);
+    }
+    if (clauseSet1 != clauseSet2)
+    {
+      Trace("bool-pfcheck") << id << ": clause set1: " << clauseSet1 << "\n"
+                            << id << ": clause set2: " << clauseSet2 << "\n";
+      return Node::null();
+    }
+    return args[0];
+  }
+  if (id == PfRule::CHAIN_RESOLUTION)
+  {
+    Assert(children.size() > 1);
+    Assert(args.size() == children.size() - 1);
+    Trace("bool-pfcheck") << "chain_res:\n" << push;
+    std::vector<Node> clauseNodes;
+    for (unsigned i = 0, childrenSize = children.size(); i < childrenSize; ++i)
+    {
+      std::unordered_set<Node, NodeHashFunction> elim;
+      // literals to be removed from "first" clause
+      if (i < childrenSize - 1)
+      {
+        elim.insert(args.begin() + i, args.end());
+      }
+      // literal to be removed from "second" clause. They will be negated
+      if (i > 0)
+      {
+        elim.insert(args[i - 1].negate());
+      }
+      Trace("bool-pfcheck") << i << ": elimination set: " << elim << "\n";
+      // only add to conclusion nodes that are not in elimination set. First get
+      // the nodes.
+      //
+      // Since unit clauses can also be OR nodes, we rely on the invariant that
+      // non-unit clauses will not occur themselves in their elimination sets.
+      // If they do then they must be unit.
+      std::vector<Node> lits;
+      if (children[i].getKind() == kind::OR && elim.count(children[i]) == 0)
+      {
+        lits.insert(lits.end(), children[i].begin(), children[i].end());
+      }
+      else
+      {
+        lits.push_back(children[i]);
+      }
+      Trace("bool-pfcheck") << i << ": clause lits: " << lits << "\n";
+      std::vector<Node> added;
+      for (unsigned j = 0, size = lits.size(); j < size; ++j)
+      {
+        if (elim.count(lits[j]) == 0)
+        {
+          clauseNodes.push_back(lits[j]);
+          added.push_back(lits[j]);
+        }
+      }
+      Trace("bool-pfcheck") << i << ": added lits: " << added << "\n\n";
+    }
+    Trace("bool-pfcheck") << "clause: " << clauseNodes << "\n" << pop;
+    NodeManager* nm = NodeManager::currentNM();
+    return clauseNodes.empty()
+               ? nm->mkConst<bool>(false)
+               : clauseNodes.size() == 1 ? clauseNodes[0]
+                                         : nm->mkNode(kind::OR, clauseNodes);
+  }
   if (id == PfRule::SPLIT)
   {
     Assert(children.empty());
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/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 573449287..b9b7b6061 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -50,10 +50,9 @@ TheorySep::TheorySep(context::Context* c,
       d_lemmas_produced_c(u),
       d_bounds_init(false),
       d_state(c, u, valuation),
+      d_im(*this, d_state, pnm),
       d_notify(*this),
       d_reduce(u),
-      d_infer(c),
-      d_infer_exp(c),
       d_spatial_assertions(c)
 {
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
@@ -61,6 +60,7 @@ TheorySep::TheorySep(context::Context* c,
 
   // indicate we are using the default theory state object
   d_theoryState = &d_state;
+  d_inferManager = &d_im;
 }
 
 TheorySep::~TheorySep() {
@@ -128,31 +128,10 @@ bool TheorySep::propagateLit(TNode literal)
   return ok;
 }
 
-void TheorySep::explain(TNode literal, std::vector<TNode>& assumptions) {
-  if( literal.getKind()==kind::SEP_LABEL ||
-      ( literal.getKind()==kind::NOT && literal[0].getKind()==kind::SEP_LABEL ) ){
-    //labelled assertions are never given to equality engine and should only come from the outside
-    assumptions.push_back( literal );
-  }else{
-    // Do the work
-    bool polarity = literal.getKind() != kind::NOT;
-    TNode atom = polarity ? literal : literal[0];
-    if (atom.getKind() == kind::EQUAL) {
-      d_equalityEngine->explainEquality(
-          atom[0], atom[1], polarity, assumptions, NULL);
-    } else {
-      d_equalityEngine->explainPredicate(atom, polarity, assumptions);
-    }
-  }
-}
-
 TrustNode TheorySep::explain(TNode literal)
 {
   Debug("sep") << "TheorySep::explain(" << literal << ")" << std::endl;
-  std::vector<TNode> assumptions;
-  explain(literal, assumptions);
-  Node exp = mkAnd(assumptions);
-  return TrustNode::mkTrustPropExp(literal, exp, nullptr);
+  return d_im.explainLit(literal);
 }
 
 
@@ -298,7 +277,7 @@ bool TheorySep::preNotifyFact(
     return false;
   }
   // otherwise, maybe propagate
-  doPendingFacts();
+  doPending();
   return true;
 }
 
@@ -316,7 +295,7 @@ void TheorySep::notifyFact(TNode atom,
     addPto(ei, r, atom, polarity);
   }
   // maybe propagate
-  doPendingFacts();
+  doPending();
 }
 
 void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact)
@@ -943,12 +922,7 @@ bool TheorySep::needsCheckLastEffort() {
 
 void TheorySep::conflict(TNode a, TNode b) {
   Trace("sep-conflict") << "Sep::conflict : " << a << " " << b << std::endl;
-  Node eq = a.eqNode(b);
-  std::vector<TNode> assumptions;
-  explain(eq, assumptions);
-  Node conflictNode = mkAnd(assumptions);
-  d_state.notifyInConflict();
-  d_out->conflict( conflictNode );
+  d_im.conflictEqConstantMerge(a, b);
 }
 
 
@@ -1825,81 +1799,29 @@ void TheorySep::sendLemma( std::vector< Node >& ant, Node conc, const char * c,
   Trace("sep-lemma-debug") << "Got : " << conc << std::endl;
   if( conc!=d_true ){
     if( infer && conc!=d_false ){
-      Node ant_n;
-      if( ant.empty() ){
-        ant_n = d_true;
-      }else if( ant.size()==1 ){
-        ant_n = ant[0];
-      }else{
-        ant_n = NodeManager::currentNM()->mkNode( kind::AND, ant );
-      }
+      Node ant_n = NodeManager::currentNM()->mkAnd(ant);
       Trace("sep-lemma") << "Sep::Infer: " << conc << " from " << ant_n << " by " << c << std::endl;
-      d_pending_exp.push_back( ant_n );
-      d_pending.push_back( conc );
-      d_infer.push_back( ant_n );
-      d_infer_exp.push_back( conc );
+      d_im.addPendingFact(conc, ant_n);
     }else{
-      std::vector< TNode > ant_e;
-      for( unsigned i=0; i<ant.size(); i++ ){
-        Trace("sep-lemma-debug") << "Explain : " << ant[i] << std::endl;
-        explain( ant[i], ant_e );
-      }
-      Node ant_n;
-      if( ant_e.empty() ){
-        ant_n = d_true;
-      }else if( ant_e.size()==1 ){
-        ant_n = ant_e[0];
-      }else{
-        ant_n = NodeManager::currentNM()->mkNode( kind::AND, ant_e );
-      }
       if( conc==d_false ){
-        Trace("sep-lemma") << "Sep::Conflict: " << ant_n << " by " << c << std::endl;
-        d_out->conflict( ant_n );
-        d_state.notifyInConflict();
+        Trace("sep-lemma") << "Sep::Conflict: " << ant << " by " << c
+                           << std::endl;
+        d_im.conflictExp(ant, nullptr);
       }else{
-        Trace("sep-lemma") << "Sep::Lemma: " << conc << " from " << ant_n << " by " << c << std::endl;
-        d_pending_exp.push_back( ant_n );
-        d_pending.push_back( conc );
-        d_pending_lem.push_back( d_pending.size()-1 );
+        Trace("sep-lemma") << "Sep::Lemma: " << conc << " from " << ant
+                           << " by " << c << std::endl;
+        TrustNode trn = d_im.mkLemmaExp(conc, ant, {});
+        d_im.addPendingLemma(
+            trn.getNode(), LemmaProperty::NONE, trn.getGenerator());
       }
     }
   }
 }
 
-void TheorySep::doPendingFacts() {
-  if( d_pending_lem.empty() ){
-    for( unsigned i=0; i<d_pending.size(); i++ ){
-      if (d_state.isInConflict())
-      {
-        break;
-      }
-      Node atom = d_pending[i].getKind()==kind::NOT ? d_pending[i][0] : d_pending[i];
-      bool pol = d_pending[i].getKind()!=kind::NOT;
-      Trace("sep-pending") << "Sep : Assert to EE : " << atom << ", pol = " << pol << std::endl;
-      if( atom.getKind()==kind::EQUAL ){
-        d_equalityEngine->assertEquality(atom, pol, d_pending_exp[i]);
-      }else{
-        d_equalityEngine->assertPredicate(atom, pol, d_pending_exp[i]);
-      }
-    }
-  }else{
-    for( unsigned i=0; i<d_pending_lem.size(); i++ ){
-      if (d_state.isInConflict())
-      {
-        break;
-      }
-      int index = d_pending_lem[i];
-      Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, d_pending_exp[index], d_pending[index] );
-      if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){
-        d_lemmas_produced_c.insert( lem );
-        d_out->lemma( lem );
-        Trace("sep-pending") << "Sep : Lemma : " << lem << std::endl;
-      }
-    }
-  }
-  d_pending_exp.clear();
-  d_pending.clear();
-  d_pending_lem.clear();
+void TheorySep::doPending()
+{
+  d_im.doPendingFacts();
+  d_im.doPendingLemmas();
 }
 
 void TheorySep::debugPrintHeap( HeapInfo& heap, const char * c ) {
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 6bef1b37e..8eb9927f0 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -23,6 +23,7 @@
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
 #include "context/cdqueue.h"
+#include "theory/inference_manager_buffered.h"
 #include "theory/sep/theory_sep_rewriter.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
@@ -60,6 +61,8 @@ class TheorySep : public Theory {
   TheorySepRewriter d_rewriter;
   /** A (default) theory state object */
   TheoryState d_state;
+  /** A buffered inference manager */
+  InferenceManagerBuffered d_im;
 
   Node mkAnd( std::vector< TNode >& assumptions );
 
@@ -108,8 +111,6 @@ class TheorySep : public Theory {
   bool propagateLit(TNode literal);
   /** Conflict when merging constants */
   void conflict(TNode a, TNode b);
-  /** Explain why this literal is true by adding assumptions */
-  void explain(TNode literal, std::vector<TNode>& assumptions);
 
  public:
   TrustNode explain(TNode n) override;
@@ -213,11 +214,6 @@ class TheorySep : public Theory {
   /** The notify class for d_equalityEngine */
   NotifyClass d_notify;
 
-  /** Are we in conflict? */
-  std::vector< Node > d_pending_exp;
-  std::vector< Node > d_pending;
-  std::vector< int > d_pending_lem;
-
   /** list of all refinement lemms */
   std::map< Node, std::map< Node, std::vector< Node > > > d_refinement_lem;
 
@@ -230,9 +226,6 @@ class TheorySep : public Theory {
   std::map<Node, std::unique_ptr<DecisionStrategySingleton> >
       d_neg_guard_strategy;
   std::map< Node, Node > d_guard_to_assertion;
-  /** inferences: maintained to ensure ref count for internally introduced nodes */
-  NodeList d_infer;
-  NodeList d_infer_exp;
   NodeList d_spatial_assertions;
 
   //data,ref type (globally fixed)
@@ -327,7 +320,7 @@ class TheorySep : public Theory {
   void eqNotifyMerge(TNode t1, TNode t2);
 
   void sendLemma( std::vector< Node >& ant, Node conc, const char * c, bool infer = false );
-  void doPendingFacts();
+  void doPending();
 
  public:
 
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/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp
index d7b615ffa..8b1e05fb0 100644
--- a/src/theory/uf/eq_proof.cpp
+++ b/src/theory/uf/eq_proof.cpp
@@ -16,6 +16,7 @@
 #include "theory/uf/eq_proof.h"
 
 #include "expr/proof.h"
+#include "options/uf_options.h"
 
 namespace CVC4 {
 namespace theory {
@@ -700,9 +701,10 @@ void EqProof::reduceNestedCongruence(
         << transitivityMatrix[i].back() << "\n";
     // if i == 0, first child must be REFL step, standing for (= f f), which can
     // be ignored in a first-order calculus
-    Assert(i > 0 || d_children[0]->d_id == MERGED_THROUGH_REFLEXIVITY);
+    Assert(i > 0 || d_children[0]->d_id == MERGED_THROUGH_REFLEXIVITY
+           || options::ufHo());
     // recurse
-    if (i > 0)
+    if (i > 1)
     {
       Trace("eqproof-conv")
           << "EqProof::reduceNestedCongruence: Reduce first child\n"
@@ -716,9 +718,21 @@ void EqProof::reduceNestedCongruence(
                                             isNary);
       Trace("eqproof-conv") << pop;
     }
+    // higher-order case
+    else if (d_children[0]->d_id != MERGED_THROUGH_REFLEXIVITY)
+    {
+      Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: HO case. "
+                               "Processing first child\n";
+      // we only handle these cases
+      Assert(d_children[0]->d_id == MERGED_THROUGH_EQUALITY
+             || d_children[0]->d_id == MERGED_THROUGH_TRANS);
+      transitivityMatrix[0].push_back(
+          d_children[0]->addToProof(p, visited, assumptions));
+    }
     return;
   }
-  Assert(d_id == MERGED_THROUGH_TRANS);
+  Assert(d_id == MERGED_THROUGH_TRANS)
+      << "id is " << static_cast<MergeReasonType>(d_id) << "\n";
   Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: it's a "
                            "transitivity step.\n";
   Assert(d_node.isNull()
@@ -1186,23 +1200,24 @@ Node EqProof::addToProof(
   // example).
   if (d_node[0].getNumChildren() != d_node[1].getNumChildren())
   {
-    Assert(isNary);
+    Assert(isNary) << "We only handle congruences of apps with different "
+                      "number of children for theory n-ary operators";
     arity =
         d_node[1].getNumChildren() < arity ? arity : d_node[1].getNumChildren();
     Trace("eqproof-conv")
         << "EqProof::addToProof: Mismatching arities in cong conclusion "
         << d_node << ". Use tentative arity " << arity << "\n";
   }
-  // For a congruence proof of (= (f a0 ... an-1) (f b0 ... bn-1)), build a
-  // transitivity matrix where each row contains a transitivity chain justifying
-  // (= ai bi)
+  // For a congruence proof of (= (f a0 ... an-1) (g b0 ... bn-1)), build a
+  // transitivity matrix of n rows where the first row contains a transitivity
+  // chain justifying (= f g) and the next rows (= ai bi)
   std::vector<std::vector<Node>> transitivityChildren;
-  for (unsigned i = 0; i < arity; ++i)
+  for (unsigned i = 0; i < arity + 1; ++i)
   {
     transitivityChildren.push_back(std::vector<Node>());
   }
   reduceNestedCongruence(
-      arity - 1, d_node, transitivityChildren, p, visited, assumptions, isNary);
+      arity, d_node, transitivityChildren, p, visited, assumptions, isNary);
   // Congruences over n-ary operators may require changing the conclusion (as in
   // the above example). This is handled in a general manner below according to
   // whether the transitivity matrix computed by reduceNestedCongruence contains
@@ -1212,7 +1227,7 @@ Node EqProof::addToProof(
   if (isNary)
   {
     unsigned emptyRows = 0;
-    for (unsigned i = 0; i < arity; ++i)
+    for (unsigned i = 1; i <= arity; ++i)
     {
       if (transitivityChildren[i].empty())
       {
@@ -1232,7 +1247,11 @@ Node EqProof::addToProof(
     //  n - k1 == m - k2
     // Note that by construction the equality between the first emptyRows + 1
     // arguments of each application is justified by the transitivity step in
-    // the row emptyRows +1 in the matrix.
+    // the row emptyRows + 1 in the matrix.
+    //
+    // All of the above is with the very first row in the matrix, reserved for
+    // justifying the equality between the functions, which is not necessary in
+    // the n-ary case, notwithstanding.
     if (emptyRows > 0)
     {
       Trace("eqproof-conv")
@@ -1242,9 +1261,11 @@ Node EqProof::addToProof(
       // beginning are eliminated, as the new arity is the maximal arity among
       // the applications minus the number of empty rows.
       std::vector<std::vector<Node>> newTransitivityChildren{
-          transitivityChildren.begin() + emptyRows, transitivityChildren.end()};
+          transitivityChildren.begin() + 1 + emptyRows,
+          transitivityChildren.end()};
       transitivityChildren.clear();
-      transitivityChildren.insert(transitivityChildren.begin(),
+      transitivityChildren.push_back(std::vector<Node>());
+      transitivityChildren.insert(transitivityChildren.end(),
                                   newTransitivityChildren.begin(),
                                   newTransitivityChildren.end());
       unsigned arityPrefix1 =
@@ -1293,27 +1314,40 @@ Node EqProof::addToProof(
     Trace("eqproof-conv")
         << "EqProof::addToProof: premises from reduced cong of " << conclusion
         << ":\n";
-    for (unsigned i = 0; i < arity; ++i)
+    for (unsigned i = 0; i <= arity; ++i)
     {
       Trace("eqproof-conv") << "EqProof::addToProof:\t" << i
                             << "-th arg: " << transitivityChildren[i] << "\n";
     }
   }
+  std::vector<Node> children(arity + 1);
+  // Check if there is a justification for equality between functions (HO case)
+  if (!transitivityChildren[0].empty())
+  {
+    Assert(k == kind::APPLY_UF) << "Congruence with different functions only "
+                                   "allowed for uninterpreted functions.\n";
+
+    children[0] =
+        conclusion[0].getOperator().eqNode(conclusion[1].getOperator());
+    Assert(transitivityChildren[0].size() == 1
+           && CDProof::isSame(children[0], transitivityChildren[0][0]))
+        << "Justification of operators equality is wrong: "
+        << transitivityChildren[0] << "\n";
+  }
   // Proccess transitivity matrix to (possibly) generate transitivity steps for
   // congruence premises (= ai bi)
-  std::vector<Node> children(arity);
-  for (unsigned i = 0; i < arity; ++i)
+  for (unsigned i = 1; i <= arity; ++i)
   {
-    Node transConclusion = conclusion[0][i].eqNode(conclusion[1][i]);
+    Node transConclusion = conclusion[0][i - 1].eqNode(conclusion[1][i - 1]);
     children[i] = transConclusion;
     Assert(!transitivityChildren[i].empty())
         << "EqProof::addToProof: did not add any justification for " << i
         << "-th arg of congruence " << conclusion << "\n";
     // If the transitivity conclusion is a reflexivity step, just add it. Note
-    // that this can happen with with transitivityChildren containing several
-    // equalities in the case of (= ai bi) being the same n-ary application that
-    // was justified by a congruence step, which can happen in the current
-    // equality engine
+    // that this can happen even with the respective transitivityChildren row
+    // containing several equalities in the case of (= ai bi) being the same
+    // n-ary application that was justified by a congruence step, which can
+    // happen in the current equality engine.
     if (transConclusion[0] == transConclusion[1])
     {
       p->addStep(transConclusion, PfRule::REFL, {}, {transConclusion[0]});
@@ -1355,18 +1389,34 @@ Node EqProof::addToProof(
           transConclusion, PfRule::TRANS, transitivityChildren[i], {}, true);
     }
   }
-  // Get node of the function operator over which congruence is being applied.
-  std::vector<Node> args;
-  args.push_back(ProofRuleChecker::mkKindNode(k));
-  if (kind::metaKindOf(k) == kind::metakind::PARAMETERIZED)
+  // first-order case
+  if (children[0].isNull())
+  {
+    // remove placehold for function equality case
+    children.erase(children.begin());
+    // Get node of the function operator over which congruence is being
+    // applied.
+    std::vector<Node> args;
+    args.push_back(ProofRuleChecker::mkKindNode(k));
+    if (kind::metaKindOf(k) == kind::metakind::PARAMETERIZED)
+    {
+      args.push_back(conclusion[0].getOperator());
+    }
+    // Add congruence step
+    Trace("eqproof-conv") << "EqProof::addToProof: build cong step of "
+                          << conclusion << " with op " << args[0]
+                          << " and children " << children << "\n";
+    p->addStep(conclusion, PfRule::CONG, children, args, true);
+  }
+  // higher-order case
+  else
   {
-    args.push_back(conclusion[0].getOperator());
+    // Add congruence step
+    Trace("eqproof-conv") << "EqProof::addToProof: build HO-cong step of "
+                          << conclusion << " with children " << children
+                          << "\n";
+    p->addStep(conclusion, PfRule::HO_CONG, children, {}, true);
   }
-  // Add congruence step
-  Trace("eqproof-conv") << "EqProof::addToProof: build cong step of "
-                        << conclusion << " with op " << args[0]
-                        << " and children " << children << "\n";
-  p->addStep(conclusion, PfRule::CONG, children, args, true);
   // If the conclusion of the congruence step changed due to the n-ary handling,
   // we obtained for example (= (f (f t1 t2 t3) t4) (f (f t5 t6) t7)), which is
   // flattened into the original conclusion (= (f t1 t2 t3 t4) (f t5 t6 t7)) via