Remove template argument from `NodeBuilder`an/refactor/NodeBuilder

Currently, `NodeBuilder` takes a single template argument: An integer
that determines the expected number of arguments. This argument is used
to determine the size of the `d_inlineNvChildSpace` array. This array is
used to construct nodes inline. The advantage of this is that we don't
have to allocate a `NodeValue` on the heap for the node under
construction until we are sure that the node is new. While templating
the array size may save some stack space (or avoid a heap allocation if
we statically know that we a fixed number of children and that number is
greater than 10), it complicates the code and leads to longer compile
times. Thus, this commit removes the template argument and moves some of
the `NodeBuilder` code to a source file for faster compilation.

CPU build time before change (debug build): 2429.68s
CPU build time after change (debug build): 2228.44s

99 files changed, 1208 insertions, 1562 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 463fe74df..53242f077 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -46,6 +46,7 @@
 #include "expr/metakind.h"
 #include "expr/node.h"
 #include "expr/node_algorithm.h"
+#include "expr/node_builder.h"
 #include "expr/node_manager.h"
 #include "expr/sequence.h"
 #include "expr/type_node.h"
@@ -3960,7 +3961,7 @@ Term Grammar::purifySygusGTerm(
   if (term.d_node->getMetaKind() == kind::metakind::PARAMETERIZED)
   {
     // it's an indexed operator so we should provide the op
-    NodeBuilder<> nb(term.d_node->getKind());
+    NodeBuilder nb(term.d_node->getKind());
     nb << term.d_node->getOperator();
     nb.append(Term::termVectorToNodes(pchildren));
     nret = nb.constructNode();
@@ -4348,7 +4349,7 @@ Term Solver::mkTermHelper(const Op& op, const std::vector<Term>& children) const
   const cvc5::Kind int_kind = extToIntKind(op.d_kind);
   std::vector<Node> echildren = Term::termVectorToNodes(children);
 
-  NodeBuilder<> nb(int_kind);
+  NodeBuilder nb(int_kind);
   nb << *op.d_node;
   nb.append(echildren);
   Node res = nb.constructNode();
@@ -5547,7 +5548,7 @@ Term Solver::mkTuple(const std::vector<Sort>& sorts,
 
   Sort s = mkTupleSortHelper(sorts);
   Datatype dt = s.getDatatype();
-  NodeBuilder<> nb(extToIntKind(APPLY_CONSTRUCTOR));
+  NodeBuilder nb(extToIntKind(APPLY_CONSTRUCTOR));
   nb << *dt[0].getConstructorTerm().d_node;
   nb.append(args);
   Node res = nb.constructNode();
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 3e8717986..1161d1b70 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -38,6 +38,7 @@ libcvc4_add_sources(
   node.h
   node_algorithm.cpp
   node_algorithm.h
+  node_builder.cpp
   node_builder.h
   node_manager.cpp
   node_manager.h
diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
index 59b870897..ce15c7ede 100644
--- a/src/expr/dtype_cons.cpp
+++ b/src/expr/dtype_cons.cpp
@@ -655,7 +655,7 @@ TypeNode DTypeConstructor::doParametricSubstitution(
       }
     }
   }
-  NodeBuilder<> nb(range.getKind());
+  NodeBuilder nb(range.getKind());
   for (size_t i = 0, csize = children.size(); i < csize; ++i)
   {
     nb << children[i];
diff --git a/src/expr/node.h b/src/expr/node.h
index 29bfaa157..fb3cf1478 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -196,7 +196,6 @@ class NodeTemplate {
   friend class TypeNode;
   friend class NodeManager;
 
-  template <unsigned nchild_thresh>
   friend class NodeBuilder;
 
   friend class ::cvc5::expr::attr::AttributeManager;
@@ -1291,7 +1290,7 @@ NodeTemplate<ref_count>::substitute(TNode node, TNode replacement,
   }
 
   // otherwise compute
-  NodeBuilder<> nb(getKind());
+  NodeBuilder nb(getKind());
   if(getMetaKind() == kind::metakind::PARAMETERIZED) {
     // push the operator
     if(getOperator() == node) {
@@ -1359,7 +1358,7 @@ NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
     cache[*this] = *this;
     return *this;
   } else {
-    NodeBuilder<> nb(getKind());
+    NodeBuilder nb(getKind());
     if(getMetaKind() == kind::metakind::PARAMETERIZED) {
       // push the operator
       nb << getOperator().substitute(nodesBegin, nodesEnd,
@@ -1421,7 +1420,7 @@ NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin,
     cache[*this] = *this;
     return *this;
   } else {
-    NodeBuilder<> nb(getKind());
+    NodeBuilder nb(getKind());
     if(getMetaKind() == kind::metakind::PARAMETERIZED) {
       // push the operator
       nb << getOperator().substitute(substitutionsBegin, substitutionsEnd, cache);
diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index bcf74a944..1fb1a5220 100644
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -624,7 +624,7 @@ Node substituteCaptureAvoiding(TNode n,
     else if (it->second.isNull())
     {
       // build node
-      NodeBuilder<> nb(curr.getKind());
+      NodeBuilder nb(curr.getKind());
       if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
       {
         // push the operator
diff --git a/src/expr/node_builder.cpp b/src/expr/node_builder.cpp
new file mode 100644
index 000000000..72b7dd4dc
--- /dev/null
+++ b/src/expr/node_builder.cpp
@@ -0,0 +1,717 @@
+/*********************                                                        */
+/*! \file node_builder.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 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 A builder interface for Nodes.
+ **/
+
+#include "expr/node_builder.h"
+
+#include <memory>
+
+namespace cvc5 {
+
+NodeBuilder::NodeBuilder()
+    : d_nv(&d_inlineNv),
+      d_nm(NodeManager::currentNM()),
+      d_nvMaxChildren(default_nchild_thresh)
+{
+  d_inlineNv.d_id = 0;
+  d_inlineNv.d_rc = 0;
+  d_inlineNv.d_kind = expr::NodeValue::kindToDKind(kind::UNDEFINED_KIND);
+  d_inlineNv.d_nchildren = 0;
+}
+
+NodeBuilder::NodeBuilder(Kind k)
+    : d_nv(&d_inlineNv),
+      d_nm(NodeManager::currentNM()),
+      d_nvMaxChildren(default_nchild_thresh)
+{
+  Assert(k != kind::NULL_EXPR && k != kind::UNDEFINED_KIND)
+      << "illegal Node-building kind";
+
+  d_inlineNv.d_id = 1;  // have a kind already
+  d_inlineNv.d_rc = 0;
+  d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k);
+  d_inlineNv.d_nchildren = 0;
+}
+
+NodeBuilder::NodeBuilder(NodeManager* nm)
+    : d_nv(&d_inlineNv), d_nm(nm), d_nvMaxChildren(default_nchild_thresh)
+{
+  d_inlineNv.d_id = 0;
+  d_inlineNv.d_rc = 0;
+  d_inlineNv.d_kind = expr::NodeValue::kindToDKind(kind::UNDEFINED_KIND);
+  d_inlineNv.d_nchildren = 0;
+}
+
+NodeBuilder::NodeBuilder(NodeManager* nm, Kind k)
+    : d_nv(&d_inlineNv), d_nm(nm), d_nvMaxChildren(default_nchild_thresh)
+{
+  Assert(k != kind::NULL_EXPR && k != kind::UNDEFINED_KIND)
+      << "illegal Node-building kind";
+
+  d_inlineNv.d_id = 1;  // have a kind already
+  d_inlineNv.d_rc = 0;
+  d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k);
+  d_inlineNv.d_nchildren = 0;
+}
+
+NodeBuilder::NodeBuilder(const NodeBuilder& nb)
+    : d_nv(&d_inlineNv), d_nm(nb.d_nm), d_nvMaxChildren(default_nchild_thresh)
+{
+  d_inlineNv.d_id = nb.d_nv->d_id;
+  d_inlineNv.d_rc = 0;
+  d_inlineNv.d_kind = nb.d_nv->d_kind;
+  d_inlineNv.d_nchildren = 0;
+
+  internalCopy(nb);
+}
+
+NodeBuilder::~NodeBuilder()
+{
+  if (__builtin_expect((nvIsAllocated()), false))
+  {
+    dealloc();
+  }
+  else if (__builtin_expect((!isUsed()), false))
+  {
+    decrRefCounts();
+  }
+}
+
+Kind NodeBuilder::getKind() const
+{
+  Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                       "attempt to access it after conversion";
+  return d_nv->getKind();
+}
+
+kind::MetaKind NodeBuilder::getMetaKind() const
+{
+  Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                       "attempt to access it after conversion";
+  Assert(getKind() != kind::UNDEFINED_KIND)
+      << "The metakind of a NodeBuilder is undefined "
+         "until a Kind is set";
+  return d_nv->getMetaKind();
+}
+
+unsigned NodeBuilder::getNumChildren() const
+{
+  Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                       "attempt to access it after conversion";
+  Assert(getKind() != kind::UNDEFINED_KIND)
+      << "The number of children of a NodeBuilder is undefined "
+         "until a Kind is set";
+  return d_nv->getNumChildren();
+}
+
+Node NodeBuilder::getOperator() const
+{
+  Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                       "attempt to access it after conversion";
+  Assert(getKind() != kind::UNDEFINED_KIND)
+      << "NodeBuilder operator access is not permitted "
+         "until a Kind is set";
+  Assert(getMetaKind() == kind::metakind::PARAMETERIZED)
+      << "NodeBuilder operator access is only permitted "
+         "on parameterized kinds, not `"
+      << getKind() << "'";
+  return Node(d_nv->getOperator());
+}
+
+Node NodeBuilder::getChild(int i) const
+{
+  Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                       "attempt to access it after conversion";
+  Assert(getKind() != kind::UNDEFINED_KIND)
+      << "NodeBuilder child access is not permitted "
+         "until a Kind is set";
+  Assert(i >= 0 && unsigned(i) < d_nv->getNumChildren())
+      << "index out of range for NodeBuilder::getChild()";
+  return Node(d_nv->getChild(i));
+}
+
+Node NodeBuilder::operator[](int i) const { return getChild(i); }
+
+void NodeBuilder::clear(Kind k)
+{
+  Assert(k != kind::NULL_EXPR) << "illegal Node-building clear kind";
+
+  if (__builtin_expect((nvIsAllocated()), false))
+  {
+    dealloc();
+  }
+  else if (__builtin_expect((!isUsed()), false))
+  {
+    decrRefCounts();
+  }
+  else
+  {
+    setUnused();
+  }
+
+  d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k);
+  for (expr::NodeValue::nv_iterator i = d_inlineNv.nv_begin();
+       i != d_inlineNv.nv_end();
+       ++i)
+  {
+    (*i)->dec();
+  }
+  d_inlineNv.d_nchildren = 0;
+  // keep track of whether or not we hvae a kind already
+  d_inlineNv.d_id = (k == kind::UNDEFINED_KIND) ? 0 : 1;
+}
+
+NodeBuilder& NodeBuilder::operator<<(const Kind& k)
+{
+  Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                       "attempt to access it after conversion";
+  Assert(getKind() == kind::UNDEFINED_KIND || d_nv->d_id == 0)
+      << "can't redefine the Kind of a NodeBuilder";
+  Assert(d_nv->d_id == 0)
+      << "internal inconsistency with NodeBuilder: d_id != 0";
+  AssertArgument(
+      k != kind::UNDEFINED_KIND && k != kind::NULL_EXPR && k < kind::LAST_KIND,
+      k,
+      "illegal node-building kind");
+  // This test means: we didn't have a Kind at the beginning (on
+  // NodeBuilder construction or at the last clear()), but we do
+  // now.  That means we appended a Kind with operator<<(Kind),
+  // which now (lazily) we'll collapse.
+  if (__builtin_expect((d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND),
+                       false))
+  {
+    Node n2 = operator Node();
+    clear();
+    append(n2);
+  }
+  else if (d_nv->d_nchildren == 0)
+  {
+    d_nv->d_id = 1;  // remember that we had a kind from the start
+  }
+  d_nv->d_kind = expr::NodeValue::kindToDKind(k);
+  return *this;
+}
+
+NodeBuilder& NodeBuilder::operator<<(TNode n)
+{
+  Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                       "attempt to access it after conversion";
+  // This test means: we didn't have a Kind at the beginning (on
+  // NodeBuilder construction or at the last clear()), but we do
+  // now.  That means we appended a Kind with operator<<(Kind),
+  // which now (lazily) we'll collapse.
+  if (__builtin_expect((d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND),
+                       false))
+  {
+    Node n2 = operator Node();
+    clear();
+    append(n2);
+  }
+  return append(n);
+}
+
+NodeBuilder& NodeBuilder::operator<<(TypeNode n)
+{
+  Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                       "attempt to access it after conversion";
+  // This test means: we didn't have a Kind at the beginning (on
+  // NodeBuilder construction or at the last clear()), but we do
+  // now.  That means we appended a Kind with operator<<(Kind),
+  // which now (lazily) we'll collapse.
+  if (__builtin_expect((d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND),
+                       false))
+  {
+    Node n2 = operator Node();
+    clear();
+    append(n2);
+  }
+  return append(n);
+}
+
+NodeBuilder& NodeBuilder::append(const std::vector<TypeNode>& children)
+{
+  Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                       "attempt to access it after conversion";
+  return append(children.begin(), children.end());
+}
+
+NodeBuilder& NodeBuilder::append(TNode n)
+{
+  Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                       "attempt to access it after conversion";
+  Assert(!n.isNull()) << "Cannot use NULL Node as a child of a Node";
+  if (n.getKind() == kind::BUILTIN)
+  {
+    return *this << NodeManager::operatorToKind(n);
+  }
+  allocateNvIfNecessaryForAppend();
+  expr::NodeValue* nv = n.d_nv;
+  nv->inc();
+  d_nv->d_children[d_nv->d_nchildren++] = nv;
+  Assert(d_nv->d_nchildren <= d_nvMaxChildren);
+  return *this;
+}
+
+NodeBuilder& NodeBuilder::append(const TypeNode& typeNode)
+{
+  Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                       "attempt to access it after conversion";
+  Assert(!typeNode.isNull()) << "Cannot use NULL Node as a child of a Node";
+  allocateNvIfNecessaryForAppend();
+  expr::NodeValue* nv = typeNode.d_nv;
+  nv->inc();
+  d_nv->d_children[d_nv->d_nchildren++] = nv;
+  Assert(d_nv->d_nchildren <= d_nvMaxChildren);
+  return *this;
+}
+
+void NodeBuilder::realloc(size_t toSize)
+{
+  AlwaysAssert(toSize > d_nvMaxChildren)
+      << "attempt to realloc() a NodeBuilder to a smaller/equal size!";
+  Assert(toSize < (static_cast<size_t>(1) << expr::NodeValue::NBITS_NCHILDREN))
+      << "attempt to realloc() a NodeBuilder to size " << toSize
+      << " (beyond hard limit of " << expr::NodeValue::MAX_CHILDREN << ")";
+
+  if (__builtin_expect((nvIsAllocated()), false))
+  {
+    // Ensure d_nv is not modified on allocation failure
+    expr::NodeValue* newBlock = (expr::NodeValue*)std::realloc(
+        d_nv, sizeof(expr::NodeValue) + (sizeof(expr::NodeValue*) * toSize));
+    if (newBlock == NULL)
+    {
+      // In this case, d_nv was NOT freed.  If we throw, the
+      // deallocation should occur on destruction of the NodeBuilder.
+      throw std::bad_alloc();
+    }
+    d_nvMaxChildren = toSize;
+    Assert(d_nvMaxChildren == toSize);  // overflow check
+    // Here, the copy (between two heap-allocated buffers) has already
+    // been done for us by the std::realloc().
+    d_nv = newBlock;
+  }
+  else
+  {
+    // Ensure d_nv is not modified on allocation failure
+    expr::NodeValue* newBlock = (expr::NodeValue*)std::malloc(
+        sizeof(expr::NodeValue) + (sizeof(expr::NodeValue*) * toSize));
+    if (newBlock == NULL)
+    {
+      throw std::bad_alloc();
+    }
+    d_nvMaxChildren = toSize;
+    Assert(d_nvMaxChildren == toSize);  // overflow check
+
+    d_nv = newBlock;
+    d_nv->d_id = d_inlineNv.d_id;
+    d_nv->d_rc = 0;
+    d_nv->d_kind = d_inlineNv.d_kind;
+    d_nv->d_nchildren = d_inlineNv.d_nchildren;
+
+    std::copy(d_inlineNv.d_children,
+              d_inlineNv.d_children + d_inlineNv.d_nchildren,
+              d_nv->d_children);
+
+    // ensure "inline" children don't get decremented in dtor
+    d_inlineNv.d_nchildren = 0;
+  }
+}
+
+void NodeBuilder::dealloc()
+{
+  Assert(nvIsAllocated())
+      << "Internal error: NodeBuilder: dealloc() called without a "
+         "private NodeBuilder-allocated buffer";
+
+  for (expr::NodeValue::nv_iterator i = d_nv->nv_begin(); i != d_nv->nv_end();
+       ++i)
+  {
+    (*i)->dec();
+  }
+
+  free(d_nv);
+  d_nv = &d_inlineNv;
+  d_nvMaxChildren = default_nchild_thresh;
+}
+
+void NodeBuilder::decrRefCounts()
+{
+  Assert(!nvIsAllocated())
+      << "Internal error: NodeBuilder: decrRefCounts() called with a "
+         "private NodeBuilder-allocated buffer";
+
+  for (expr::NodeValue::nv_iterator i = d_inlineNv.nv_begin();
+       i != d_inlineNv.nv_end();
+       ++i)
+  {
+    (*i)->dec();
+  }
+
+  d_inlineNv.d_nchildren = 0;
+}
+
+TypeNode NodeBuilder::constructTypeNode() { return TypeNode(constructNV()); }
+
+Node NodeBuilder::constructNode()
+{
+  Node n(constructNV());
+  maybeCheckType(n);
+  return n;
+}
+
+Node* NodeBuilder::constructNodePtr()
+{
+  std::unique_ptr<Node> np(new Node(constructNV()));
+  maybeCheckType(*np.get());
+  return np.release();
+}
+
+NodeBuilder::operator Node() { return constructNode(); }
+
+NodeBuilder::operator TypeNode() { return constructTypeNode(); }
+
+expr::NodeValue* NodeBuilder::constructNV()
+{
+  Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                       "attempt to access it after conversion";
+  Assert(getKind() != kind::UNDEFINED_KIND)
+      << "Can't make an expression of an undefined kind!";
+
+  // NOTE: The comments in this function refer to the cases in the
+  // file comments at the top of this file.
+
+  // Case 0: If a VARIABLE
+  if (getMetaKind() == kind::metakind::VARIABLE
+      || getMetaKind() == kind::metakind::NULLARY_OPERATOR)
+  {
+    /* 0. If a VARIABLE, treat similarly to 1(b), except that we know
+     * there are no children (no reference counts to reason about),
+     * and we don't keep VARIABLE-kinded Nodes in the NodeManager
+     * pool. */
+
+    Assert(!nvIsAllocated())
+        << "internal NodeBuilder error: "
+           "VARIABLE-kinded NodeBuilder is heap-allocated !?";
+    Assert(d_inlineNv.d_nchildren == 0)
+        << "improperly-formed VARIABLE-kinded NodeBuilder: "
+           "no children permitted";
+
+    // we have to copy the inline NodeValue out
+    expr::NodeValue* nv =
+        (expr::NodeValue*)std::malloc(sizeof(expr::NodeValue));
+    if (nv == NULL)
+    {
+      throw std::bad_alloc();
+    }
+    // there are no children, so we don't have to worry about
+    // reference counts in this case.
+    nv->d_nchildren = 0;
+    nv->d_kind = d_nv->d_kind;
+    nv->d_id = d_nm->next_id++;  // FIXME multithreading
+    nv->d_rc = 0;
+    setUsed();
+    if (Debug.isOn("gc"))
+    {
+      Debug("gc") << "creating node value " << nv << " [" << nv->d_id << "]: ";
+      nv->printAst(Debug("gc"));
+      Debug("gc") << std::endl;
+    }
+    return nv;
+  }
+
+  // check that there are the right # of children for this kind
+  Assert(getMetaKind() != kind::metakind::CONSTANT)
+      << "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds";
+  Assert(getNumChildren() >= kind::metakind::getMinArityForKind(getKind()))
+      << "Nodes with kind " << getKind() << " must have at least "
+      << kind::metakind::getMinArityForKind(getKind())
+      << " children (the one under "
+         "construction has "
+      << getNumChildren() << ")";
+  Assert(getNumChildren() <= kind::metakind::getMaxArityForKind(getKind()))
+      << "Nodes with kind " << getKind() << " must have at most "
+      << kind::metakind::getMaxArityForKind(getKind())
+      << " children (the one under "
+         "construction has "
+      << getNumChildren() << ")";
+
+  // Implementation differs depending on whether the NodeValue was
+  // malloc'ed or not and whether or not it's in the already-been-seen
+  // NodeManager pool of Nodes.  See implementation notes at the top
+  // of this file.
+
+  if (__builtin_expect((!nvIsAllocated()), true))
+  {
+    /** Case 1.  d_nv points to d_inlineNv: it is the backing store
+     ** allocated "inline" in this NodeBuilder. **/
+
+    // Lookup the expression value in the pool we already have
+    expr::NodeValue* poolNv = d_nm->poolLookup(&d_inlineNv);
+    // If something else is there, we reuse it
+    if (poolNv != NULL)
+    {
+      /* Subcase (a): The Node under construction already exists in
+       * the NodeManager's pool. */
+
+      /* 1(a). Reference-counts for all children in d_inlineNv must be
+       * decremented, and the NodeBuilder must be marked as "used" and
+       * the number of children set to zero so that we don't decrement
+       * them again on destruction.  The existing NodeManager pool
+       * entry is returned.
+       */
+      decrRefCounts();
+      d_inlineNv.d_nchildren = 0;
+      setUsed();
+      return poolNv;
+    }
+    else
+    {
+      /* Subcase (b): The Node under construction is NOT already in
+       * the NodeManager's pool. */
+
+      /* 1(b). A new heap-allocated NodeValue must be constructed and
+       * all settings and children from d_inlineNv copied into it.
+       * This new NodeValue is put into the NodeManager's pool.  The
+       * NodeBuilder is marked as "used" and the number of children in
+       * d_inlineNv set to zero so that we don't decrement child
+       * reference counts on destruction (the child reference counts
+       * have been "taken over" by the new NodeValue).  We return a
+       * Node wrapper for this new NodeValue, which increments its
+       * reference count. */
+
+      // create the canonical expression value for this node
+      expr::NodeValue* nv = (expr::NodeValue*)std::malloc(
+          sizeof(expr::NodeValue)
+          + (sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren));
+      if (nv == NULL)
+      {
+        throw std::bad_alloc();
+      }
+      nv->d_nchildren = d_inlineNv.d_nchildren;
+      nv->d_kind = d_inlineNv.d_kind;
+      nv->d_id = d_nm->next_id++;  // FIXME multithreading
+      nv->d_rc = 0;
+
+      std::copy(d_inlineNv.d_children,
+                d_inlineNv.d_children + d_inlineNv.d_nchildren,
+                nv->d_children);
+
+      d_inlineNv.d_nchildren = 0;
+      setUsed();
+
+      // poolNv = nv;
+      d_nm->poolInsert(nv);
+      if (Debug.isOn("gc"))
+      {
+        Debug("gc") << "creating node value " << nv << " [" << nv->d_id
+                    << "]: ";
+        nv->printAst(Debug("gc"));
+        Debug("gc") << std::endl;
+      }
+      return nv;
+    }
+  }
+  else
+  {
+    /** Case 2. d_nv does NOT point to d_inlineNv: it is a new, larger
+     ** buffer that was heap-allocated by this NodeBuilder. **/
+
+    // Lookup the expression value in the pool we already have (with insert)
+    expr::NodeValue* poolNv = d_nm->poolLookup(d_nv);
+    // If something else is there, we reuse it
+    if (poolNv != NULL)
+    {
+      /* Subcase (a): The Node under construction already exists in
+       * the NodeManager's pool. */
+
+      /* 2(a). Reference-counts for all children in d_nv must be
+       * decremented.  The NodeBuilder is marked as "used" and the
+       * heap-allocated d_nv deleted.  d_nv is repointed to d_inlineNv
+       * so that destruction of the NodeBuilder doesn't cause any
+       * problems.  The existing NodeManager pool entry is
+       * returned. */
+
+      dealloc();
+      setUsed();
+      return poolNv;
+    }
+    else
+    {
+      /* Subcase (b) The Node under construction is NOT already in the
+       * NodeManager's pool. */
+
+      /* 2(b). The heap-allocated d_nv is "cropped" to the correct
+       * size (based on the number of children it _actually_ has).
+       * d_nv is repointed to d_inlineNv so that destruction of the
+       * NodeBuilder doesn't cause any problems, and the (old) value
+       * it had is placed into the NodeManager's pool and returned in
+       * a Node wrapper. */
+
+      crop();
+      expr::NodeValue* nv = d_nv;
+      nv->d_id = d_nm->next_id++;  // FIXME multithreading
+      d_nv = &d_inlineNv;
+      d_nvMaxChildren = default_nchild_thresh;
+      setUsed();
+
+      // poolNv = nv;
+      d_nm->poolInsert(nv);
+      Debug("gc") << "creating node value " << nv << " [" << nv->d_id
+                  << "]: " << *nv << "\n";
+      return nv;
+    }
+  }
+}
+
+void NodeBuilder::internalCopy(const NodeBuilder& nb)
+{
+  if (nb.isUsed())
+  {
+    setUsed();
+    return;
+  }
+
+  bool realloced CVC4_UNUSED = false;
+  if (nb.d_nvMaxChildren > d_nvMaxChildren)
+  {
+    realloced = true;
+    realloc(nb.d_nvMaxChildren);
+  }
+
+  Assert(nb.d_nvMaxChildren <= d_nvMaxChildren);
+  Assert(nb.d_nv->nv_end() >= nb.d_nv->nv_begin());
+  Assert((size_t)(nb.d_nv->nv_end() - nb.d_nv->nv_begin()) <= d_nvMaxChildren)
+      << "realloced:" << (realloced ? "true" : "false")
+      << ", d_nvMax:" << d_nvMaxChildren
+      << ", size:" << nb.d_nv->nv_end() - nb.d_nv->nv_begin()
+      << ", nc:" << nb.d_nv->getNumChildren();
+  std::copy(nb.d_nv->nv_begin(), nb.d_nv->nv_end(), d_nv->nv_begin());
+
+  d_nv->d_nchildren = nb.d_nv->d_nchildren;
+
+  for (expr::NodeValue::nv_iterator i = d_nv->nv_begin(); i != d_nv->nv_end();
+       ++i)
+  {
+    (*i)->inc();
+  }
+}
+
+#ifdef CVC4_DEBUG
+inline void NodeBuilder::maybeCheckType(const TNode n) const
+{
+  /* force an immediate type check, if early type checking is
+     enabled and the current node isn't a variable or constant */
+  kind::MetaKind mk = n.getMetaKind();
+  if (mk != kind::metakind::VARIABLE && mk != kind::metakind::NULLARY_OPERATOR
+      && mk != kind::metakind::CONSTANT)
+  {
+    d_nm->getType(n, true);
+  }
+}
+#endif /* CVC4_DEBUG */
+
+bool NodeBuilder::isUsed() const
+{
+  return __builtin_expect((d_nv == NULL), false);
+}
+
+void NodeBuilder::setUsed()
+{
+  Assert(!isUsed()) << "Internal error: bad `used' state in NodeBuilder!";
+  Assert(d_inlineNv.d_nchildren == 0
+         && d_nvMaxChildren == default_nchild_thresh)
+      << "Internal error: bad `inline' state in NodeBuilder!";
+  d_nv = NULL;
+}
+
+void NodeBuilder::setUnused()
+{
+  Assert(isUsed()) << "Internal error: bad `used' state in NodeBuilder!";
+  Assert(d_inlineNv.d_nchildren == 0
+         && d_nvMaxChildren == default_nchild_thresh)
+      << "Internal error: bad `inline' state in NodeBuilder!";
+  d_nv = &d_inlineNv;
+}
+
+bool NodeBuilder::nvIsAllocated() const
+{
+  return __builtin_expect((d_nv != &d_inlineNv), false)
+         && __builtin_expect((d_nv != NULL), true);
+}
+
+bool NodeBuilder::nvNeedsToBeAllocated() const
+{
+  return __builtin_expect((d_nv->d_nchildren == d_nvMaxChildren), false);
+}
+
+void NodeBuilder::realloc()
+{
+  size_t newSize = 2 * size_t(d_nvMaxChildren);
+  size_t hardLimit = expr::NodeValue::MAX_CHILDREN;
+  realloc(__builtin_expect((newSize > hardLimit), false) ? hardLimit : newSize);
+}
+
+void NodeBuilder::allocateNvIfNecessaryForAppend()
+{
+  if (__builtin_expect((nvNeedsToBeAllocated()), false))
+  {
+    realloc();
+  }
+}
+
+void NodeBuilder::crop()
+{
+  if (__builtin_expect((nvIsAllocated()), false)
+      && __builtin_expect((d_nvMaxChildren > d_nv->d_nchildren), true))
+  {
+    // Ensure d_nv is not modified on allocation failure
+    expr::NodeValue* newBlock = (expr::NodeValue*)std::realloc(
+        d_nv,
+        sizeof(expr::NodeValue)
+            + (sizeof(expr::NodeValue*) * d_nv->d_nchildren));
+    if (newBlock == NULL)
+    {
+      // In this case, d_nv was NOT freed.  If we throw, the
+      // deallocation should occur on destruction of the
+      // NodeBuilder.
+      throw std::bad_alloc();
+    }
+    d_nv = newBlock;
+    d_nvMaxChildren = d_nv->d_nchildren;
+  }
+}
+
+NodeBuilder& NodeBuilder::collapseTo(Kind k)
+{
+  AssertArgument(
+      k != kind::UNDEFINED_KIND && k != kind::NULL_EXPR && k < kind::LAST_KIND,
+      k,
+      "illegal collapsing kind");
+
+  if (getKind() != k)
+  {
+    Node n = operator Node();
+    clear();
+    d_nv->d_kind = expr::NodeValue::kindToDKind(k);
+    d_nv->d_id = 1;  // have a kind already
+    return append(n);
+  }
+  return *this;
+}
+
+std::ostream& operator<<(std::ostream& out, const NodeBuilder& nb)
+{
+  return out << *nb.d_nv;
+}
+
+}  // namespace cvc5
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index eaf5b040d..218a08766 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -102,7 +102,7 @@
  **         returned in a Node wrapper.
  **
  ** NOTE IN 1(b) AND 2(b) THAT we can NOT create Node wrapper
- ** temporary for the NodeValue in the NodeBuilder<>::operator Node()
+ ** temporary for the NodeValue in the NodeBuilder::operator Node()
  ** member function.  If we create a temporary (for example by writing
  ** Debug("builder") << Node(nv) << endl), the NodeValue will have its
  ** reference count incremented from zero to one, then decremented,
@@ -130,413 +130,70 @@
  **   2. d_nv != &d_inlineNv (d_nv heap-allocated by NodeBuilder): all
  **      d_nv children have their reference counts decremented, and
  **      d_nv is deallocated.
- **
- ** Regarding the backing store (typically on the stack): the file
- ** below provides the template:
- **
- **   template < unsigned nchild_thresh > class NodeBuilder;
- **
- **     The default:
- **
- **       NodeBuilder<> b;
- **
- **     gives you a backing buffer with capacity for 10 children in
- **     the same place as the NodeBuilder<> itself is allocated.  You
- **     can specify another size as a template parameter, but it must
- **     be a compile-time constant.
  **/
 
 #include "cvc4_private.h"
 
 /* strong dependency; make sure node is included first */
 #include "expr/node.h"
-#include "expr/type_node.h"
 
 #ifndef CVC4__NODE_BUILDER_H
 #define CVC4__NODE_BUILDER_H
 
-#include <cstdlib>
 #include <iostream>
-#include <memory>
 #include <vector>
 
-namespace cvc5 {
-static const unsigned default_nchild_thresh = 10;
-
-template <unsigned nchild_thresh>
-class NodeBuilder;
-
-class NodeManager;
-}  // namespace cvc5
-
 #include "base/check.h"
-#include "base/output.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
 #include "expr/node_value.h"
+#include "expr/type_node.h"
 
 namespace cvc5 {
 
-// Sometimes it's useful for debugging to output a NodeBuilder that
-// isn't yet a Node..
-template <unsigned nchild_thresh>
-std::ostream& operator<<(std::ostream& out, const NodeBuilder<nchild_thresh>& nb);
+class NodeManager;
 
 /**
- * The main template NodeBuilder.
+ * The NodeBuilder.
  */
-template <unsigned nchild_thresh = default_nchild_thresh>
 class NodeBuilder {
-  /**
-   * An "in-line" stack-allocated buffer for use by the
-   * NodeBuilder.
-   */
-  expr::NodeValue d_inlineNv;
-  /**
-   * Space for the children of the node being constructed.  This is
-   * never accessed directly, but rather through
-   * d_inlineNv.d_children[i].
-   */
-  expr::NodeValue* d_inlineNvChildSpace[nchild_thresh];
-
-  /**
-   * A pointer to the "current" NodeValue buffer; either &d_inlineNv
-   * or a heap-allocated one if d_inlineNv wasn't big enough.
-   */
-  expr::NodeValue* d_nv;
-
-  /** The NodeManager at play */
-  NodeManager* d_nm;
-
-  /**
-   * The number of children allocated in d_nv.
-   */
-  uint32_t d_nvMaxChildren;
-
-  template <unsigned N>
-  void internalCopy(const NodeBuilder<N>& nb);
-
-  /**
-   * Returns whether or not this NodeBuilder has been "used"---i.e.,
-   * whether a Node has been extracted with operator Node().
-   * Internally, this state is represented by d_nv pointing to NULL.
-   */
-  inline bool isUsed() const {
-    return __builtin_expect( ( d_nv == NULL ), false );
-  }
-
-  /**
-   * Set this NodeBuilder to the `used' state.
-   */
-  inline void setUsed() {
-    Assert(!isUsed()) << "Internal error: bad `used' state in NodeBuilder!";
-    Assert(d_inlineNv.d_nchildren == 0 && d_nvMaxChildren == nchild_thresh)
-        << "Internal error: bad `inline' state in NodeBuilder!";
-    d_nv = NULL;
-  }
-
-  /**
-   * Set this NodeBuilder to the `unused' state.  Should only be done
-   * from clear().
-   */
-  inline void setUnused() {
-    Assert(isUsed()) << "Internal error: bad `used' state in NodeBuilder!";
-    Assert(d_inlineNv.d_nchildren == 0 && d_nvMaxChildren == nchild_thresh)
-        << "Internal error: bad `inline' state in NodeBuilder!";
-    d_nv = &d_inlineNv;
-  }
-
-  /**
-   * Returns true if d_nv is *not* the "in-line" one (it was
-   * heap-allocated by this class).
-   */
-  inline bool nvIsAllocated() const {
-    return __builtin_expect( ( d_nv != &d_inlineNv ), false ) && __builtin_expect(( d_nv != NULL ), true );
-  }
-
-  /**
-   * Returns true if adding a child requires (re)allocation of d_nv
-   * first.
-   */
-  inline bool nvNeedsToBeAllocated() const {
-    return __builtin_expect( ( d_nv->d_nchildren == d_nvMaxChildren ), false );
-  }
-
-  /**
-   * (Re)allocate d_nv using a default grow factor.  Ensure that child
-   * pointers are copied into the new buffer, and if the "inline"
-   * NodeValue is evacuated, make sure its children won't be
-   * double-decremented later (on destruction/clear).
-   */
-  inline void realloc()
-  {
-    size_t newSize = 2 * size_t(d_nvMaxChildren);
-    size_t hardLimit = expr::NodeValue::MAX_CHILDREN;
-    realloc(__builtin_expect((newSize > hardLimit), false) ? hardLimit
-                                                           : newSize);
-  }
-
-  /**
-   * (Re)allocate d_nv to a specific size.  Specify "copy" if the
-   * children should be copied; if they are, and if the "inline"
-   * NodeValue is evacuated, make sure its children won't be
-   * double-decremented later (on destruction/clear).
-   */
-  void realloc(size_t toSize);
-
-  /**
-   * If d_nv needs to be (re)allocated to add an additional child, do
-   * so using realloc(), which ensures child pointers are copied and
-   * that the reference counts of the "inline" NodeValue won't be
-   * double-decremented on destruction/clear.  Otherwise, do nothing.
-   */
-  inline void allocateNvIfNecessaryForAppend() {
-    if(__builtin_expect( ( nvNeedsToBeAllocated() ), false )) {
-      realloc();
-    }
-  }
-
-  /**
-   * Deallocate a d_nv that was heap-allocated by this class during
-   * grow operations.  (Marks this NodeValue no longer allocated so
-   * that double-deallocations don't occur.)
-   *
-   * PRECONDITION: only call this when nvIsAllocated() == true.
-   * POSTCONDITION: !nvIsAllocated()
-   */
-  void dealloc();
-
-  /**
-   * "Purge" the "inline" children.  Decrement all their reference
-   * counts and set the number of children to zero.
-   *
-   * PRECONDITION: only call this when nvIsAllocated() == false.
-   * POSTCONDITION: d_inlineNv.d_nchildren == 0.
-   */
-  void decrRefCounts();
-
-  /**
-   * Trim d_nv down to the size it needs to be for the number of
-   * children it has.  Used when a Node is extracted from a
-   * NodeBuilder and we want the returned memory not to suffer from
-   * internal fragmentation.  If d_nv was not heap-allocated by this
-   * class, or is already the right size, this function does nothing.
-   *
-   * @throws bad_alloc if the reallocation fails
-   */
-  void crop() {
-    if(__builtin_expect( ( nvIsAllocated() ), false ) &&
-       __builtin_expect( ( d_nvMaxChildren > d_nv->d_nchildren ), true )) {
-      // Ensure d_nv is not modified on allocation failure
-      expr::NodeValue* newBlock = (expr::NodeValue*)
-        std::realloc(d_nv,
-                     sizeof(expr::NodeValue) +
-                     ( sizeof(expr::NodeValue*) * d_nv->d_nchildren ));
-      if(newBlock == NULL) {
-        // In this case, d_nv was NOT freed.  If we throw, the
-        // deallocation should occur on destruction of the
-        // NodeBuilder.
-        throw std::bad_alloc();
-      }
-      d_nv = newBlock;
-      d_nvMaxChildren = d_nv->d_nchildren;
-    }
-  }
-
-  // used by convenience node builders
-  NodeBuilder<nchild_thresh>& collapseTo(Kind k) {
-    AssertArgument(k != kind::UNDEFINED_KIND &&
-                   k != kind::NULL_EXPR &&
-                   k < kind::LAST_KIND,
-                   k, "illegal collapsing kind");
-
-    if(getKind() != k) {
-      Node n = operator Node();
-      clear();
-      d_nv->d_kind = expr::NodeValue::kindToDKind(k);
-      d_nv->d_id = 1; // have a kind already
-      return append(n);
-    }
-    return *this;
-  }
-
-public:
-
-  inline NodeBuilder() :
-    d_nv(&d_inlineNv),
-    d_nm(NodeManager::currentNM()),
-    d_nvMaxChildren(nchild_thresh) {
-
-    d_inlineNv.d_id = 0;
-    d_inlineNv.d_rc = 0;
-    d_inlineNv.d_kind = expr::NodeValue::kindToDKind(kind::UNDEFINED_KIND);
-    d_inlineNv.d_nchildren = 0;
-  }
-
-  inline NodeBuilder(Kind k) :
-    d_nv(&d_inlineNv),
-    d_nm(NodeManager::currentNM()),
-    d_nvMaxChildren(nchild_thresh) {
-    Assert(k != kind::NULL_EXPR && k != kind::UNDEFINED_KIND)
-        << "illegal Node-building kind";
-
-    d_inlineNv.d_id = 1; // have a kind already
-    d_inlineNv.d_rc = 0;
-    d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k);
-    d_inlineNv.d_nchildren = 0;
-  }
-
-  inline NodeBuilder(NodeManager* nm) :
-    d_nv(&d_inlineNv),
-    d_nm(nm),
-    d_nvMaxChildren(nchild_thresh) {
+  friend std::ostream& operator<<(std::ostream& out, const NodeBuilder& nb);
 
-    d_inlineNv.d_id = 0;
-    d_inlineNv.d_rc = 0;
-    d_inlineNv.d_kind = expr::NodeValue::kindToDKind(kind::UNDEFINED_KIND);
-    d_inlineNv.d_nchildren = 0;
-  }
-
-  inline NodeBuilder(NodeManager* nm, Kind k) :
-    d_nv(&d_inlineNv),
-    d_nm(nm),
-    d_nvMaxChildren(nchild_thresh) {
-    Assert(k != kind::NULL_EXPR && k != kind::UNDEFINED_KIND)
-        << "illegal Node-building kind";
-
-    d_inlineNv.d_id = 1; // have a kind already
-    d_inlineNv.d_rc = 0;
-    d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k);
-    d_inlineNv.d_nchildren = 0;
-  }
-
-  inline ~NodeBuilder() {
-    if(__builtin_expect( ( nvIsAllocated() ), false )) {
-      dealloc();
-    } else if(__builtin_expect( ( !isUsed() ), false )) {
-      decrRefCounts();
-    }
-  }
+  constexpr static size_t default_nchild_thresh = 10;
 
-  // These implementations are identical, but we need to have both of
-  // these because the templatized version isn't recognized as a
-  // generalization of a copy constructor (and a default copy
-  // constructor will be generated [?])
-  inline NodeBuilder(const NodeBuilder& nb) :
-    d_nv(&d_inlineNv),
-    d_nm(nb.d_nm),
-    d_nvMaxChildren(nchild_thresh) {
+ public:
+  NodeBuilder();
+  NodeBuilder(Kind k);
+  NodeBuilder(NodeManager* nm);
+  NodeBuilder(NodeManager* nm, Kind k);
+  NodeBuilder(const NodeBuilder& nb);
 
-    d_inlineNv.d_id = nb.d_nv->d_id;
-    d_inlineNv.d_rc = 0;
-    d_inlineNv.d_kind = nb.d_nv->d_kind;
-    d_inlineNv.d_nchildren = 0;
-
-    internalCopy(nb);
-  }
-
-  // technically this is a conversion, not a copy
-  template <unsigned N>
-  inline NodeBuilder(const NodeBuilder<N>& nb) :
-    d_nv(&d_inlineNv),
-    d_nm(nb.d_nm),
-    d_nvMaxChildren(nchild_thresh) {
-
-    d_inlineNv.d_id = nb.d_nv->d_id;
-    d_inlineNv.d_rc = 0;
-    d_inlineNv.d_kind = nb.d_nv->d_kind;
-    d_inlineNv.d_nchildren = 0;
-
-    internalCopy(nb);
-  }
-
-  typedef expr::NodeValue::iterator< NodeTemplate<true>  > iterator;
-  typedef expr::NodeValue::iterator< NodeTemplate<true> > const_iterator;
-
-  /** Get the begin-const-iterator of this Node-under-construction. */
-  inline const_iterator begin() const {
-    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
-                         "attempt to access it after conversion";
-    Assert(getKind() != kind::UNDEFINED_KIND)
-        << "Iterators over NodeBuilder<> are undefined "
-           "until a Kind is set";
-    return d_nv->begin< NodeTemplate<true> >();
-  }
-
-  /** Get the end-const-iterator of this Node-under-construction. */
-  inline const_iterator end() const {
-    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
-                         "attempt to access it after conversion";
-    Assert(getKind() != kind::UNDEFINED_KIND)
-        << "Iterators over NodeBuilder<> are undefined "
-           "until a Kind is set";
-    return d_nv->end< NodeTemplate<true> >();
-  }
+  ~NodeBuilder();
 
   /** Get the kind of this Node-under-construction. */
-  inline Kind getKind() const {
-    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
-                         "attempt to access it after conversion";
-    return d_nv->getKind();
-  }
+  Kind getKind() const;
 
   /** Get the kind of this Node-under-construction. */
-  inline kind::MetaKind getMetaKind() const {
-    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
-                         "attempt to access it after conversion";
-    Assert(getKind() != kind::UNDEFINED_KIND)
-        << "The metakind of a NodeBuilder<> is undefined "
-           "until a Kind is set";
-    return d_nv->getMetaKind();
-  }
+  kind::MetaKind getMetaKind() const;
 
   /** Get the current number of children of this Node-under-construction. */
-  inline unsigned getNumChildren() const {
-    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
-                         "attempt to access it after conversion";
-    Assert(getKind() != kind::UNDEFINED_KIND)
-        << "The number of children of a NodeBuilder<> is undefined "
-           "until a Kind is set";
-    return d_nv->getNumChildren();
-  }
+  unsigned getNumChildren() const;
 
   /**
    * Access to the operator of this Node-under-construction.  Only
    * allowed if this NodeBuilder is unused, and has a defined kind
    * that is of PARAMETERIZED metakind.
    */
-  inline Node getOperator() const {
-    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
-                         "attempt to access it after conversion";
-    Assert(getKind() != kind::UNDEFINED_KIND)
-        << "NodeBuilder<> operator access is not permitted "
-           "until a Kind is set";
-    Assert(getMetaKind() == kind::metakind::PARAMETERIZED)
-        << "NodeBuilder<> operator access is only permitted "
-           "on parameterized kinds, not `"
-        << getKind() << "'";
-    return Node(d_nv->getOperator());
-  }
+  Node getOperator() const;
 
   /**
    * Access to children of this Node-under-construction.  Only allowed
    * if this NodeBuilder is unused and has a defined kind.
    */
-  inline Node getChild(int i) const {
-    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
-                         "attempt to access it after conversion";
-    Assert(getKind() != kind::UNDEFINED_KIND)
-        << "NodeBuilder<> child access is not permitted "
-           "until a Kind is set";
-    Assert(i >= 0 && unsigned(i) < d_nv->getNumChildren())
-        << "index out of range for NodeBuilder::getChild()";
-    return Node(d_nv->getChild(i));
-  }
+  Node getChild(int i) const;
 
   /** Access to children of this Node-under-construction. */
-  inline Node operator[](int i) const {
-    return getChild(i);
-  }
+  Node operator[](int i) const;
 
   /**
    * "Reset" this node builder (optionally setting a new kind for it),
@@ -555,82 +212,28 @@ public:
   // "Stream" expression constructor syntax
 
   /** Set the Kind of this Node-under-construction. */
-  inline NodeBuilder<nchild_thresh>& operator<<(const Kind& k) {
-    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
-                         "attempt to access it after conversion";
-    Assert(getKind() == kind::UNDEFINED_KIND || d_nv->d_id == 0)
-        << "can't redefine the Kind of a NodeBuilder";
-    Assert(d_nv->d_id == 0)
-        << "internal inconsistency with NodeBuilder: d_id != 0";
-    AssertArgument(k != kind::UNDEFINED_KIND &&
-                   k != kind::NULL_EXPR &&
-                   k < kind::LAST_KIND,
-                   k, "illegal node-building kind");
-    // This test means: we didn't have a Kind at the beginning (on
-    // NodeBuilder construction or at the last clear()), but we do
-    // now.  That means we appended a Kind with operator<<(Kind),
-    // which now (lazily) we'll collapse.
-    if(__builtin_expect( ( d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND ), false )) {
-      Node n2 = operator Node();
-      clear();
-      append(n2);
-    } else if(d_nv->d_nchildren == 0) {
-      d_nv->d_id = 1; // remember that we had a kind from the start
-    }
-    d_nv->d_kind = expr::NodeValue::kindToDKind(k);
-    return *this;
-  }
+  NodeBuilder& operator<<(const Kind& k);
 
   /**
    * If this Node-under-construction has a Kind set, collapse it and
    * append the given Node as a child.  Otherwise, simply append.
    */
-  NodeBuilder<nchild_thresh>& operator<<(TNode n) {
-    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
-                         "attempt to access it after conversion";
-    // This test means: we didn't have a Kind at the beginning (on
-    // NodeBuilder construction or at the last clear()), but we do
-    // now.  That means we appended a Kind with operator<<(Kind),
-    // which now (lazily) we'll collapse.
-    if(__builtin_expect( ( d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND ), false )) {
-      Node n2 = operator Node();
-      clear();
-      append(n2);
-    }
-    return append(n);
-  }
+  NodeBuilder& operator<<(TNode n);
 
   /**
    * If this Node-under-construction has a Kind set, collapse it and
    * append the given Node as a child.  Otherwise, simply append.
    */
-  NodeBuilder<nchild_thresh>& operator<<(TypeNode n) {
-    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
-                         "attempt to access it after conversion";
-    // This test means: we didn't have a Kind at the beginning (on
-    // NodeBuilder construction or at the last clear()), but we do
-    // now.  That means we appended a Kind with operator<<(Kind),
-    // which now (lazily) we'll collapse.
-    if(__builtin_expect( ( d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND ), false )) {
-      Node n2 = operator Node();
-      clear();
-      append(n2);
-    }
-    return append(n);
-  }
+  NodeBuilder& operator<<(TypeNode n);
 
   /** Append a sequence of children to this TypeNode-under-construction. */
-  inline NodeBuilder<nchild_thresh>&
-  append(const std::vector<TypeNode>& children) {
-    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
-                         "attempt to access it after conversion";
-    return append(children.begin(), children.end());
-  }
+  NodeBuilder& append(const std::vector<TypeNode>& children);
 
   /** Append a sequence of children to this Node-under-construction. */
   template <bool ref_count>
-  inline NodeBuilder<nchild_thresh>&
-  append(const std::vector<NodeTemplate<ref_count> >& children) {
+  inline NodeBuilder& append(
+      const std::vector<NodeTemplate<ref_count> >& children)
+  {
     Assert(!isUsed()) << "NodeBuilder is one-shot only; "
                          "attempt to access it after conversion";
     return append(children.begin(), children.end());
@@ -638,7 +241,8 @@ public:
 
   /** Append a sequence of children to this Node-under-construction. */
   template <class Iterator>
-  NodeBuilder<nchild_thresh>& append(const Iterator& begin, const Iterator& end) {
+  NodeBuilder& append(const Iterator& begin, const Iterator& end)
+  {
     Assert(!isUsed()) << "NodeBuilder is one-shot only; "
                          "attempt to access it after conversion";
     for(Iterator i = begin; i != end; ++i) {
@@ -648,681 +252,158 @@ public:
   }
 
   /** Append a child to this Node-under-construction. */
-  NodeBuilder<nchild_thresh>& append(TNode n) {
-    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
-                         "attempt to access it after conversion";
-    Assert(!n.isNull()) << "Cannot use NULL Node as a child of a Node";
-    if(n.getKind() == kind::BUILTIN) {
-      return *this << NodeManager::operatorToKind(n);
-    }
-    allocateNvIfNecessaryForAppend();
-    expr::NodeValue* nv = n.d_nv;
-    nv->inc();
-    d_nv->d_children[d_nv->d_nchildren++] = nv;
-    Assert(d_nv->d_nchildren <= d_nvMaxChildren);
-    return *this;
-  }
+  NodeBuilder& append(TNode n);
 
   /** Append a child to this Node-under-construction. */
-  NodeBuilder<nchild_thresh>& append(const TypeNode& typeNode) {
-    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
-                         "attempt to access it after conversion";
-    Assert(!typeNode.isNull()) << "Cannot use NULL Node as a child of a Node";
-    allocateNvIfNecessaryForAppend();
-    expr::NodeValue* nv = typeNode.d_nv;
-    nv->inc();
-    d_nv->d_children[d_nv->d_nchildren++] = nv;
-    Assert(d_nv->d_nchildren <= d_nvMaxChildren);
-    return *this;
-  }
-
-private:
-
-  /** Construct the node value out of the node builder */
-  expr::NodeValue* constructNV();
-  expr::NodeValue* constructNV() const;
-
-#ifdef CVC4_DEBUG
-  // Throws a TypeCheckingExceptionPrivate on a failure.
-  void maybeCheckType(const TNode n) const;
-#else /* CVC4_DEBUG */
-  // Do nothing if not in debug mode.
-  inline void maybeCheckType(const TNode n) const {}
-#endif /* CVC4_DEBUG */
-
-public:
+  NodeBuilder& append(const TypeNode& typeNode);
 
   /** Construct the Node out of the node builder */
   Node constructNode();
-  Node constructNode() const;
 
   /** Construct a Node on the heap out of the node builder */
   Node* constructNodePtr();
-  Node* constructNodePtr() const;
 
   /** Construction of the TypeNode out of the node builder */
   TypeNode constructTypeNode();
-  TypeNode constructTypeNode() const;
 
   // two versions, so we can support extraction from (const)
   // NodeBuilders which are temporaries appearing as rvalues
   operator Node();
-  operator Node() const;
 
   // similarly for TypeNode
   operator TypeNode();
-  operator TypeNode() const;
-
-  NodeBuilder<nchild_thresh>& operator&=(TNode);
-  NodeBuilder<nchild_thresh>& operator|=(TNode);
-  NodeBuilder<nchild_thresh>& operator+=(TNode);
-  NodeBuilder<nchild_thresh>& operator-=(TNode);
-  NodeBuilder<nchild_thresh>& operator*=(TNode);
-
-  // This is needed for copy constructors of different sizes to access
-  // private fields
-  template <unsigned N>
-  friend class NodeBuilder;
-
-  template <unsigned N>
-  friend std::ostream& operator<<(std::ostream& out, const NodeBuilder<N>& nb);
-
-};/* class NodeBuilder<> */
-
-}  // namespace cvc5
-
-// TODO: add templatized NodeTemplate<ref_count> to all above and
-// below inlines for 'const [T]Node&' arguments?  Technically a lot of
-// time is spent in the TNode conversion and copy constructor, but
-// this should be optimized into a simple pointer copy (?)
-// TODO: double-check this.
-
-#include "expr/node.h"
-#include "expr/node_manager.h"
-#include "options/expr_options.h"
-
-namespace cvc5 {
-
-template <unsigned nchild_thresh>
-void NodeBuilder<nchild_thresh>::clear(Kind k) {
-  Assert(k != kind::NULL_EXPR) << "illegal Node-building clear kind";
-
-  if(__builtin_expect( ( nvIsAllocated() ), false )) {
-    dealloc();
-  } else if(__builtin_expect( ( !isUsed() ), false )) {
-    decrRefCounts();
-  } else {
-    setUnused();
-  }
-
-  d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k);
-  for(expr::NodeValue::nv_iterator i = d_inlineNv.nv_begin();
-      i != d_inlineNv.nv_end();
-      ++i) {
-    (*i)->dec();
-  }
-  d_inlineNv.d_nchildren = 0;
-  // keep track of whether or not we hvae a kind already
-  d_inlineNv.d_id = (k == kind::UNDEFINED_KIND) ? 0 : 1;
-}
-
-template <unsigned nchild_thresh>
-void NodeBuilder<nchild_thresh>::realloc(size_t toSize) {
-  AlwaysAssert(toSize > d_nvMaxChildren)
-      << "attempt to realloc() a NodeBuilder to a smaller/equal size!";
-  Assert(toSize < (static_cast<size_t>(1) << expr::NodeValue::NBITS_NCHILDREN))
-      << "attempt to realloc() a NodeBuilder to size " << toSize
-      << " (beyond hard limit of " << expr::NodeValue::MAX_CHILDREN << ")";
-
-  if(__builtin_expect( ( nvIsAllocated() ), false )) {
-    // Ensure d_nv is not modified on allocation failure
-    expr::NodeValue* newBlock = (expr::NodeValue*)
-      std::realloc(d_nv, sizeof(expr::NodeValue) +
-                   ( sizeof(expr::NodeValue*) * toSize ));
-    if(newBlock == NULL) {
-      // In this case, d_nv was NOT freed.  If we throw, the
-      // deallocation should occur on destruction of the NodeBuilder.
-      throw std::bad_alloc();
-    }
-    d_nvMaxChildren = toSize;
-    Assert(d_nvMaxChildren == toSize);  // overflow check
-    // Here, the copy (between two heap-allocated buffers) has already
-    // been done for us by the std::realloc().
-    d_nv = newBlock;
-  } else {
-    // Ensure d_nv is not modified on allocation failure
-    expr::NodeValue* newBlock = (expr::NodeValue*)
-      std::malloc(sizeof(expr::NodeValue) +
-                  ( sizeof(expr::NodeValue*) * toSize ));
-    if(newBlock == NULL) {
-      throw std::bad_alloc();
-    }
-    d_nvMaxChildren = toSize;
-    Assert(d_nvMaxChildren == toSize);  // overflow check
-
-    d_nv = newBlock;
-    d_nv->d_id = d_inlineNv.d_id;
-    d_nv->d_rc = 0;
-    d_nv->d_kind = d_inlineNv.d_kind;
-    d_nv->d_nchildren = d_inlineNv.d_nchildren;
-
-    std::copy(d_inlineNv.d_children,
-              d_inlineNv.d_children + d_inlineNv.d_nchildren,
-              d_nv->d_children);
-
-    // ensure "inline" children don't get decremented in dtor
-    d_inlineNv.d_nchildren = 0;
-  }
-}
-
-template <unsigned nchild_thresh>
-void NodeBuilder<nchild_thresh>::dealloc() {
-  Assert(nvIsAllocated())
-      << "Internal error: NodeBuilder: dealloc() called without a "
-         "private NodeBuilder-allocated buffer";
-
-  for(expr::NodeValue::nv_iterator i = d_nv->nv_begin();
-      i != d_nv->nv_end();
-      ++i) {
-    (*i)->dec();
-  }
-
-  free(d_nv);
-  d_nv = &d_inlineNv;
-  d_nvMaxChildren = nchild_thresh;
-}
-
-template <unsigned nchild_thresh>
-void NodeBuilder<nchild_thresh>::decrRefCounts() {
-  Assert(!nvIsAllocated())
-      << "Internal error: NodeBuilder: decrRefCounts() called with a "
-         "private NodeBuilder-allocated buffer";
-
-  for(expr::NodeValue::nv_iterator i = d_inlineNv.nv_begin();
-      i != d_inlineNv.nv_end();
-      ++i) {
-    (*i)->dec();
-  }
-
-  d_inlineNv.d_nchildren = 0;
-}
-
-
-template <unsigned nchild_thresh>
-TypeNode NodeBuilder<nchild_thresh>::constructTypeNode() {
-  return TypeNode(constructNV());
-}
-
-template <unsigned nchild_thresh>
-TypeNode NodeBuilder<nchild_thresh>::constructTypeNode() const {
-  return TypeNode(constructNV());
-}
-
-template <unsigned nchild_thresh>
-Node NodeBuilder<nchild_thresh>::constructNode() {
-  Node n = Node(constructNV());
-  maybeCheckType(n);
-  return n;
-}
-
-template <unsigned nchild_thresh>
-Node NodeBuilder<nchild_thresh>::constructNode() const {
-  Node n = Node(constructNV());
-  maybeCheckType(n);
-  return n;
-}
-
-template <unsigned nchild_thresh>
-Node* NodeBuilder<nchild_thresh>::constructNodePtr() {
-  // maybeCheckType() can throw an exception. Make sure to call the destructor
-  // on the exception branch.
-  std::unique_ptr<Node> np(new Node(constructNV()));
-  maybeCheckType(*np.get());
-  return np.release();
-}
 
-template <unsigned nchild_thresh>
-Node* NodeBuilder<nchild_thresh>::constructNodePtr() const {
-  std::unique_ptr<Node> np(new Node(constructNV()));
-  maybeCheckType(*np.get());
-  return np.release();
-}
+ private:
+  void internalCopy(const NodeBuilder& nb);
 
-template <unsigned nchild_thresh>
-NodeBuilder<nchild_thresh>::operator Node() {
-  return constructNode();
-}
-
-template <unsigned nchild_thresh>
-NodeBuilder<nchild_thresh>::operator Node() const {
-  return constructNode();
-}
-
-template <unsigned nchild_thresh>
-NodeBuilder<nchild_thresh>::operator TypeNode() {
-  return constructTypeNode();
-}
-
-template <unsigned nchild_thresh>
-NodeBuilder<nchild_thresh>::operator TypeNode() const {
-  return constructTypeNode();
-}
-
-template <unsigned nchild_thresh>
-expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() {
-  Assert(!isUsed()) << "NodeBuilder is one-shot only; "
-                       "attempt to access it after conversion";
-  Assert(getKind() != kind::UNDEFINED_KIND)
-      << "Can't make an expression of an undefined kind!";
-
-  // NOTE: The comments in this function refer to the cases in the
-  // file comments at the top of this file.
-
-  // Case 0: If a VARIABLE
-  if(getMetaKind() == kind::metakind::VARIABLE || getMetaKind() == kind::metakind::NULLARY_OPERATOR) {
-    /* 0. If a VARIABLE, treat similarly to 1(b), except that we know
-     * there are no children (no reference counts to reason about),
-     * and we don't keep VARIABLE-kinded Nodes in the NodeManager
-     * pool. */
-
-    Assert(!nvIsAllocated())
-        << "internal NodeBuilder error: "
-           "VARIABLE-kinded NodeBuilder is heap-allocated !?";
-    Assert(d_inlineNv.d_nchildren == 0)
-        << "improperly-formed VARIABLE-kinded NodeBuilder: "
-           "no children permitted";
-
-    // we have to copy the inline NodeValue out
-    expr::NodeValue* nv = (expr::NodeValue*)
-      std::malloc(sizeof(expr::NodeValue));
-    if(nv == NULL) {
-      throw std::bad_alloc();
-    }
-    // there are no children, so we don't have to worry about
-    // reference counts in this case.
-    nv->d_nchildren = 0;
-    nv->d_kind = d_nv->d_kind;
-    nv->d_id = d_nm->next_id++;// FIXME multithreading
-    nv->d_rc = 0;
-    setUsed();
-    if(Debug.isOn("gc")) {
-      Debug("gc") << "creating node value " << nv
-                  << " [" << nv->d_id << "]: ";
-      nv->printAst(Debug("gc"));
-      Debug("gc") << std::endl;
-    }
-    return nv;
-  }
-
-  // check that there are the right # of children for this kind
-  Assert(getMetaKind() != kind::metakind::CONSTANT)
-      << "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds";
-  Assert(getNumChildren() >= kind::metakind::getMinArityForKind(getKind()))
-      << "Nodes with kind " << getKind() << " must have at least "
-      << kind::metakind::getMinArityForKind(getKind())
-      << " children (the one under "
-         "construction has "
-      << getNumChildren() << ")";
-  Assert(getNumChildren() <= kind::metakind::getMaxArityForKind(getKind()))
-      << "Nodes with kind " << getKind() << " must have at most "
-      << kind::metakind::getMaxArityForKind(getKind())
-      << " children (the one under "
-         "construction has "
-      << getNumChildren() << ")";
-
-  // Implementation differs depending on whether the NodeValue was
-  // malloc'ed or not and whether or not it's in the already-been-seen
-  // NodeManager pool of Nodes.  See implementation notes at the top
-  // of this file.
-
-  if(__builtin_expect( ( ! nvIsAllocated() ), true )) {
-    /** Case 1.  d_nv points to d_inlineNv: it is the backing store
-     ** allocated "inline" in this NodeBuilder. **/
-
-    // Lookup the expression value in the pool we already have
-    expr::NodeValue* poolNv = d_nm->poolLookup(&d_inlineNv);
-    // If something else is there, we reuse it
-    if(poolNv != NULL) {
-      /* Subcase (a): The Node under construction already exists in
-       * the NodeManager's pool. */
-
-      /* 1(a). Reference-counts for all children in d_inlineNv must be
-       * decremented, and the NodeBuilder must be marked as "used" and
-       * the number of children set to zero so that we don't decrement
-       * them again on destruction.  The existing NodeManager pool
-       * entry is returned.
-       */
-      decrRefCounts();
-      d_inlineNv.d_nchildren = 0;
-      setUsed();
-      return poolNv;
-    } else {
-      /* Subcase (b): The Node under construction is NOT already in
-       * the NodeManager's pool. */
-
-      /* 1(b). A new heap-allocated NodeValue must be constructed and
-       * all settings and children from d_inlineNv copied into it.
-       * This new NodeValue is put into the NodeManager's pool.  The
-       * NodeBuilder is marked as "used" and the number of children in
-       * d_inlineNv set to zero so that we don't decrement child
-       * reference counts on destruction (the child reference counts
-       * have been "taken over" by the new NodeValue).  We return a
-       * Node wrapper for this new NodeValue, which increments its
-       * reference count. */
-
-      // create the canonical expression value for this node
-      expr::NodeValue* nv = (expr::NodeValue*)
-        std::malloc(sizeof(expr::NodeValue) +
-                    ( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));
-      if(nv == NULL) {
-        throw std::bad_alloc();
-      }
-      nv->d_nchildren = d_inlineNv.d_nchildren;
-      nv->d_kind = d_inlineNv.d_kind;
-      nv->d_id = d_nm->next_id++;// FIXME multithreading
-      nv->d_rc = 0;
-
-      std::copy(d_inlineNv.d_children,
-                d_inlineNv.d_children + d_inlineNv.d_nchildren,
-                nv->d_children);
-
-      d_inlineNv.d_nchildren = 0;
-      setUsed();
-
-      //poolNv = nv;
-      d_nm->poolInsert(nv);
-      if(Debug.isOn("gc")) {
-        Debug("gc") << "creating node value " << nv
-                    << " [" << nv->d_id << "]: ";
-        nv->printAst(Debug("gc"));
-        Debug("gc") << std::endl;
-      }
-      return nv;
-    }
-  } else {
-    /** Case 2. d_nv does NOT point to d_inlineNv: it is a new, larger
-     ** buffer that was heap-allocated by this NodeBuilder. **/
-
-    // Lookup the expression value in the pool we already have (with insert)
-    expr::NodeValue* poolNv = d_nm->poolLookup(d_nv);
-    // If something else is there, we reuse it
-    if(poolNv != NULL) {
-      /* Subcase (a): The Node under construction already exists in
-       * the NodeManager's pool. */
-
-      /* 2(a). Reference-counts for all children in d_nv must be
-       * decremented.  The NodeBuilder is marked as "used" and the
-       * heap-allocated d_nv deleted.  d_nv is repointed to d_inlineNv
-       * so that destruction of the NodeBuilder doesn't cause any
-       * problems.  The existing NodeManager pool entry is
-       * returned. */
-
-      dealloc();
-      setUsed();
-      return poolNv;
-    } else {
-      /* Subcase (b) The Node under construction is NOT already in the
-       * NodeManager's pool. */
-
-      /* 2(b). The heap-allocated d_nv is "cropped" to the correct
-       * size (based on the number of children it _actually_ has).
-       * d_nv is repointed to d_inlineNv so that destruction of the
-       * NodeBuilder doesn't cause any problems, and the (old) value
-       * it had is placed into the NodeManager's pool and returned in
-       * a Node wrapper. */
-
-      crop();
-      expr::NodeValue* nv = d_nv;
-      nv->d_id = d_nm->next_id++;// FIXME multithreading
-      d_nv = &d_inlineNv;
-      d_nvMaxChildren = nchild_thresh;
-      setUsed();
-
-      //poolNv = nv;
-      d_nm->poolInsert(nv);
-      Debug("gc") << "creating node value " << nv
-                  << " [" << nv->d_id << "]: " << *nv << "\n";
-      return nv;
-    }
-  }
-}
-
-// CONST VERSION OF NODE EXTRACTOR
-template <unsigned nchild_thresh>
-expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const {
-  Assert(!isUsed()) << "NodeBuilder is one-shot only; "
-                       "attempt to access it after conversion";
-  Assert(getKind() != kind::UNDEFINED_KIND)
-      << "Can't make an expression of an undefined kind!";
-
-  // NOTE: The comments in this function refer to the cases in the
-  // file comments at the top of this file.
-
-  // Case 0: If a VARIABLE
-  if(getMetaKind() == kind::metakind::VARIABLE || getMetaKind() == kind::metakind::NULLARY_OPERATOR) {
-    /* 0. If a VARIABLE, treat similarly to 1(b), except that we know
-     * there are no children (no reference counts to reason about),
-     * and we don't keep VARIABLE-kinded Nodes in the NodeManager
-     * pool. */
-
-    Assert(!nvIsAllocated())
-        << "internal NodeBuilder error: "
-           "VARIABLE-kinded NodeBuilder is heap-allocated !?";
-    Assert(d_inlineNv.d_nchildren == 0)
-        << "improperly-formed VARIABLE-kinded NodeBuilder: "
-           "no children permitted";
-
-    // we have to copy the inline NodeValue out
-    expr::NodeValue* nv = (expr::NodeValue*)
-      std::malloc(sizeof(expr::NodeValue));
-    if(nv == NULL) {
-      throw std::bad_alloc();
-    }
-    // there are no children, so we don't have to worry about
-    // reference counts in this case.
-    nv->d_nchildren = 0;
-    nv->d_kind = d_nv->d_kind;
-    nv->d_id = d_nm->next_id++;// FIXME multithreading
-    nv->d_rc = 0;
-    Debug("gc") << "creating node value " << nv
-                << " [" << nv->d_id << "]: " << *nv << "\n";
-    return nv;
-  }
-
-  // check that there are the right # of children for this kind
-  Assert(getMetaKind() != kind::metakind::CONSTANT)
-      << "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds";
-  Assert(getNumChildren() >= kind::metakind::getMinArityForKind(getKind()))
-      << "Nodes with kind " << getKind() << " must have at least "
-      << kind::metakind::getMinArityForKind(getKind())
-      << " children (the one under "
-         "construction has "
-      << getNumChildren() << ")";
-  Assert(getNumChildren() <= kind::metakind::getMaxArityForKind(getKind()))
-      << "Nodes with kind " << getKind() << " must have at most "
-      << kind::metakind::getMaxArityForKind(getKind())
-      << " children (the one under "
-         "construction has "
-      << getNumChildren() << ")";
-
-#if 0
-  // if the kind is PARAMETERIZED, check that the operator is correctly-kinded
-  Assert(kind::metaKindOf(getKind()) != kind::metakind::PARAMETERIZED ||
-         NodeManager::operatorToKind(getOperator()) == getKind()) << 
-         "Attempted to construct a parameterized kind `"<< getKind() <<"' with "
-         "incorrectly-kinded operator `"<< getOperator().getKind() <<"'";
-#endif /* 0 */
-
-  // Implementation differs depending on whether the NodeValue was
-  // malloc'ed or not and whether or not it's in the already-been-seen
-  // NodeManager pool of Nodes.  See implementation notes at the top
-  // of this file.
-
-  if(__builtin_expect( ( ! nvIsAllocated() ), true )) {
-    /** Case 1.  d_nv points to d_inlineNv: it is the backing store
-     ** allocated "inline" in this NodeBuilder. **/
-
-    // Lookup the expression value in the pool we already have
-    expr::NodeValue* poolNv = d_nm->poolLookup(const_cast<expr::NodeValue*>(&d_inlineNv));
-    // If something else is there, we reuse it
-    if(poolNv != NULL) {
-      /* Subcase (a): The Node under construction already exists in
-       * the NodeManager's pool. */
-
-      /* 1(a). The existing NodeManager pool entry is returned; we
-       * leave child reference counts alone and get them at
-       * NodeBuilder destruction time. */
-
-      return poolNv;
-    } else {
-      /* Subcase (b): The Node under construction is NOT already in
-       * the NodeManager's pool. */
-
-      /* 1(b). A new heap-allocated NodeValue must be constructed and
-       * all settings and children from d_inlineNv copied into it.
-       * This new NodeValue is put into the NodeManager's pool.  The
-       * NodeBuilder cannot be marked as "used", so we increment all
-       * child reference counts (which will be decremented to match on
-       * destruction of the NodeBuilder).  We return a Node wrapper
-       * for this new NodeValue, which increments its reference
-       * count. */
-
-      // create the canonical expression value for this node
-      expr::NodeValue* nv = (expr::NodeValue*)
-        std::malloc(sizeof(expr::NodeValue) +
-                    ( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));
-      if(nv == NULL) {
-        throw std::bad_alloc();
-      }
-      nv->d_nchildren = d_inlineNv.d_nchildren;
-      nv->d_kind = d_inlineNv.d_kind;
-      nv->d_id = d_nm->next_id++;// FIXME multithreading
-      nv->d_rc = 0;
+  /**
+   * Returns whether or not this NodeBuilder has been "used"---i.e.,
+   * whether a Node has been extracted with operator Node().
+   * Internally, this state is represented by d_nv pointing to NULL.
+   */
+  bool isUsed() const;
 
-      std::copy(d_inlineNv.d_children,
-                d_inlineNv.d_children + d_inlineNv.d_nchildren,
-                nv->d_children);
+  /**
+   * Set this NodeBuilder to the `used' state.
+   */
+  void setUsed();
 
-      for(expr::NodeValue::nv_iterator i = nv->nv_begin();
-          i != nv->nv_end();
-          ++i) {
-        (*i)->inc();
-      }
+  /**
+   * Set this NodeBuilder to the `unused' state.  Should only be done
+   * from clear().
+   */
+  void setUnused();
 
-      //poolNv = nv;
-      d_nm->poolInsert(nv);
-      Debug("gc") << "creating node value " << nv
-                  << " [" << nv->d_id << "]: " << *nv << "\n";
-      return nv;
-    }
-  } else {
-    /** Case 2. d_nv does NOT point to d_inlineNv: it is a new, larger
-     ** buffer that was heap-allocated by this NodeBuilder. **/
+  /**
+   * Returns true if d_nv is *not* the "in-line" one (it was
+   * heap-allocated by this class).
+   */
+  bool nvIsAllocated() const;
 
-    // Lookup the expression value in the pool we already have (with insert)
-    expr::NodeValue* poolNv = d_nm->poolLookup(d_nv);
-    // If something else is there, we reuse it
-    if(poolNv != NULL) {
-      /* Subcase (a): The Node under construction already exists in
-       * the NodeManager's pool. */
+  /**
+   * Returns true if adding a child requires (re)allocation of d_nv
+   * first.
+   */
+  bool nvNeedsToBeAllocated() const;
 
-      /* 2(a). The existing NodeManager pool entry is returned; we
-       * leave child reference counts alone and get them at
-       * NodeBuilder destruction time. */
+  /**
+   * (Re)allocate d_nv using a default grow factor.  Ensure that child
+   * pointers are copied into the new buffer, and if the "inline"
+   * NodeValue is evacuated, make sure its children won't be
+   * double-decremented later (on destruction/clear).
+   */
+  void realloc();
 
-      return poolNv;
-    } else {
-      /* Subcase (b) The Node under construction is NOT already in the
-       * NodeManager's pool. */
+  /**
+   * (Re)allocate d_nv to a specific size.  Specify "copy" if the
+   * children should be copied; if they are, and if the "inline"
+   * NodeValue is evacuated, make sure its children won't be
+   * double-decremented later (on destruction/clear).
+   */
+  void realloc(size_t toSize);
 
-      /* 2(b). The heap-allocated d_nv cannot be "cropped" to the
-       * correct size; we create a copy, increment child reference
-       * counts, place this copy into the NodeManager pool, and return
-       * a Node wrapper around it.  The child reference counts will be
-       * decremented to match at NodeBuilder destruction time. */
+  /**
+   * If d_nv needs to be (re)allocated to add an additional child, do
+   * so using realloc(), which ensures child pointers are copied and
+   * that the reference counts of the "inline" NodeValue won't be
+   * double-decremented on destruction/clear.  Otherwise, do nothing.
+   */
+  void allocateNvIfNecessaryForAppend();
 
-      // create the canonical expression value for this node
-      expr::NodeValue* nv = (expr::NodeValue*)
-        std::malloc(sizeof(expr::NodeValue) +
-                    ( sizeof(expr::NodeValue*) * d_nv->d_nchildren ));
-      if(nv == NULL) {
-        throw std::bad_alloc();
-      }
-      nv->d_nchildren = d_nv->d_nchildren;
-      nv->d_kind = d_nv->d_kind;
-      nv->d_id = d_nm->next_id++;// FIXME multithreading
-      nv->d_rc = 0;
+  /**
+   * Deallocate a d_nv that was heap-allocated by this class during
+   * grow operations.  (Marks this NodeValue no longer allocated so
+   * that double-deallocations don't occur.)
+   *
+   * PRECONDITION: only call this when nvIsAllocated() == true.
+   * POSTCONDITION: !nvIsAllocated()
+   */
+  void dealloc();
 
-      std::copy(d_nv->d_children,
-                d_nv->d_children + d_nv->d_nchildren,
-                nv->d_children);
+  /**
+   * "Purge" the "inline" children.  Decrement all their reference
+   * counts and set the number of children to zero.
+   *
+   * PRECONDITION: only call this when nvIsAllocated() == false.
+   * POSTCONDITION: d_inlineNv.d_nchildren == 0.
+   */
+  void decrRefCounts();
 
-      for(expr::NodeValue::nv_iterator i = nv->nv_begin();
-          i != nv->nv_end();
-          ++i) {
-        (*i)->inc();
-      }
+  /**
+   * Trim d_nv down to the size it needs to be for the number of
+   * children it has.  Used when a Node is extracted from a
+   * NodeBuilder and we want the returned memory not to suffer from
+   * internal fragmentation.  If d_nv was not heap-allocated by this
+   * class, or is already the right size, this function does nothing.
+   *
+   * @throws bad_alloc if the reallocation fails
+   */
+  void crop();
 
-      //poolNv = nv;
-      d_nm->poolInsert(nv);
-      Debug("gc") << "creating node value " << nv
-                  << " [" << nv->d_id << "]: " << *nv << "\n";
-      return nv;
-    }
-  }
-}
+  /** Construct the node value out of the node builder */
+  expr::NodeValue* constructNV();
 
-template <unsigned nchild_thresh>
-template <unsigned N>
-void NodeBuilder<nchild_thresh>::internalCopy(const NodeBuilder<N>& nb) {
-  if(nb.isUsed()) {
-    setUsed();
-    return;
-  }
+#ifdef CVC4_DEBUG
+  // Throws a TypeCheckingExceptionPrivate on a failure.
+  void maybeCheckType(const TNode n) const;
+#else  /* CVC4_DEBUG */
+  // Do nothing if not in debug mode.
+  inline void maybeCheckType(const TNode n) const {}
+#endif /* CVC4_DEBUG */
 
-  bool realloced CVC4_UNUSED = false;
-  if(nb.d_nvMaxChildren > d_nvMaxChildren) {
-    realloced = true;
-    realloc(nb.d_nvMaxChildren);
-  }
+  // used by convenience node builders
+  NodeBuilder& collapseTo(Kind k);
 
-  Assert(nb.d_nvMaxChildren <= d_nvMaxChildren);
-  Assert(nb.d_nv->nv_end() >= nb.d_nv->nv_begin());
-  Assert((size_t)(nb.d_nv->nv_end() - nb.d_nv->nv_begin()) <= d_nvMaxChildren)
-      << "realloced:" << (realloced ? "true" : "false")
-      << ", d_nvMax:" << d_nvMaxChildren
-      << ", size:" << nb.d_nv->nv_end() - nb.d_nv->nv_begin()
-      << ", nc:" << nb.d_nv->getNumChildren();
-  std::copy(nb.d_nv->nv_begin(), nb.d_nv->nv_end(), d_nv->nv_begin());
+  /**
+   * An "in-line" stack-allocated buffer for use by the
+   * NodeBuilder.
+   */
+  expr::NodeValue d_inlineNv;
+  /**
+   * Space for the children of the node being constructed.  This is
+   * never accessed directly, but rather through
+   * d_inlineNv.d_children[i].
+   */
+  expr::NodeValue* d_inlineNvChildSpace[default_nchild_thresh];
 
-  d_nv->d_nchildren = nb.d_nv->d_nchildren;
+  /**
+   * A pointer to the "current" NodeValue buffer; either &d_inlineNv
+   * or a heap-allocated one if d_inlineNv wasn't big enough.
+   */
+  expr::NodeValue* d_nv;
 
-  for(expr::NodeValue::nv_iterator i = d_nv->nv_begin();
-      i != d_nv->nv_end();
-      ++i) {
-    (*i)->inc();
-  }
-}
+  /** The NodeManager at play */
+  NodeManager* d_nm;
 
-#ifdef CVC4_DEBUG
-template <unsigned nchild_thresh>
-inline void NodeBuilder<nchild_thresh>::maybeCheckType(const TNode n) const
-{
-  /* force an immediate type check, if early type checking is
-     enabled and the current node isn't a variable or constant */
-  kind::MetaKind mk = n.getMetaKind();
-  if (mk != kind::metakind::VARIABLE && mk != kind::metakind::NULLARY_OPERATOR
-      && mk != kind::metakind::CONSTANT)
-  {
-    d_nm->getType(n, true);
-  }
-}
-#endif /* CVC4_DEBUG */
+  /**
+   * The number of children allocated in d_nv.
+   */
+  uint32_t d_nvMaxChildren;
+}; /* class NodeBuilder */
 
-template <unsigned nchild_thresh>
-std::ostream& operator<<(std::ostream& out, const NodeBuilder<nchild_thresh>& nb) {
-  return out << *nb.d_nv;
-}
+// Sometimes it's useful for debugging to output a NodeBuilder that
+// isn't yet a Node..
+std::ostream& operator<<(std::ostream& out, const NodeBuilder& nb);
 
 }  // namespace cvc5
 
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 6d2d150f5..4b95e08df 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -504,7 +504,7 @@ TypeNode NodeManager::getType(TNode n, bool check)
 }
 
 Node NodeManager::mkSkolem(const std::string& prefix, const TypeNode& type, const std::string& comment, int flags) {
-  Node n = NodeBuilder<0>(this, kind::SKOLEM);
+  Node n = NodeBuilder(this, kind::SKOLEM);
   setAttribute(n, TypeAttr(), type);
   setAttribute(n, TypeCheckedAttr(), true);
   if((flags & SKOLEM_EXACT_NAME) == 0) {
@@ -834,8 +834,8 @@ size_t NodeManager::poolSize() const{
 }
 
 TypeNode NodeManager::mkSort(uint32_t flags) {
-  NodeBuilder<1> nb(this, kind::SORT_TYPE);
-  Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
+  NodeBuilder nb(this, kind::SORT_TYPE);
+  Node sortTag = NodeBuilder(this, kind::SORT_TAG);
   nb << sortTag;
   TypeNode tn = nb.constructTypeNode();
   for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
@@ -845,8 +845,8 @@ TypeNode NodeManager::mkSort(uint32_t flags) {
 }
 
 TypeNode NodeManager::mkSort(const std::string& name, uint32_t flags) {
-  NodeBuilder<1> nb(this, kind::SORT_TYPE);
-  Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
+  NodeBuilder nb(this, kind::SORT_TYPE);
+  Node sortTag = NodeBuilder(this, kind::SORT_TAG);
   nb << sortTag;
   TypeNode tn = nb.constructTypeNode();
   setAttribute(tn, expr::VarNameAttr(), name);
@@ -870,7 +870,7 @@ TypeNode NodeManager::mkSort(TypeNode constructor,
   Assert(getAttribute(constructor.d_nv, expr::SortArityAttr())
          == children.size())
       << "arity mismatch in application of sort constructor";
-  NodeBuilder<> nb(this, kind::SORT_TYPE);
+  NodeBuilder nb(this, kind::SORT_TYPE);
   Node sortTag = Node(constructor.d_nv->d_children[0]);
   nb << sortTag;
   nb.append(children);
@@ -887,8 +887,8 @@ TypeNode NodeManager::mkSortConstructor(const std::string& name,
                                         uint32_t flags)
 {
   Assert(arity > 0);
-  NodeBuilder<> nb(this, kind::SORT_TYPE);
-  Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
+  NodeBuilder nb(this, kind::SORT_TYPE);
+  Node sortTag = NodeBuilder(this, kind::SORT_TAG);
   nb << sortTag;
   TypeNode type = nb.constructTypeNode();
   setAttribute(type, expr::VarNameAttr(), name);
@@ -901,7 +901,7 @@ TypeNode NodeManager::mkSortConstructor(const std::string& name,
 
 Node NodeManager::mkVar(const std::string& name, const TypeNode& type)
 {
-  Node n = NodeBuilder<0>(this, kind::VARIABLE);
+  Node n = NodeBuilder(this, kind::VARIABLE);
   setAttribute(n, TypeAttr(), type);
   setAttribute(n, TypeCheckedAttr(), true);
   setAttribute(n, expr::VarNameAttr(), name);
@@ -913,7 +913,7 @@ Node NodeManager::mkVar(const std::string& name, const TypeNode& type)
 
 Node* NodeManager::mkVarPtr(const std::string& name, const TypeNode& type)
 {
-  Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
+  Node* n = NodeBuilder(this, kind::VARIABLE).constructNodePtr();
   setAttribute(*n, TypeAttr(), type);
   setAttribute(*n, TypeCheckedAttr(), true);
   setAttribute(*n, expr::VarNameAttr(), name);
@@ -1044,7 +1044,7 @@ Node NodeManager::mkChain(Kind kind, const std::vector<Node>& children)
 
 Node NodeManager::mkVar(const TypeNode& type)
 {
-  Node n = NodeBuilder<0>(this, kind::VARIABLE);
+  Node n = NodeBuilder(this, kind::VARIABLE);
   setAttribute(n, TypeAttr(), type);
   setAttribute(n, TypeCheckedAttr(), true);
   for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
@@ -1055,7 +1055,7 @@ Node NodeManager::mkVar(const TypeNode& type)
 
 Node* NodeManager::mkVarPtr(const TypeNode& type)
 {
-  Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
+  Node* n = NodeBuilder(this, kind::VARIABLE).constructNodePtr();
   setAttribute(*n, TypeAttr(), type);
   setAttribute(*n, TypeCheckedAttr(), true);
   for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
@@ -1065,28 +1065,28 @@ Node* NodeManager::mkVarPtr(const TypeNode& type)
 }
 
 Node NodeManager::mkBoundVar(const TypeNode& type) {
-  Node n = NodeBuilder<0>(this, kind::BOUND_VARIABLE);
+  Node n = NodeBuilder(this, kind::BOUND_VARIABLE);
   setAttribute(n, TypeAttr(), type);
   setAttribute(n, TypeCheckedAttr(), true);
   return n;
 }
 
 Node* NodeManager::mkBoundVarPtr(const TypeNode& type) {
-  Node* n = NodeBuilder<0>(this, kind::BOUND_VARIABLE).constructNodePtr();
+  Node* n = NodeBuilder(this, kind::BOUND_VARIABLE).constructNodePtr();
   setAttribute(*n, TypeAttr(), type);
   setAttribute(*n, TypeCheckedAttr(), true);
   return n;
 }
 
 Node NodeManager::mkInstConstant(const TypeNode& type) {
-  Node n = NodeBuilder<0>(this, kind::INST_CONSTANT);
+  Node n = NodeBuilder(this, kind::INST_CONSTANT);
   n.setAttribute(TypeAttr(), type);
   n.setAttribute(TypeCheckedAttr(), true);
   return n;
 }
 
 Node NodeManager::mkBooleanTermVariable() {
-  Node n = NodeBuilder<0>(this, kind::BOOLEAN_TERM_VARIABLE);
+  Node n = NodeBuilder(this, kind::BOOLEAN_TERM_VARIABLE);
   n.setAttribute(TypeAttr(), booleanType());
   n.setAttribute(TypeCheckedAttr(), true);
   return n;
@@ -1095,7 +1095,7 @@ Node NodeManager::mkBooleanTermVariable() {
 Node NodeManager::mkNullaryOperator(const TypeNode& type, Kind k) {
   std::map< TypeNode, Node >::iterator it = d_unique_vars[k].find( type );
   if( it==d_unique_vars[k].end() ){
-    Node n = NodeBuilder<0>(this, k).constructNode();
+    Node n = NodeBuilder(this, k).constructNode();
     setAttribute(n, TypeAttr(), type);
     //setAttribute(n, TypeCheckedAttr(), true);
     d_unique_vars[k][type] = n;
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 857bcc25f..a72eada23 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -88,7 +88,6 @@ class NodeManager
   friend class expr::NodeValue;
   friend class expr::TypeChecker;
 
-  template <unsigned nchild_thresh>
   friend class NodeBuilder;
   friend class NodeManagerScope;
 
@@ -1239,67 +1238,67 @@ inline Kind NodeManager::operatorToKind(TNode n) {
 }
 
 inline Node NodeManager::mkNode(Kind kind, TNode child1) {
-  NodeBuilder<1> nb(this, kind);
+  NodeBuilder nb(this, kind);
   nb << child1;
   return nb.constructNode();
 }
 
 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1) {
-  NodeBuilder<1> nb(this, kind);
+  NodeBuilder nb(this, kind);
   nb << child1;
   return nb.constructNodePtr();
 }
 
 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2) {
-  NodeBuilder<2> nb(this, kind);
+  NodeBuilder nb(this, kind);
   nb << child1 << child2;
   return nb.constructNode();
 }
 
 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2) {
-  NodeBuilder<2> nb(this, kind);
+  NodeBuilder nb(this, kind);
   nb << child1 << child2;
   return nb.constructNodePtr();
 }
 
 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
                                 TNode child3) {
-  NodeBuilder<3> nb(this, kind);
+  NodeBuilder nb(this, kind);
   nb << child1 << child2 << child3;
   return nb.constructNode();
 }
 
 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
                                 TNode child3) {
-  NodeBuilder<3> nb(this, kind);
+  NodeBuilder nb(this, kind);
   nb << child1 << child2 << child3;
   return nb.constructNodePtr();
 }
 
 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
                                 TNode child3, TNode child4) {
-  NodeBuilder<4> nb(this, kind);
+  NodeBuilder nb(this, kind);
   nb << child1 << child2 << child3 << child4;
   return nb.constructNode();
 }
 
 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
                                 TNode child3, TNode child4) {
-  NodeBuilder<4> nb(this, kind);
+  NodeBuilder nb(this, kind);
   nb << child1 << child2 << child3 << child4;
   return nb.constructNodePtr();
 }
 
 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
                                 TNode child3, TNode child4, TNode child5) {
-  NodeBuilder<5> nb(this, kind);
+  NodeBuilder nb(this, kind);
   nb << child1 << child2 << child3 << child4 << child5;
   return nb.constructNode();
 }
 
 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
                                     TNode child3, TNode child4, TNode child5) {
-  NodeBuilder<5> nb(this, kind);
+  NodeBuilder nb(this, kind);
   nb << child1 << child2 << child3 << child4 << child5;
   return nb.constructNodePtr();
 }
@@ -1309,7 +1308,7 @@ template <bool ref_count>
 inline Node NodeManager::mkNode(Kind kind,
                                 const std::vector<NodeTemplate<ref_count> >&
                                 children) {
-  NodeBuilder<> nb(this, kind);
+  NodeBuilder nb(this, kind);
   nb.append(children);
   return nb.constructNode();
 }
@@ -1346,14 +1345,14 @@ template <bool ref_count>
 inline Node* NodeManager::mkNodePtr(Kind kind,
                                 const std::vector<NodeTemplate<ref_count> >&
                                 children) {
-  NodeBuilder<> nb(this, kind);
+  NodeBuilder nb(this, kind);
   nb.append(children);
   return nb.constructNodePtr();
 }
 
 // for operators
 inline Node NodeManager::mkNode(TNode opNode) {
-  NodeBuilder<1> nb(this, operatorToKind(opNode));
+  NodeBuilder nb(this, operatorToKind(opNode));
   if(opNode.getKind() != kind::BUILTIN) {
     nb << opNode;
   }
@@ -1361,7 +1360,7 @@ inline Node NodeManager::mkNode(TNode opNode) {
 }
 
 inline Node* NodeManager::mkNodePtr(TNode opNode) {
-  NodeBuilder<1> nb(this, operatorToKind(opNode));
+  NodeBuilder nb(this, operatorToKind(opNode));
   if(opNode.getKind() != kind::BUILTIN) {
     nb << opNode;
   }
@@ -1369,7 +1368,7 @@ inline Node* NodeManager::mkNodePtr(TNode opNode) {
 }
 
 inline Node NodeManager::mkNode(TNode opNode, TNode child1) {
-  NodeBuilder<2> nb(this, operatorToKind(opNode));
+  NodeBuilder nb(this, operatorToKind(opNode));
   if(opNode.getKind() != kind::BUILTIN) {
     nb << opNode;
   }
@@ -1378,7 +1377,7 @@ inline Node NodeManager::mkNode(TNode opNode, TNode child1) {
 }
 
 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1) {
-  NodeBuilder<2> nb(this, operatorToKind(opNode));
+  NodeBuilder nb(this, operatorToKind(opNode));
   if(opNode.getKind() != kind::BUILTIN) {
     nb << opNode;
   }
@@ -1387,7 +1386,7 @@ inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1) {
 }
 
 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2) {
-  NodeBuilder<3> nb(this, operatorToKind(opNode));
+  NodeBuilder nb(this, operatorToKind(opNode));
   if(opNode.getKind() != kind::BUILTIN) {
     nb << opNode;
   }
@@ -1396,7 +1395,7 @@ inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2) {
 }
 
 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2) {
-  NodeBuilder<3> nb(this, operatorToKind(opNode));
+  NodeBuilder nb(this, operatorToKind(opNode));
   if(opNode.getKind() != kind::BUILTIN) {
     nb << opNode;
   }
@@ -1406,7 +1405,7 @@ inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2) {
 
 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
                                 TNode child3) {
-  NodeBuilder<4> nb(this, operatorToKind(opNode));
+  NodeBuilder nb(this, operatorToKind(opNode));
   if(opNode.getKind() != kind::BUILTIN) {
     nb << opNode;
   }
@@ -1416,7 +1415,7 @@ inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
 
 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
                                 TNode child3) {
-  NodeBuilder<4> nb(this, operatorToKind(opNode));
+  NodeBuilder nb(this, operatorToKind(opNode));
   if(opNode.getKind() != kind::BUILTIN) {
     nb << opNode;
   }
@@ -1426,7 +1425,7 @@ inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
 
 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
                                 TNode child3, TNode child4) {
-  NodeBuilder<5> nb(this, operatorToKind(opNode));
+  NodeBuilder nb(this, operatorToKind(opNode));
   if(opNode.getKind() != kind::BUILTIN) {
     nb << opNode;
   }
@@ -1436,7 +1435,7 @@ inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
 
 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
                                 TNode child3, TNode child4) {
-  NodeBuilder<5> nb(this, operatorToKind(opNode));
+  NodeBuilder nb(this, operatorToKind(opNode));
   if(opNode.getKind() != kind::BUILTIN) {
     nb << opNode;
   }
@@ -1446,7 +1445,7 @@ inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
 
 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
                                 TNode child3, TNode child4, TNode child5) {
-  NodeBuilder<6> nb(this, operatorToKind(opNode));
+  NodeBuilder nb(this, operatorToKind(opNode));
   if(opNode.getKind() != kind::BUILTIN) {
     nb << opNode;
   }
@@ -1456,7 +1455,7 @@ inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
 
 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
                                     TNode child3, TNode child4, TNode child5) {
-  NodeBuilder<6> nb(this, operatorToKind(opNode));
+  NodeBuilder nb(this, operatorToKind(opNode));
   if(opNode.getKind() != kind::BUILTIN) {
     nb << opNode;
   }
@@ -1469,7 +1468,7 @@ template <bool ref_count>
 inline Node NodeManager::mkNode(TNode opNode,
                                 const std::vector<NodeTemplate<ref_count> >&
                                 children) {
-  NodeBuilder<> nb(this, operatorToKind(opNode));
+  NodeBuilder nb(this, operatorToKind(opNode));
   if(opNode.getKind() != kind::BUILTIN) {
     nb << opNode;
   }
@@ -1481,7 +1480,7 @@ template <bool ref_count>
 inline Node* NodeManager::mkNodePtr(TNode opNode,
                                     const std::vector<NodeTemplate<ref_count> >&
                                     children) {
-  NodeBuilder<> nb(this, operatorToKind(opNode));
+  NodeBuilder nb(this, operatorToKind(opNode));
   if(opNode.getKind() != kind::BUILTIN) {
     nb << opNode;
   }
@@ -1491,23 +1490,24 @@ inline Node* NodeManager::mkNodePtr(TNode opNode,
 
 
 inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1) {
-  return (NodeBuilder<1>(this, kind) << child1).constructTypeNode();
+  return (NodeBuilder(this, kind) << child1).constructTypeNode();
 }
 
 inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1,
                                         TypeNode child2) {
-  return (NodeBuilder<2>(this, kind) << child1 << child2).constructTypeNode();
+  return (NodeBuilder(this, kind) << child1 << child2).constructTypeNode();
 }
 
 inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1,
                                         TypeNode child2, TypeNode child3) {
-  return (NodeBuilder<3>(this, kind) << child1 << child2 << child3).constructTypeNode();
+  return (NodeBuilder(this, kind) << child1 << child2 << child3)
+      .constructTypeNode();
 }
 
 // N-ary version for types
 inline TypeNode NodeManager::mkTypeNode(Kind kind,
                                         const std::vector<TypeNode>& children) {
-  return NodeBuilder<>(this, kind).append(children).constructTypeNode();
+  return NodeBuilder(this, kind).append(children).constructTypeNode();
 }
 
 template <class T>
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 3815ea5be..3f4b7602e 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -36,7 +36,7 @@ namespace cvc5 {
 
 template <bool ref_count> class NodeTemplate;
 class TypeNode;
-template <unsigned N> class NodeBuilder;
+class NodeBuilder;
 class NodeManager;
 
 namespace expr {
@@ -65,7 +65,6 @@ class NodeValue
   template <bool>
   friend class ::cvc5::NodeTemplate;
   friend class ::cvc5::TypeNode;
-  template <unsigned nchild_thresh>
   friend class ::cvc5::NodeBuilder;
   friend class ::cvc5::NodeManager;
 
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index cbade1220..2dafe40da 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -39,7 +39,7 @@ TypeNode TypeNode::substitute(const TypeNode& type,
   }
 
   // otherwise compute
-  NodeBuilder<> nb(getKind());
+  NodeBuilder nb(getKind());
   if(getMetaKind() == kind::metakind::PARAMETERIZED) {
     // push the operator
     nb << TypeNode(d_nv->d_children[0]);
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 98515be2a..f8cc5a44b 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -77,7 +77,6 @@ private:
 
   friend class NodeManager;
 
-  template <unsigned nchild_thresh>
   friend class NodeBuilder;
 
   /**
@@ -797,7 +796,7 @@ TypeNode TypeNode::substitute(Iterator1 typesBegin,
     cache[*this] = *this;
     return *this;
   } else {
-    NodeBuilder<> nb(getKind());
+    NodeBuilder nb(getKind());
     if(getMetaKind() == kind::metakind::PARAMETERIZED) {
       // push the operator
       nb << TypeNode(d_nv->d_children[0]);
diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp
index df8e93bc7..ac7707d16 100644
--- a/src/preprocessing/passes/bool_to_bv.cpp
+++ b/src/preprocessing/passes/bool_to_bv.cpp
@@ -356,7 +356,7 @@ void BoolToBV::rebuildNode(const TNode& n, Kind new_kind)
 {
   Kind k = n.getKind();
   NodeManager* nm = NodeManager::currentNM();
-  NodeBuilder<> builder(new_kind);
+  NodeBuilder builder(new_kind);
 
   Debug("bool-to-bv") << "BoolToBV::rebuildNode with " << n
                       << " and new_kind = " << kindToString(new_kind)
diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp
index 7bd0e7715..6b8b7af2f 100644
--- a/src/preprocessing/passes/bv_gauss.cpp
+++ b/src/preprocessing/passes/bv_gauss.cpp
@@ -500,8 +500,8 @@ BVGauss::Result BVGauss::gaussElimRewriteForUrem(
         /* Flatten mult expression. */
         n = RewriteRule<FlattenAssocCommut>::run<true>(n);
         /* Split operands into consts and non-consts */
-        NodeBuilder<> nb_consts(NodeManager::currentNM(), k);
-        NodeBuilder<> nb_nonconsts(NodeManager::currentNM(), k);
+        NodeBuilder nb_consts(NodeManager::currentNM(), k);
+        NodeBuilder nb_nonconsts(NodeManager::currentNM(), k);
         for (const Node& nn : n)
         {
           Node nnrw = Rewriter::rewrite(nn);
diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp
index 9f219e7a4..a8382974c 100644
--- a/src/preprocessing/passes/bv_to_bool.cpp
+++ b/src/preprocessing/passes/bv_to_bool.cpp
@@ -220,7 +220,7 @@ Node BVToBool::convertBvTerm(TNode node)
     default: Unhandled();
   }
 
-  NodeBuilder<> builder(new_kind);
+  NodeBuilder builder(new_kind);
   for (unsigned i = 0; i < node.getNumChildren(); ++i)
   {
     builder << convertBvTerm(node[i]);
@@ -254,7 +254,7 @@ Node BVToBool::liftNode(TNode current)
     }
     else
     {
-      NodeBuilder<> builder(current.getKind());
+      NodeBuilder builder(current.getKind());
       if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
       {
         builder << current.getOperator();
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index 510d35419..c5f24c15c 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -116,7 +116,7 @@ Node BVToInt::makeBinary(Node n)
     else if (numChildren > 0)
     {
       // current has children, but we do not binarize it
-      NodeBuilder<> builder(k);
+      NodeBuilder builder(k);
       if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
       {
         builder << current.getOperator();
@@ -220,7 +220,7 @@ Node BVToInt::eliminationPass(Node n)
         {
           // The main operator is replaced, and the children
           // are replaced with their eliminated counterparts.
-          NodeBuilder<> builder(current.getKind());
+          NodeBuilder builder(current.getKind());
           if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
           {
             builder << current.getOperator();
@@ -886,7 +886,7 @@ Node BVToInt::reconstructNode(Node originalNode,
   // first, we adjust the children of the node as needed.
   // re-construct the term with the adjusted children.
   kind::Kind_t oldKind = originalNode.getKind();
-  NodeBuilder<> builder(oldKind);
+  NodeBuilder builder(oldKind);
   if (originalNode.getMetaKind() == kind::metakind::PARAMETERIZED)
   {
     builder << originalNode.getOperator();
diff --git a/src/preprocessing/passes/foreign_theory_rewrite.cpp b/src/preprocessing/passes/foreign_theory_rewrite.cpp
index 307be46bf..60345992f 100644
--- a/src/preprocessing/passes/foreign_theory_rewrite.cpp
+++ b/src/preprocessing/passes/foreign_theory_rewrite.cpp
@@ -121,7 +121,7 @@ Node ForeignTheoryRewrite::reconstructNode(Node originalNode,
   }
   // re-build the node with the same kind and new children
   kind::Kind_t k = originalNode.getKind();
-  NodeBuilder<> builder(k);
+  NodeBuilder builder(k);
   // special case for parameterized nodes
   if (originalNode.getMetaKind() == kind::metakind::PARAMETERIZED)
   {
diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
index b1f8ad771..ef9b261b0 100644
--- a/src/preprocessing/passes/int_to_bv.cpp
+++ b/src/preprocessing/passes/int_to_bv.cpp
@@ -79,7 +79,7 @@ Node intToBVMakeBinary(TNode n, NodeMap& cache)
     }
     else
     {
-      NodeBuilder<> builder(current.getKind());
+      NodeBuilder builder(current.getKind());
       if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
         builder << current.getOperator();
       }
@@ -186,7 +186,7 @@ Node intToBV(TNode n, NodeMap& cache)
           }
         }
       }
-      NodeBuilder<> builder(newKind);
+      NodeBuilder builder(newKind);
       if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
         builder << current.getOperator();
       }
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index 7c246c3e1..f3c4d2e12 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -57,7 +57,7 @@ size_t removeFromConjunction(Node& n,
         || (sub.getKind() == kind::AND
             && (subremovals = removeFromConjunction(sub, toRemove)) > 0))
     {
-      NodeBuilder<> b(kind::AND);
+      NodeBuilder b(kind::AND);
       b.append(n.begin(), j);
       if (subremovals > 0)
       {
@@ -559,7 +559,7 @@ PreprocessingPassResult MipLibTrick::applyInternal(
           Node sum;
           if (pos.getKind() == kind::AND)
           {
-            NodeBuilder<> sumb(kind::PLUS);
+            NodeBuilder sumb(kind::PLUS);
             for (size_t jj = 0; jj < pos.getNumChildren(); ++jj)
             {
               sumb << nm->mkNode(
diff --git a/src/preprocessing/passes/static_learning.cpp b/src/preprocessing/passes/static_learning.cpp
index 028322c1e..5e572d1d8 100644
--- a/src/preprocessing/passes/static_learning.cpp
+++ b/src/preprocessing/passes/static_learning.cpp
@@ -37,7 +37,7 @@ PreprocessingPassResult StaticLearning::applyInternal(
 
   for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
   {
-    NodeBuilder<> learned(kind::AND);
+    NodeBuilder learned(kind::AND);
     learned << (*assertionsToPreprocess)[i];
     d_preprocContext->getTheoryEngine()->ppStaticLearn(
         (*assertionsToPreprocess)[i], learned);
diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp
index a3ad701a8..7826c207b 100644
--- a/src/preprocessing/util/ite_utilities.cpp
+++ b/src/preprocessing/util/ite_utilities.cpp
@@ -401,7 +401,7 @@ Node ITECompressor::compressBooleanITEs(Node toCompress)
     }
   }
 
-  NodeBuilder<> nb(kind::AND);
+  NodeBuilder nb(kind::AND);
   Node curr = toCompress;
   while (curr.getKind() == kind::ITE
          && (curr[1] == d_false || curr[2] == d_false)
@@ -465,7 +465,7 @@ Node ITECompressor::compressTerm(Node toCompress)
     }
   }
 
-  NodeBuilder<> nb(toCompress.getKind());
+  NodeBuilder nb(toCompress.getKind());
 
   if (toCompress.getMetaKind() == kind::metakind::PARAMETERIZED)
   {
@@ -504,7 +504,7 @@ Node ITECompressor::compressBoolean(Node toCompress)
   else
   {
     bool ta = ite::isTheoryAtom(toCompress);
-    NodeBuilder<> nb(toCompress.getKind());
+    NodeBuilder nb(toCompress.getKind());
     if (toCompress.getMetaKind() == kind::metakind::PARAMETERIZED)
     {
       nb << (toCompress.getOperator());
@@ -906,7 +906,7 @@ Node ITESimplifier::replaceOver(Node n, Node replaceWith, Node simpVar)
     return d_replaceOverCache[p];
   }
 
-  NodeBuilder<> builder(n.getKind());
+  NodeBuilder builder(n.getKind());
   if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
   {
     builder << n.getOperator();
@@ -1207,7 +1207,7 @@ Node ITESimplifier::intersectConstantIte(TNode lcite, TNode rcite)
   }
   else
   {
-    NodeBuilder<> nb(kind::OR);
+    NodeBuilder nb(kind::OR);
     NodeVec::const_iterator it = intersection.begin(), end = intersection.end();
     for (; it != end; ++it)
     {
@@ -1332,7 +1332,7 @@ Node ITESimplifier::simpConstants(TNode simpContext,
 
   if (iteNode.getKind() == kind::ITE)
   {
-    NodeBuilder<> builder(kind::ITE);
+    NodeBuilder builder(kind::ITE);
     builder << iteNode[0];
     unsigned i = 1;
     for (; i < iteNode.getNumChildren(); ++i)
@@ -1428,7 +1428,7 @@ Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar)
     return simpVar;
   }
 
-  NodeBuilder<> builder(c.getKind());
+  NodeBuilder builder(c.getKind());
   if (c.getMetaKind() == kind::metakind::PARAMETERIZED)
   {
     builder << c.getOperator();
@@ -1584,7 +1584,7 @@ Node ITESimplifier::simpITE(TNode assertion)
     if (stackHead.d_children_added)
     {
       // Children have been processed, so substitute
-      NodeBuilder<> builder(current.getKind());
+      NodeBuilder builder(current.getKind());
       if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
       {
         builder << current.getOperator();
@@ -1731,7 +1731,7 @@ Node ITECareSimplifier::substitute(TNode e,
     return e;
   }
 
-  NodeBuilder<> builder(e.getKind());
+  NodeBuilder builder(e.getKind());
   if (e.getMetaKind() == kind::metakind::PARAMETERIZED)
   {
     builder << e.getOperator();
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 1caea7bb7..10c84f582 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -76,7 +76,7 @@ bool CnfStream::assertClause(TNode node, SatClause& c)
     else
     {
       Assert(c.size() > 1);
-      NodeBuilder<> b(kind::OR);
+      NodeBuilder b(kind::OR);
       for (unsigned i = 0; i < c.size(); ++i)
       {
         b << getNode(c[i]);
diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index 07d072751..bfb14e2c4 100644
--- a/src/smt/assertions.cpp
+++ b/src/smt/assertions.cpp
@@ -18,6 +18,7 @@
 
 #include "expr/node_algorithm.h"
 #include "options/base_options.h"
+#include "options/expr_options.h"
 #include "options/language.h"
 #include "options/smt_options.h"
 #include "proof/proof_manager.h"
diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp
index e00ed907f..c1daf9879 100644
--- a/src/smt/dump.cpp
+++ b/src/smt/dump.cpp
@@ -19,6 +19,7 @@
 #include "base/configuration.h"
 #include "base/output.h"
 #include "lib/strtok_r.h"
+#include "options/option_exception.h"
 #include "preprocessing/preprocessing_pass_registry.h"
 #include "smt/command.h"
 #include "smt/node_command.h"
diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp
index 85a2732c9..59597b97f 100644
--- a/src/smt/expand_definitions.cpp
+++ b/src/smt/expand_definitions.cpp
@@ -294,7 +294,7 @@ TrustNode ExpandDefs::expandDefinitions(
       if (node.getNumChildren() > 0)
       {
         // cout << "cons : " << node << std::endl;
-        NodeBuilder<> nb(node.getKind());
+        NodeBuilder nb(node.getKind());
         if (node.getMetaKind() == metakind::PARAMETERIZED)
         {
           Debug("expand") << "op   : " << node.getOperator() << std::endl;
diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index 9f1f71bd7..28f393704 100644
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -14,6 +14,7 @@
 
 #include "smt/preprocessor.h"
 
+#include "options/expr_options.h"
 #include "options/smt_options.h"
 #include "preprocessing/preprocessing_pass_context.h"
 #include "printer/printer.h"
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d7c44fef3..a925c04ab 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -24,6 +24,7 @@
 #include "expr/bound_var_manager.h"
 #include "expr/node.h"
 #include "options/base_options.h"
+#include "options/expr_options.h"
 #include "options/language.h"
 #include "options/main_options.h"
 #include "options/printer_options.h"
diff --git a/src/smt_util/boolean_simplification.h b/src/smt_util/boolean_simplification.h
index de53e539c..495c2c16d 100644
--- a/src/smt_util/boolean_simplification.h
+++ b/src/smt_util/boolean_simplification.h
@@ -82,7 +82,7 @@ class BooleanSimplification {
       return buffer[0];
     }
 
-    NodeBuilder<> nb(kind::AND);
+    NodeBuilder nb(kind::AND);
     nb.append(buffer);
     return nb;
   }
@@ -108,7 +108,7 @@ class BooleanSimplification {
       return buffer[0];
     }
 
-    NodeBuilder<> nb(kind::OR);
+    NodeBuilder nb(kind::OR);
     nb.append(buffer);
     return nb;
   }
@@ -128,7 +128,7 @@ class BooleanSimplification {
     TNode right = implication[1];
 
     Node notLeft = negate(left);
-    Node clause = NodeBuilder<2>(kind::OR) << notLeft << right;
+    Node clause = NodeBuilder(kind::OR) << notLeft << right;
 
     return simplifyClause(clause);
   }
diff --git a/src/smt_util/nary_builder.cpp b/src/smt_util/nary_builder.cpp
index efff058c5..ef988318f 100644
--- a/src/smt_util/nary_builder.cpp
+++ b/src/smt_util/nary_builder.cpp
@@ -185,7 +185,7 @@ Node RePairAssocCommutativeOperators::case_other(TNode n){
     return n;
   }
 
-  NodeBuilder<> nb(n.getKind());
+  NodeBuilder nb(n.getKind());
 
   if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
     nb << n.getOperator();
diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index 8e75f6850..caa052065 100644
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -1785,7 +1785,7 @@ MipResult ApproxGLPK::solveMIP(bool activelyLog){
 
 // Node explainSet(const set<ConstraintP>& inp){
 //   Assert(!inp.empty());
-//   NodeBuilder<> nb(kind::AND);
+//   NodeBuilder nb(kind::AND);
 //   set<ConstraintP>::const_iterator iter, end;
 //   for(iter = inp.begin(), end = inp.end(); iter != end; ++iter){
 //     const ConstraintP c = *iter;
diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp
index 4c991dba3..218fdf179 100644
--- a/src/theory/arith/arith_ite_utils.cpp
+++ b/src/theory/arith/arith_ite_utils.cpp
@@ -35,7 +35,7 @@ namespace theory {
 namespace arith {
 
 Node ArithIteUtils::applyReduceVariablesInItes(Node n){
-  NodeBuilder<> nb(n.getKind());
+  NodeBuilder nb(n.getKind());
   if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
     nb << (n.getOperator());
   }
@@ -239,7 +239,7 @@ Node ArithIteUtils::reduceConstantIteByGCD(Node n){
   }
 
   if(n.getNumChildren() > 0){
-    NodeBuilder<> nb(n.getKind());
+    NodeBuilder nb(n.getKind());
     if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
       nb << (n.getOperator());
     }
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 87aba7b45..452200796 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -235,7 +235,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
               if( num==1 ){
                 return RewriteResponse(REWRITE_AGAIN, base);
               }else{
-                NodeBuilder<> nb(kind::MULT);
+                NodeBuilder nb(kind::MULT);
                 for(unsigned i=0; i < num; ++i){
                   nb << base;
                 }
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index 9c764ac7a..ce54133c5 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -57,8 +57,8 @@ ArithStaticLearner::Statistics::~Statistics(){
   smtStatisticsRegistry()->unregisterStat(&d_iteConstantApplications);
 }
 
-void ArithStaticLearner::staticLearning(TNode n, NodeBuilder<>& learned){
-
+void ArithStaticLearner::staticLearning(TNode n, NodeBuilder& learned)
+{
   vector<TNode> workList;
   workList.push_back(n);
   TNodeSet processed;
@@ -101,8 +101,10 @@ void ArithStaticLearner::staticLearning(TNode n, NodeBuilder<>& learned){
   }
 }
 
-
-void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet& defTrue){
+void ArithStaticLearner::process(TNode n,
+                                 NodeBuilder& learned,
+                                 const TNodeSet& defTrue)
+{
   Debug("arith::static") << "===================== looking at " << n << endl;
 
   switch(n.getKind()){
@@ -136,7 +138,8 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet
   }
 }
 
-void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){
+void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder& learned)
+{
   Assert(n.getKind() == kind::ITE);
   Assert(n[0].getKind() != EQUAL);
   Assert(isRelationOperator(n[0].getKind()));
@@ -167,8 +170,8 @@ void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){
     switch(k){
     case LT:   // (ite (< x y) x y)
     case LEQ: { // (ite (<= x y) x y)
-      Node nLeqX = NodeBuilder<2>(LEQ) << n << t;
-      Node nLeqY = NodeBuilder<2>(LEQ) << n << e;
+      Node nLeqX = NodeBuilder(LEQ) << n << t;
+      Node nLeqY = NodeBuilder(LEQ) << n << e;
       Debug("arith::static") << n << "is a min =>"  << nLeqX << nLeqY << endl;
       learned << nLeqX << nLeqY;
       ++(d_statistics.d_iteMinMaxApplications);
@@ -176,8 +179,8 @@ void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){
     }
     case GT: // (ite (> x y) x y)
     case GEQ: { // (ite (>= x y) x y)
-      Node nGeqX = NodeBuilder<2>(GEQ) << n << t;
-      Node nGeqY = NodeBuilder<2>(GEQ) << n << e;
+      Node nGeqX = NodeBuilder(GEQ) << n << t;
+      Node nGeqY = NodeBuilder(GEQ) << n << e;
       Debug("arith::static") << n << "is a max =>"  << nGeqX << nGeqY << endl;
       learned << nGeqX << nGeqY;
       ++(d_statistics.d_iteMinMaxApplications);
@@ -188,7 +191,8 @@ void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){
   }
 }
 
-void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){
+void ArithStaticLearner::iteConstant(TNode n, NodeBuilder& learned)
+{
   Assert(n.getKind() == ITE);
 
   Debug("arith::static") << "iteConstant(" << n << ")" << endl;
@@ -202,9 +206,11 @@ void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){
       d_minMap.insert(n, min);
       Node nGeqMin;
       if (min.getInfinitesimalPart() == 0) {
-        nGeqMin = NodeBuilder<2>(kind::GEQ) << n << mkRationalNode(min.getNoninfinitesimalPart());
+        nGeqMin = NodeBuilder(kind::GEQ)
+                  << n << mkRationalNode(min.getNoninfinitesimalPart());
       } else {
-        nGeqMin = NodeBuilder<2>(kind::GT) << n << mkRationalNode(min.getNoninfinitesimalPart());
+        nGeqMin = NodeBuilder(kind::GT)
+                  << n << mkRationalNode(min.getNoninfinitesimalPart());
       }
       learned << nGeqMin;
       Debug("arith::static") << n << " iteConstant"  << nGeqMin << endl;
@@ -221,9 +227,11 @@ void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){
       d_maxMap.insert(n, max);
       Node nLeqMax;
       if (max.getInfinitesimalPart() == 0) {
-        nLeqMax = NodeBuilder<2>(kind::LEQ) << n << mkRationalNode(max.getNoninfinitesimalPart());
+        nLeqMax = NodeBuilder(kind::LEQ)
+                  << n << mkRationalNode(max.getNoninfinitesimalPart());
       } else {
-        nLeqMax = NodeBuilder<2>(kind::LT) << n << mkRationalNode(max.getNoninfinitesimalPart());
+        nLeqMax = NodeBuilder(kind::LT)
+                  << n << mkRationalNode(max.getNoninfinitesimalPart());
       }
       learned << nLeqMax;
       Debug("arith::static") << n << " iteConstant"  << nLeqMax << endl;
diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h
index 73810dedd..b96d7a86a 100644
--- a/src/theory/arith/arith_static_learner.h
+++ b/src/theory/arith/arith_static_learner.h
@@ -45,19 +45,22 @@ private:
 public:
   ArithStaticLearner(context::Context* userContext);
   ~ArithStaticLearner();
-  void staticLearning(TNode n, NodeBuilder<>& learned);
+  void staticLearning(TNode n, NodeBuilder& learned);
 
   void addBound(TNode n);
 
-private:
-  void process(TNode n, NodeBuilder<>& learned, const TNodeSet& defTrue);
+ private:
+  void process(TNode n, NodeBuilder& learned, const TNodeSet& defTrue);
 
-  void iteMinMax(TNode n, NodeBuilder<>& learned);
-  void iteConstant(TNode n, NodeBuilder<>& learned);
+  void iteMinMax(TNode n, NodeBuilder& learned);
+  void iteConstant(TNode n, NodeBuilder& learned);
 
-  /** These fields are designed to be accessible to ArithStaticLearner methods. */
-  class Statistics {
-  public:
+  /**
+   * These fields are designed to be accessible to ArithStaticLearner methods.
+   */
+  class Statistics
+  {
+   public:
     IntStat d_iteMinMaxApplications;
     IntStat d_iteConstantApplications;
 
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 852550917..bc35c6941 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -194,17 +194,18 @@ inline Kind negateKind(Kind k){
 
 inline Node negateConjunctionAsClause(TNode conjunction){
   Assert(conjunction.getKind() == kind::AND);
-  NodeBuilder<> orBuilder(kind::OR);
+  NodeBuilder orBuilder(kind::OR);
 
   for(TNode::iterator i = conjunction.begin(), end=conjunction.end(); i != end; ++i){
     TNode child = *i;
-    Node negatedChild = NodeBuilder<1>(kind::NOT)<<(child);
+    Node negatedChild = NodeBuilder(kind::NOT) << (child);
     orBuilder << negatedChild;
   }
   return orBuilder;
 }
 
-inline Node maybeUnaryConvert(NodeBuilder<>& builder){
+inline Node maybeUnaryConvert(NodeBuilder& builder)
+{
   Assert(builder.getKind() == kind::OR || builder.getKind() == kind::AND
          || builder.getKind() == kind::PLUS || builder.getKind() == kind::MULT);
   Assert(builder.getNumChildren() >= 1);
@@ -247,7 +248,8 @@ inline Node getIdentity(Kind k){
   }
 }
 
-inline Node safeConstructNary(NodeBuilder<>& nb) {
+inline Node safeConstructNary(NodeBuilder& nb)
+{
   switch (nb.getNumChildren()) {
     case 0:
       return getIdentity(nb.getKind());
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index ea597468d..43589fdce 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -223,7 +223,7 @@ void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP lb, ConstraintCP
   TNode eq = d_watchedEqualities[s];
   ConstraintCP eqC = d_constraintDatabase.getConstraint(
       s, ConstraintType::Equality, lb->getValue());
-  NodeBuilder<> reasonBuilder(Kind::AND);
+  NodeBuilder reasonBuilder(Kind::AND);
   auto pfLb = lb->externalExplainByAssertions(reasonBuilder);
   auto pfUb = ub->externalExplainByAssertions(reasonBuilder);
   Node reason = safeConstructNary(reasonBuilder);
@@ -256,7 +256,7 @@ void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP eq){
   //Explain for conflict is correct as these proofs are generated
   //and stored eagerly
   //These will be safe for propagation later as well
-  NodeBuilder<> nb(Kind::AND);
+  NodeBuilder nb(Kind::AND);
   // An open proof of eq from literals now in reason.
   if (Debug.isOn("arith::cong"))
   {
@@ -284,7 +284,7 @@ void ArithCongruenceManager::watchedVariableCannotBeZero(ConstraintCP c){
 
   //Explain for conflict is correct as these proofs are generated and stored eagerly
   //These will be safe for propagation later as well
-  NodeBuilder<> nb(Kind::AND);
+  NodeBuilder nb(Kind::AND);
   // An open proof of eq from literals now in reason.
   auto pf = c->externalExplainByAssertions(nb);
   if (Debug.isOn("arith::cong::notzero"))
@@ -456,7 +456,9 @@ void ArithCongruenceManager::explain(TNode literal, std::vector<TNode>& assumpti
   }
 }
 
-void ArithCongruenceManager::enqueueIntoNB(const std::set<TNode> s, NodeBuilder<>& nb){
+void ArithCongruenceManager::enqueueIntoNB(const std::set<TNode> s,
+                                           NodeBuilder& nb)
+{
   std::set<TNode>::const_iterator it = s.begin();
   std::set<TNode>::const_iterator it_end = s.end();
   for(; it != it_end; ++it) {
@@ -504,7 +506,8 @@ TrustNode ArithCongruenceManager::explain(TNode external)
   return trn;
 }
 
-void ArithCongruenceManager::explain(TNode external, NodeBuilder<>& out){
+void ArithCongruenceManager::explain(TNode external, NodeBuilder& out)
+{
   Node internal = externalToInternal(external);
 
   std::vector<TNode> assumptions;
@@ -627,7 +630,7 @@ void ArithCongruenceManager::equalsConstant(ConstraintCP c){
   Node eq = xAsNode.eqNode(asRational);
   d_keepAlive.push_back(eq);
 
-  NodeBuilder<> nb(Kind::AND);
+  NodeBuilder nb(Kind::AND);
   auto pf = c->externalExplainByAssertions(nb);
   Node reason = safeConstructNary(nb);
   d_keepAlive.push_back(reason);
@@ -646,7 +649,7 @@ void ArithCongruenceManager::equalsConstant(ConstraintCP lb, ConstraintCP ub){
                           << ub << std::endl;
 
   ArithVar x = lb->getVariable();
-  NodeBuilder<> nb(Kind::AND);
+  NodeBuilder nb(Kind::AND);
   auto pfLb = lb->externalExplainByAssertions(nb);
   auto pfUb = ub->externalExplainByAssertions(nb);
   Node reason = safeConstructNary(nb);
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 055d5ddbb..325f7002b 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -212,7 +212,7 @@ private:
   void enableSharedTerms();
   void dequeueLiterals();
 
-  void enqueueIntoNB(const std::set<TNode> all, NodeBuilder<>& nb);
+  void enqueueIntoNB(const std::set<TNode> all, NodeBuilder& nb);
 
   /**
    * Determine an explaination for `internal`. That is a conjunction of theory
@@ -251,7 +251,7 @@ private:
    */
   TrustNode explain(TNode literal);
 
-  void explain(TNode lit, NodeBuilder<>& out);
+  void explain(TNode lit, NodeBuilder& out);
 
   void addWatchedPair(ArithVar s, TNode x, TNode y);
 
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index baa9b1ebb..14daca11b 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -481,7 +481,7 @@ bool Constraint::isInternalAssumption() const {
 
 TrustNode Constraint::externalExplainByAssertions() const
 {
-  NodeBuilder<> nb(kind::AND);
+  NodeBuilder nb(kind::AND);
   auto pfFromAssumptions = externalExplain(nb, AssertionOrderSentinel);
   Node exp = safeConstructNary(nb);
   if (d_database->isProofEnabled())
@@ -1078,12 +1078,12 @@ TrustNode Constraint::split()
   TNode lhs = eqNode[0];
   TNode rhs = eqNode[1];
 
-  Node leqNode = NodeBuilder<2>(kind::LEQ) << lhs << rhs;
-  Node ltNode = NodeBuilder<2>(kind::LT) << lhs << rhs;
-  Node gtNode = NodeBuilder<2>(kind::GT) << lhs << rhs;
-  Node geqNode = NodeBuilder<2>(kind::GEQ) << lhs << rhs;
+  Node leqNode = NodeBuilder(kind::LEQ) << lhs << rhs;
+  Node ltNode = NodeBuilder(kind::LT) << lhs << rhs;
+  Node gtNode = NodeBuilder(kind::GT) << lhs << rhs;
+  Node geqNode = NodeBuilder(kind::GEQ) << lhs << rhs;
 
-  Node lemma = NodeBuilder<3>(OR) << leqNode << geqNode;
+  Node lemma = NodeBuilder(OR) << leqNode << geqNode;
 
   TrustNode trustedLemma;
   if (d_database->isProofEnabled())
@@ -1517,7 +1517,7 @@ TrustNode Constraint::externalExplainForPropagation(TNode lit) const
   Assert(hasProof());
   Assert(!isAssumption());
   Assert(!isInternalAssumption());
-  NodeBuilder<> nb(Kind::AND);
+  NodeBuilder nb(Kind::AND);
   auto pfFromAssumptions = externalExplain(nb, d_assertionOrder);
   Node n = safeConstructNary(nb);
   if (d_database->isProofEnabled())
@@ -1553,7 +1553,7 @@ TrustNode Constraint::externalExplainConflict() const
 {
   Debug("pf::arith::explain") << this << std::endl;
   Assert(inConflict());
-  NodeBuilder<> nb(kind::AND);
+  NodeBuilder nb(kind::AND);
   auto pf1 = externalExplainByAssertions(nb);
   auto not2 = getNegation()->getProofLiteral().negate();
   auto pf2 = getNegation()->externalExplainByAssertions(nb);
@@ -1650,7 +1650,7 @@ void Constraint::assertionFringe(ConstraintCPVec& o, const ConstraintCPVec& i){
 }
 
 Node Constraint::externalExplain(const ConstraintCPVec& v, AssertionOrder order){
-  NodeBuilder<> nb(kind::AND);
+  NodeBuilder nb(kind::AND);
   ConstraintCPVec::const_iterator i, end;
   for(i = v.begin(), end = v.end(); i != end; ++i){
     ConstraintCP v_i = *i;
@@ -1660,7 +1660,7 @@ Node Constraint::externalExplain(const ConstraintCPVec& v, AssertionOrder order)
 }
 
 std::shared_ptr<ProofNode> Constraint::externalExplain(
-    NodeBuilder<>& nb, AssertionOrder order) const
+    NodeBuilder& nb, AssertionOrder order) const
 {
   if (Debug.isOn("pf::arith::explain"))
   {
@@ -1857,14 +1857,14 @@ std::shared_ptr<ProofNode> Constraint::externalExplain(
 }
 
 Node Constraint::externalExplainByAssertions(ConstraintCP a, ConstraintCP b){
-  NodeBuilder<> nb(kind::AND);
+  NodeBuilder nb(kind::AND);
   a->externalExplainByAssertions(nb);
   b->externalExplainByAssertions(nb);
   return nb;
 }
 
 Node Constraint::externalExplainByAssertions(ConstraintCP a, ConstraintCP b, ConstraintCP c){
-  NodeBuilder<> nb(kind::AND);
+  NodeBuilder nb(kind::AND);
   a->externalExplainByAssertions(nb);
   b->externalExplainByAssertions(nb);
   c->externalExplainByAssertions(nb);
@@ -1982,7 +1982,7 @@ TrustNode ConstraintDatabase::eeExplain(const Constraint* const c) const
   return d_congruenceManager.explain(c->getLiteral());
 }
 
-void ConstraintDatabase::eeExplain(ConstraintCP c, NodeBuilder<>& nb) const
+void ConstraintDatabase::eeExplain(ConstraintCP c, NodeBuilder& nb) const
 {
   Assert(c->hasLiteral());
   // NOTE: this is not a recommended method since it ignores proofs
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index d00f16c90..33e39a5f0 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -571,8 +571,7 @@ class Constraint {
    * This is not appropriate for propagation!
    * Use explainForPropagation() instead.
    */
-  std::shared_ptr<ProofNode> externalExplainByAssertions(
-      NodeBuilder<>& nb) const
+  std::shared_ptr<ProofNode> externalExplainByAssertions(NodeBuilder& nb) const
   {
     return externalExplain(nb, AssertionOrderSentinel);
   }
@@ -876,7 +875,7 @@ class Constraint {
    * This is the minimum fringe of the implication tree
    * s.t. every constraint is assertedBefore(order) or hasEqualityEngineProof().
    */
-  std::shared_ptr<ProofNode> externalExplain(NodeBuilder<>& nb,
+  std::shared_ptr<ProofNode> externalExplain(NodeBuilder& nb,
                                              AssertionOrder order) const;
 
   static Node externalExplain(const ConstraintCPVec& b, AssertionOrder order);
@@ -1168,7 +1167,7 @@ private:
    */
   TrustNode eeExplain(ConstraintCP c) const;
   /** Get an explanation for this constraint from the equality engine */
-  void eeExplain(ConstraintCP c, NodeBuilder<>& nb) const;
+  void eeExplain(ConstraintCP c, NodeBuilder& nb) const;
 
   /**
    * Returns a constraint with the variable v, the constraint type t, and a value
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 6e069cdf6..3825a3a42 100644
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -198,7 +198,7 @@ Node DioSolver::proveIndex(TrailIndex i){
   const Polynomial& proof = d_trail[i].d_proof;
   Assert(!proof.isConstant());
 
-  NodeBuilder<> nb(kind::AND);
+  NodeBuilder nb(kind::AND);
   for(Polynomial::iterator iter = proof.begin(), end = proof.end(); iter!= end; ++iter){
     Monomial m = (*iter);
     Assert(!m.isConstant());
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 7b9002d82..940812604 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -420,7 +420,7 @@ public:
 
 template <class GetNodeIterator>
 inline Node makeNode(Kind k, GetNodeIterator start, GetNodeIterator end) {
-  NodeBuilder<> nb(k);
+  NodeBuilder nb(k);
 
   while(start != end) {
     nb << (*start).getNode();
diff --git a/src/theory/arith/proof_checker.cpp b/src/theory/arith/proof_checker.cpp
index 23f141535..248897ced 100644
--- a/src/theory/arith/proof_checker.cpp
+++ b/src/theory/arith/proof_checker.cpp
@@ -108,8 +108,8 @@ Node ArithProofRuleChecker::checkInternal(PfRule id,
 
       // Whether a strict inequality is in the sum.
       bool strict = false;
-      NodeBuilder<> leftSum(Kind::PLUS);
-      NodeBuilder<> rightSum(Kind::PLUS);
+      NodeBuilder leftSum(Kind::PLUS);
+      NodeBuilder rightSum(Kind::PLUS);
       for (size_t i = 0; i < children.size(); ++i)
       {
         // Adjust strictness
@@ -163,8 +163,8 @@ Node ArithProofRuleChecker::checkInternal(PfRule id,
 
       // Whether a strict inequality is in the sum.
       bool strict = false;
-      NodeBuilder<> leftSum(Kind::PLUS);
-      NodeBuilder<> rightSum(Kind::PLUS);
+      NodeBuilder leftSum(Kind::PLUS);
+      NodeBuilder rightSum(Kind::PLUS);
       for (size_t i = 0; i < children.size(); ++i)
       {
         Rational scalar = args[i].getConst<Rational>();
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 577aa0e6c..2e2a99174 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -139,8 +139,8 @@ TrustNode TheoryArith::ppRewriteEq(TNode atom)
     return TrustNode::null();
   }
   Assert(atom[0].getType().isReal());
-  Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1];
-  Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1];
+  Node leq = NodeBuilder(kind::LEQ) << atom[0] << atom[1];
+  Node geq = NodeBuilder(kind::GEQ) << atom[0] << atom[1];
   Node rewritten = Rewriter::rewrite(leq.andNode(geq));
   Debug("arith::preprocess")
       << "arith::preprocess() : returning " << rewritten << endl;
@@ -161,7 +161,8 @@ Theory::PPAssertStatus TheoryArith::ppAssert(
   return d_internal->ppAssert(tin, outSubstitutions);
 }
 
-void TheoryArith::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
+void TheoryArith::ppStaticLearn(TNode n, NodeBuilder& learned)
+{
   d_internal->ppStaticLearn(n, learned);
 }
 
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 40abe21e0..94d8a11dd 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -120,7 +120,7 @@ class TheoryArith : public Theory {
    * symbols.
    */
   TrustNode ppRewrite(TNode atom, std::vector<SkolemLemma>& lems) override;
-  void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
+  void ppStaticLearn(TNode in, NodeBuilder& learned) override;
 
   std::string identify() const override { return std::string("TheoryArith"); }
 
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index b11bff768..349630c02 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -244,7 +244,7 @@ static void resolve(ConstraintCPVec& buf, ConstraintP c, const ConstraintCPVec&
   // Assert(uppos < upconf.getNumChildren());
   // Assert(equalUpToNegation(dnconf[dnpos], upconf[uppos]));
 
-  // NodeBuilder<> nb(kind::AND);
+  // NodeBuilder nb(kind::AND);
   // dropPosition(nb, dnconf, dnpos);
   // dropPosition(nb, upconf, uppos);
   // return safeConstructNary(nb);
@@ -1201,14 +1201,13 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert(
   return Theory::PP_ASSERT_STATUS_UNSOLVED;
 }
 
-void TheoryArithPrivate::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
+void TheoryArithPrivate::ppStaticLearn(TNode n, NodeBuilder& learned)
+{
   TimerStat::CodeTimer codeTimer(d_statistics.d_staticLearningTimer);
 
   d_learner.staticLearning(n, learned);
 }
 
-
-
 ArithVar TheoryArithPrivate::findShortestBasicRow(ArithVar variable){
   ArithVar bestBasic = ARITHVAR_SENTINEL;
   uint64_t bestRowLength = std::numeric_limits<uint64_t>::max();
@@ -2211,7 +2210,7 @@ std::pair<ConstraintP, ArithVar> TheoryArithPrivate::replayGetConstraint(const C
 
 Node toSumNode(const ArithVariables& vars, const DenseMap<Rational>& sum){
   Debug("arith::toSumNode") << "toSumNode() begin" << endl;
-  NodeBuilder<> nb(kind::PLUS);
+  NodeBuilder nb(kind::PLUS);
   NodeManager* nm = NodeManager::currentNM();
   DenseMap<Rational>::const_iterator iter, end;
   iter = sum.begin(), end = sum.end();
@@ -4682,7 +4681,7 @@ bool TheoryArithPrivate::tryToPropagate(RowIndex ridx, bool rowUp, ArithVar v, b
 }
 
 Node flattenImplication(Node imp){
-  NodeBuilder<> nb(kind::OR);
+  NodeBuilder nb(kind::OR);
   std::unordered_set<Node, NodeHashFunction> included;
   Node left = imp[0];
   Node right = imp[1];
@@ -4770,7 +4769,7 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C
         // Add the explaination proofs.
         for (const auto constraint : explain)
         {
-          NodeBuilder<> nb;
+          NodeBuilder nb;
           conflictPfs.push_back(constraint->externalExplainByAssertions(nb));
         }
         // Collect the farkas coefficients, as nodes.
@@ -5275,7 +5274,7 @@ void TheoryArithPrivate::entailmentCheckRowSum(std::pair<Node, DeltaRational>& t
   Assert(Polynomial::isMember(tp));
 
   tmp.second = DeltaRational(0);
-  NodeBuilder<> nb(kind::AND);
+  NodeBuilder nb(kind::AND);
 
   Polynomial p = Polynomial::parsePolynomial(tp);
   for(Polynomial::iterator i = p.begin(), iend = p.end(); i != iend; ++i) {
@@ -5460,7 +5459,7 @@ std::pair<Node, DeltaRational> TheoryArithPrivate::entailmentCheckSimplex(int sg
   switch(finalState){
   case Inferred:
     {
-      NodeBuilder<> nb(kind::AND);
+      NodeBuilder nb(kind::AND);
       for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){
         const Tableau::Entry& e =*ri;
         ArithVar colVar = e.getColVar();
@@ -5668,7 +5667,7 @@ std::pair<Node, DeltaRational> TheoryArithPrivate::entailmentCheckSimplex(int sg
 //   switch(finalState){
 //   case Inferred:
 //     {
-//       NodeBuilder<> nb(kind::AND);
+//       NodeBuilder nb(kind::AND);
 //       for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx);
 //       !ri.atEnd(); ++ri){
 //         const Tableau::Entry& e =*ri;
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 929f40b56..1a40af4a0 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -474,7 +474,7 @@ private:
   void notifyRestart();
   Theory::PPAssertStatus ppAssert(TrustNode tin,
                                   TrustSubstitutionMap& outSubstitutions);
-  void ppStaticLearn(TNode in, NodeBuilder<>& learned);
+  void ppStaticLearn(TNode in, NodeBuilder& learned);
 
   std::string identify() const { return std::string("TheoryArith"); }
 
@@ -678,8 +678,7 @@ private:
   bool isImpliedUpperBound(ArithVar var, Node exp);
   bool isImpliedLowerBound(ArithVar var, Node exp);
 
-  void internalExplain(TNode n, NodeBuilder<>& explainBuilder);
-
+  void internalExplain(TNode n, NodeBuilder& explainBuilder);
 
   void asVectors(const Polynomial& p,
                  std::vector<Rational>& coeffs,
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 543d9833c..3403eaee7 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -250,7 +250,7 @@ Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck
     // (index_0 != index_1 & index_0 != index_2 & ... & index_0 != index_n) -> read(store, index_0) = v_0
     TNode write_i, write_j, index_i, index_j;
     Node conc;
-    NodeBuilder<> result(kind::AND);
+    NodeBuilder result(kind::AND);
     int i, j;
     write_i = left;
     for (i = leftWrites-1; i >= 0; --i) {
@@ -260,7 +260,7 @@ Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck
       //         ... && index_i /= index_(i+1)] -> read(store, index_i) = v_i
       write_j = left;
       {
-        NodeBuilder<> hyp(kind::AND);
+        NodeBuilder hyp(kind::AND);
         for (j = leftWrites - 1; j > i; --j) {
           index_j = write_j[1];
           if (!ppCheck || !ppDisequal(index_i, index_j)) {
@@ -303,7 +303,7 @@ Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck
     // store(store(...),i,select(a,i)) = a && select(store(...),i)=v
     Node l = left;
     Node tmp;
-    NodeBuilder<> nb(kind::AND);
+    NodeBuilder nb(kind::AND);
     while (right.getKind() == kind::STORE) {
       tmp = nm->mkNode(kind::SELECT, l, right[1]);
       nb << tmp.eqNode(right[2]);
@@ -337,7 +337,7 @@ TrustNode TheoryArrays::ppRewrite(TNode term, std::vector<SkolemLemma>& lems)
       // select(store(a,i,v),j) = select(a,j)
       //    IF i != j
       if (term[0].getKind() == kind::STORE && ppDisequal(term[0][1], term[1])) {
-        ret = NodeBuilder<2>(kind::SELECT) << term[0][0] << term[1];
+        ret = NodeBuilder(kind::SELECT) << term[0][0] << term[1];
       }
       break;
     }
@@ -345,8 +345,10 @@ TrustNode TheoryArrays::ppRewrite(TNode term, std::vector<SkolemLemma>& lems)
       // store(store(a,i,v),j,w) = store(store(a,j,w),i,v)
       //    IF i != j and j comes before i in the ordering
       if (term[0].getKind() == kind::STORE && (term[1] < term[0][1]) && ppDisequal(term[1],term[0][1])) {
-        Node inner = NodeBuilder<3>(kind::STORE) << term[0][0] << term[1] << term[2];
-        Node outer = NodeBuilder<3>(kind::STORE) << inner << term[0][1] << term[0][2];
+        Node inner = NodeBuilder(kind::STORE)
+                     << term[0][0] << term[1] << term[2];
+        Node outer = NodeBuilder(kind::STORE)
+                     << inner << term[0][1] << term[0][2];
         ret = outer;
       }
       break;
@@ -1443,7 +1445,7 @@ Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions, bool invert, unsigned
     }
   }
 
-  NodeBuilder<> conjunction(invert ? kind::OR : kind::AND);
+  NodeBuilder conjunction(invert ? kind::OR : kind::AND);
   std::set<TNode>::const_iterator it = all.begin();
   std::set<TNode>::const_iterator it_end = all.end();
   while (it != it_end) {
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index f1e002735..70a5674b8 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -88,7 +88,7 @@ RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode)
     Assert(childList.size()
            < static_cast<size_t>(expr::NodeValue::MAX_CHILDREN)
                  * static_cast<size_t>(expr::NodeValue::MAX_CHILDREN));
-    NodeBuilder<> nb(k);
+    NodeBuilder nb(k);
     ChildList::iterator cur = childList.begin(), next, en = childList.end();
     while (cur != en)
     {
diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index 62c458723..acb67a373 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -151,7 +151,7 @@ Node AbstractionModule::reverseAbstraction(Node assertion, NodeNodeMap& seen) {
     return assertion;
   }
 
-  NodeBuilder<> result(assertion.getKind());
+  NodeBuilder result(assertion.getKind());
   if (assertion.getMetaKind() == kind::metakind::PARAMETERIZED) {
     result << assertion.getOperator();
   }
@@ -204,7 +204,7 @@ void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions)
       assertion_table.addEntry(func.getOperator(), args);
     }
 
-    NodeBuilder<> assertion_builder(kind::OR);
+    NodeBuilder assertion_builder(kind::OR);
     // construct skolemized assertion
     for (ArgsTable::iterator it = assertion_table.begin();
          it != assertion_table.end();
@@ -214,7 +214,7 @@ void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions)
       ++(d_statistics.d_numArgsSkolemized);
       TNode func = it->first;
       ArgsTableEntry& args = it->second;
-      NodeBuilder<> skolem_func(kind::APPLY_UF);
+      NodeBuilder skolem_func(kind::APPLY_UF);
       skolem_func << func;
       std::vector<Node> skolem_args;
 
@@ -241,7 +241,7 @@ void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions)
       // for (ArgsTableEntry::iterator it = args.begin(); it != args.end();
       // ++it)
       {
-        NodeBuilder<> arg_assignment(kind::AND);
+        NodeBuilder arg_assignment(kind::AND);
         // ArgsVec& args = *it;
         for (unsigned k = 0; k < av.size(); ++k)
         {
@@ -342,7 +342,7 @@ Node AbstractionModule::computeSignatureRec(TNode node, NodeNodeMap& cache) {
     return sig;
   }
 
-  NodeBuilder<> builder(node.getKind());
+  NodeBuilder builder(node.getKind());
   if (node.getMetaKind() == kind::metakind::PARAMETERIZED) {
     builder << node.getOperator();
   }
@@ -676,7 +676,7 @@ Node AbstractionModule::substituteArguments(TNode signature, TNode apply, unsign
     return signature;
   }
 
-  NodeBuilder<> builder(signature.getKind());
+  NodeBuilder builder(signature.getKind());
   if (signature.getMetaKind() == kind::metakind::PARAMETERIZED) {
     builder << signature.getOperator();
   }
diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h
index 311d44c94..dd0be5cc0 100644
--- a/src/theory/bv/bitblast/bitblaster.h
+++ b/src/theory/bv/bitblast/bitblaster.h
@@ -247,7 +247,7 @@ Node TBitblaster<T>::getTermModel(TNode node, bool fullModel)
   }
   Assert(node.getType().isBitVector());
 
-  NodeBuilder<> nb(node.getKind());
+  NodeBuilder nb(node.getKind());
   if (node.getMetaKind() == kind::metakind::PARAMETERIZED)
   {
     nb << node.getOperator();
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index a5d3e9bb6..568ef2ebf 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -411,7 +411,7 @@ bool TLazyBitblaster::MinisatNotify::notify(prop::SatLiteral lit) {
 
 void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) {
   if (clause.size() > 1) {
-    NodeBuilder<> lemmab(kind::OR);
+    NodeBuilder lemmab(kind::OR);
     for (unsigned i = 0; i < clause.size(); ++ i) {
       lemmab << d_cnf->getNode(clause[i]);
     }
diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h
index faa285b97..8fa8fd850 100644
--- a/src/theory/bv/bv_solver.h
+++ b/src/theory/bv/bv_solver.h
@@ -90,7 +90,7 @@ class BVSolver
 
   virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); };
 
-  virtual void ppStaticLearn(TNode in, NodeBuilder<>& learned){};
+  virtual void ppStaticLearn(TNode in, NodeBuilder& learned){};
 
   virtual void presolve(){};
 
diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index 125cb243f..0aa99a889 100644
--- a/src/theory/bv/bv_solver_bitblast.cpp
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -256,7 +256,7 @@ Node BVSolverBitblast::getValue(TNode node)
     }
     else if (it->second.isNull())
     {
-      NodeBuilder<> nb(cur.getKind());
+      NodeBuilder nb(cur.getKind());
       if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
       {
         nb << cur.getOperator();
diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp
index 00190233c..c12121bf8 100644
--- a/src/theory/bv/bv_solver_lazy.cpp
+++ b/src/theory/bv/bv_solver_lazy.cpp
@@ -741,7 +741,7 @@ EqualityStatus BVSolverLazy::getEqualityStatus(TNode a, TNode b)
   ;
 }
 
-void BVSolverLazy::ppStaticLearn(TNode in, NodeBuilder<>& learned)
+void BVSolverLazy::ppStaticLearn(TNode in, NodeBuilder& learned)
 {
   if (d_staticLearnCache.find(in) != d_staticLearnCache.end())
   {
diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h
index ea647346e..35b9964e0 100644
--- a/src/theory/bv/bv_solver_lazy.h
+++ b/src/theory/bv/bv_solver_lazy.h
@@ -97,7 +97,7 @@ class BVSolverLazy : public BVSolver
 
   TrustNode ppRewrite(TNode t) override;
 
-  void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
+  void ppStaticLearn(TNode in, NodeBuilder& learned) override;
 
   void presolve() override;
 
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index c025dab5d..221ad3cbd 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -160,7 +160,7 @@ Node SubstitutionEx::internalApply(TNode node) {
 
     // children already processed
     if (head.childrenAdded) {
-      NodeBuilder<> nb(current.getKind());
+      NodeBuilder nb(current.getKind());
       std::vector<Node> reasons;
 
       if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
@@ -512,7 +512,7 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) {
       return changed;
     }
 
-    NodeBuilder<> nb(kind::BITVECTOR_XOR);
+    NodeBuilder nb(kind::BITVECTOR_XOR);
     for (unsigned i = 1; i < left.getNumChildren(); ++i) {
       nb << left[i];
     }
@@ -848,7 +848,7 @@ void ExtractSkolemizer::skolemize(std::vector<WorklistElement>& facts) {
       Node sk = utils::mkVar(size);
       skolems.push_back(sk);
     }
-    NodeBuilder<> skolem_nb(kind::BITVECTOR_CONCAT);
+    NodeBuilder skolem_nb(kind::BITVECTOR_CONCAT);
 
     for (int i = skolems.size() - 1; i >= 0; --i) {
       skolem_nb << skolems[i];
@@ -975,7 +975,7 @@ Node mergeExplanations(const std::vector<Node>& expls) {
     return *literals.begin();
   }
 
-  NodeBuilder<> nb(kind::AND);
+  NodeBuilder nb(kind::AND);
 
   for (TNodeSet::const_iterator it = literals.begin(); it!= literals.end(); ++it) {
     nb << *it;
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 8f9f88ea2..2c6d52b15 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -223,7 +223,7 @@ void TheoryBV::notifySharedTerm(TNode t)
   d_internal->notifySharedTerm(t);
 }
 
-void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned)
+void TheoryBV::ppStaticLearn(TNode in, NodeBuilder& learned)
 {
   d_internal->ppStaticLearn(in, learned);
 }
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index c9ddaad11..c22f5c95a 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -92,7 +92,7 @@ class TheoryBV : public Theory
 
   TrustNode ppRewrite(TNode t, std::vector<SkolemLemma>& lems) override;
 
-  void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
+  void ppStaticLearn(TNode in, NodeBuilder& learned) override;
 
   void presolve() override;
 
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index e92ed5543..6435e0e3c 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -642,7 +642,7 @@ struct ApplyRuleToChildren {
     if (node.getKind() != kind) {
       return RewriteRule<rule>::template run<true>(node);
     }
-    NodeBuilder<> result(kind);
+    NodeBuilder result(kind);
     for (unsigned i = 0, end = node.getNumChildren(); i < end; ++ i) {
       result << RewriteRule<rule>::template run<true>(node[i]);
     }
diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h
index 7060b68a9..c463f0faf 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_core.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_core.h
@@ -36,7 +36,7 @@ bool RewriteRule<ConcatFlatten>::applies(TNode node) {
 template<> inline
 Node RewriteRule<ConcatFlatten>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << node << ")" << std::endl;
-  NodeBuilder<> result(kind::BITVECTOR_CONCAT);
+  NodeBuilder result(kind::BITVECTOR_CONCAT);
   std::vector<Node> processing_stack;
   processing_stack.push_back(node);
   while (!processing_stack.empty()) {
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 4872f8070..39425b41e 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -284,7 +284,7 @@ static inline void updateCoefMap(TNode current, unsigned size,
         }
       }
       else if (current[current.getNumChildren()-1].isConst()) {
-        NodeBuilder<> nb(kind::BITVECTOR_MULT);
+        NodeBuilder nb(kind::BITVECTOR_MULT);
         TNode::iterator child_it = current.begin();
         for(; (child_it+1) != current.end(); ++child_it) {
           Assert(!(*child_it).isConst());
@@ -353,7 +353,7 @@ static inline void addToChildren(TNode term,
   }
   else if (term.getKind() == kind::BITVECTOR_MULT)
   {
-    NodeBuilder<> nb(kind::BITVECTOR_MULT);
+    NodeBuilder nb(kind::BITVECTOR_MULT);
     TNode::iterator child_it = term.begin();
     for (; child_it != term.end(); ++child_it)
     {
@@ -896,7 +896,7 @@ bool RewriteRule<BitwiseEq>::applies(TNode node) {
 static inline Node mkNodeKind(Kind k, TNode node, TNode c) {
   unsigned i = 0;
   unsigned nc = node.getNumChildren();
-  NodeBuilder<> nb(k);
+  NodeBuilder nb(k);
   for(; i < nc; ++i) {
     nb << node[i].eqNode(c);
   }
@@ -991,7 +991,7 @@ template<> inline
 Node RewriteRule<NegMult>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<NegMult>(" << node << ")" << std::endl;
   TNode mult = node[0];
-  NodeBuilder<> nb(kind::BITVECTOR_MULT);
+  NodeBuilder nb(kind::BITVECTOR_MULT);
   BitVector bv(utils::getSize(node), (unsigned)1);
   TNode::iterator child_it = mult.begin();
   for(; (child_it+1) != mult.end(); ++child_it) {
@@ -1492,8 +1492,8 @@ inline Node RewriteRule<NormalizeEqPlusNeg>::apply(TNode node)
   Debug("bv-rewrite") << "RewriteRule<NormalizeEqPlusNeg>(" << node << ")"
                       << std::endl;
 
-  NodeBuilder<> nb_lhs(kind::BITVECTOR_PLUS);
-  NodeBuilder<> nb_rhs(kind::BITVECTOR_PLUS);
+  NodeBuilder nb_lhs(kind::BITVECTOR_PLUS);
+  NodeBuilder nb_rhs(kind::BITVECTOR_PLUS);
   NodeManager *nm = NodeManager::currentNM();
 
   if (node[0].getKind() == kind::BITVECTOR_PLUS)
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index 3244ebb6e..3dd0da3bd 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -286,7 +286,7 @@ inline Node RewriteRule<RepeatEliminate>::apply(TNode node)
   if(amount == 1) {
     return a; 
   }
-  NodeBuilder<> result(kind::BITVECTOR_CONCAT);
+  NodeBuilder result(kind::BITVECTOR_CONCAT);
   for(unsigned i = 0; i < amount; ++i) {
     result << node[0]; 
   }
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 2e99cc467..c0bce9097 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -558,10 +558,10 @@ inline Node RewriteRule<AndOrXorConcatPullUp>::apply(TNode node)
   Kind kind = node.getKind();
   TNode concat;
   Node x, y, z, c;
-  NodeBuilder<> xb(kind);
-  NodeBuilder<> yb(kind::BITVECTOR_CONCAT);
-  NodeBuilder<> zb(kind::BITVECTOR_CONCAT);
-  NodeBuilder<> res(kind::BITVECTOR_CONCAT);
+  NodeBuilder xb(kind);
+  NodeBuilder yb(kind::BITVECTOR_CONCAT);
+  NodeBuilder zb(kind::BITVECTOR_CONCAT);
+  NodeBuilder res(kind::BITVECTOR_CONCAT);
   NodeManager* nm = NodeManager::currentNM();
 
   for (const TNode& child : node)
@@ -1680,13 +1680,13 @@ Node RewriteRule<MergeSignExtend>::apply(TNode node) {
                            .d_zeroExtendAmount;
     if (amount2 == 0)
     {
-      NodeBuilder<> nb(kind::BITVECTOR_SIGN_EXTEND);
+      NodeBuilder nb(kind::BITVECTOR_SIGN_EXTEND);
       Node op = nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(amount1));
       nb << op << node[0][0];
       Node res = nb;
       return res;
     }
-    NodeBuilder<> nb(kind::BITVECTOR_ZERO_EXTEND);
+    NodeBuilder nb(kind::BITVECTOR_ZERO_EXTEND);
     Node op = nm->mkConst<BitVectorZeroExtend>(
         BitVectorZeroExtend(amount1 + amount2));
     nb << op << node[0][0];
@@ -2246,7 +2246,7 @@ Node RewriteRule<MultSltMult>::apply(TNode node)
   Node zero_t = utils::mkZero(utils::getSize(t));
   Node zero_a = utils::mkZero(utils::getSize(a));
 
-  NodeBuilder<> nb(kind::AND);
+  NodeBuilder nb(kind::AND);
   Kind k = is_sext ? kind::BITVECTOR_SLT : kind::BITVECTOR_ULT;
   nb << t.eqNode(zero_t).notNode();
   nb << a.eqNode(zero_a).notNode();
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index c2a7f05b6..96f91ea9f 100644
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -384,7 +384,7 @@ Node mkConcat(TNode node, unsigned repeat)
   {
     return node;
   }
-  NodeBuilder<> result(kind::BITVECTOR_CONCAT);
+  NodeBuilder result(kind::BITVECTOR_CONCAT);
   for (unsigned i = 0; i < repeat; ++i)
   {
     result << node;
@@ -503,7 +503,7 @@ Node eliminateInt2Bv(TNode node)
   {
     return v[0];
   }
-  NodeBuilder<> result(kind::BITVECTOR_CONCAT);
+  NodeBuilder result(kind::BITVECTOR_CONCAT);
   result.append(v.rbegin(), v.rend());
   return Node(result);
 }
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 04258d441..38b6caf94 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -140,7 +140,7 @@ Node mkAnd(const std::vector<NodeTemplate<ref_count>>& conjunctions)
   /* All the same, or just one  */
   if (all.size() == 1) { return conjunctions[0]; }
 
-  NodeBuilder<> conjunction(kind::AND);
+  NodeBuilder conjunction(kind::AND);
   for (TNode n : all) { conjunction << n; }
   return conjunction;
 }
@@ -159,7 +159,7 @@ Node mkOr(const std::vector<NodeTemplate<ref_count>>& nodes)
   /* All the same, or just one  */
   if (all.size() == 1) { return nodes[0]; }
 
-  NodeBuilder<> disjunction(kind::OR);
+  NodeBuilder disjunction(kind::OR);
   for (TNode n : all) { disjunction << n; }
   return disjunction;
 }
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 9d231f07d..6b455e38c 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -322,7 +322,7 @@ void TheoryDatatypes::postCheck(Effort level)
                     Node test = utils::mkTester(n, consIndex, dt);
                     Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n << endl;
                     test = Rewriter::rewrite( test );
-                    NodeBuilder<> nb(kind::OR);
+                    NodeBuilder nb(kind::OR);
                     nb << test << test.notNode();
                     Node lemma = nb;
                     d_im.lemma(lemma, InferenceId::DATATYPES_BINARY_SPLIT);
@@ -543,7 +543,7 @@ TrustNode TheoryDatatypes::expandDefinition(Node n)
     {
       Assert(tn.isDatatype());
       const DType& dt = tn.getDType();
-      NodeBuilder<> b(APPLY_CONSTRUCTOR);
+      NodeBuilder b(APPLY_CONSTRUCTOR);
       b << dt[0].getConstructor();
       size_t size, updateIndex;
       if (n.getKind() == TUPLE_UPDATE)
@@ -957,7 +957,7 @@ void TheoryDatatypes::addTester(
           Assert(testerIndex != -1);
           //we must explain why each term in the set of testers for this equivalence class is equal
           std::vector< Node > eq_terms;
-          NodeBuilder<> nb(kind::AND);
+          NodeBuilder nb(kind::AND);
           for (unsigned i = 0; i < n_lbl; i++)
           {
             Node ti = d_labels_data[n][i];
diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp
index 769446fd2..ca147b88e 100644
--- a/src/theory/datatypes/type_enumerator.cpp
+++ b/src/theory/datatypes/type_enumerator.cpp
@@ -138,7 +138,7 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
        }
      }
      Debug("dt-enum-debug") << "Get constructor..." << std::endl;
-     NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
+     NodeBuilder b(kind::APPLY_CONSTRUCTOR);
      if (d_datatype.isParametric())
      {
        NodeManager* nm = NodeManager::currentNM();
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index 3b5a115c8..1d124045b 100644
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -648,7 +648,7 @@ symbolicBitVector<false> symbolicBitVector<isSigned>::toUnsigned(void) const
 template <>
 symbolicBitVector<true> symbolicBitVector<true>::extend(bwt extension) const
 {
-  NodeBuilder<> construct(kind::BITVECTOR_SIGN_EXTEND);
+  NodeBuilder construct(kind::BITVECTOR_SIGN_EXTEND);
   construct << NodeManager::currentNM()->mkConst<BitVectorSignExtend>(
                    BitVectorSignExtend(extension))
             << *this;
@@ -659,7 +659,7 @@ symbolicBitVector<true> symbolicBitVector<true>::extend(bwt extension) const
 template <>
 symbolicBitVector<false> symbolicBitVector<false>::extend(bwt extension) const
 {
-  NodeBuilder<> construct(kind::BITVECTOR_ZERO_EXTEND);
+  NodeBuilder construct(kind::BITVECTOR_ZERO_EXTEND);
   construct << NodeManager::currentNM()->mkConst<BitVectorZeroExtend>(
                    BitVectorZeroExtend(extension))
             << *this;
@@ -673,7 +673,7 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::contract(
 {
   Assert(this->getWidth() > reduction);
 
-  NodeBuilder<> construct(kind::BITVECTOR_EXTRACT);
+  NodeBuilder construct(kind::BITVECTOR_EXTRACT);
   construct << NodeManager::currentNM()->mkConst<BitVectorExtract>(
                    BitVectorExtract((this->getWidth() - 1) - reduction, 0))
             << *this;
@@ -724,7 +724,7 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::extract(
 {
   Assert(upper >= lower);
 
-  NodeBuilder<> construct(kind::BITVECTOR_EXTRACT);
+  NodeBuilder construct(kind::BITVECTOR_EXTRACT);
   construct << NodeManager::currentNM()->mkConst<BitVectorExtract>(
                    BitVectorExtract(upper, lower))
             << *this;
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 38444c7af..f2df859f0 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -91,7 +91,7 @@ Node buildConjunct(const std::vector<TNode> &assumptions) {
   } else {
     // \todo see bv::utils::flattenAnd
 
-    NodeBuilder<> conjunction(kind::AND);
+    NodeBuilder conjunction(kind::AND);
     for (std::vector<TNode>::const_iterator it = assumptions.begin();
          it != assumptions.end(); ++it) {
       conjunction << *it;
diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index d84c553de..ba94dca13 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -110,8 +110,7 @@ namespace rewrite {
 
     size_t children = node.getNumChildren();
     if (children > 2) {
-
-      NodeBuilder<> conjunction(kind::AND);
+      NodeBuilder conjunction(kind::AND);
 
       for (size_t i = 0; i < children - 1; ++i) {
 	for (size_t j = i + 1; j < children; ++j) {
diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index 014e46925..292ec2ec6 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -202,7 +202,7 @@ static Node dropChild(Node n, unsigned index)
   if (nchildren < 2) return Node::null();
 
   Kind k = n.getKind();
-  NodeBuilder<> nb(k);
+  NodeBuilder nb(k);
   for (unsigned i = 0; i < nchildren; ++i)
   {
     if (i == index) continue;
@@ -350,7 +350,7 @@ Node BvInverter::solveBvLit(Node sv,
         unsigned upper, lower;
         upper = bv::utils::getSize(t) - 1;
         lower = 0;
-        NodeBuilder<> nb(BITVECTOR_CONCAT);
+        NodeBuilder nb(BITVECTOR_CONCAT);
         for (unsigned i = 0; i < nchildren; i++)
         {
           if (i < index)
diff --git a/src/theory/quantifiers/bv_inverter_utils.cpp b/src/theory/quantifiers/bv_inverter_utils.cpp
index e53e64a94..53e672346 100644
--- a/src/theory/quantifiers/bv_inverter_utils.cpp
+++ b/src/theory/quantifiers/bv_inverter_utils.cpp
@@ -1180,7 +1180,7 @@ namespace {
 Node defaultShiftIC(Kind litk, Kind shk, Node s, Node t)
 {
   unsigned w;
-  NodeBuilder<> nb(OR);
+  NodeBuilder nb(OR);
   NodeManager* nm;
 
   nm = NodeManager::currentNM();
@@ -2000,7 +2000,7 @@ Node getICBvConcat(bool pol, Kind litk, unsigned idx, Node x, Node sv_t, Node t)
   unsigned nchildren = sv_t.getNumChildren();
   unsigned w1 = 0, w2 = 0;
   unsigned w = bv::utils::getSize(t), wx = bv::utils::getSize(x);
-  NodeBuilder<> nbs1(BITVECTOR_CONCAT), nbs2(BITVECTOR_CONCAT);
+  NodeBuilder nbs1(BITVECTOR_CONCAT), nbs2(BITVECTOR_CONCAT);
   Node s1, s2;
   Node t1, t2, tx;
   Node scl, scr;
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
index 030258113..0a544f785 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
@@ -66,7 +66,7 @@ Node normalizePvMult(
   bool neg, neg_coeff = false;
   bool found_pv = false;
   NodeManager* nm;
-  NodeBuilder<> nb(BITVECTOR_MULT);
+  NodeBuilder nb(BITVECTOR_MULT);
   BvLinearAttribute is_linear;
 
   nm = NodeManager::currentNM();
@@ -168,8 +168,8 @@ Node normalizePvPlus(
     std::unordered_map<Node, bool, NodeHashFunction>& contains_pv)
 {
   NodeManager* nm;
-  NodeBuilder<> nb_c(BITVECTOR_PLUS);
-  NodeBuilder<> nb_l(BITVECTOR_PLUS);
+  NodeBuilder nb_c(BITVECTOR_PLUS);
+  NodeBuilder nb_l(BITVECTOR_PLUS);
   BvLinearAttribute is_linear;
   bool neg;
 
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 2c91df7a7..89358c511 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -104,7 +104,8 @@ bool QuantifiersRewriter::isLiteral( Node n ){
   return true;
 }
 
-void QuantifiersRewriter::addNodeToOrBuilder( Node n, NodeBuilder<>& t ){
+void QuantifiersRewriter::addNodeToOrBuilder(Node n, NodeBuilder& t)
+{
   if( n.getKind()==OR ){
     for( int i=0; i<(int)n.getNumChildren(); i++ ){
       t << n[i];
@@ -1596,7 +1597,7 @@ Node QuantifiersRewriter::computeMiniscoping(Node q, QAttributes& qa)
       BoundVarManager* bvm = nm->getBoundVarManager();
       // Break apart the quantifed formula
       // forall x. P1 ^ ... ^ Pn ---> forall x. P1 ^ ... ^ forall x. Pn
-      NodeBuilder<> t(kind::AND);
+      NodeBuilder t(kind::AND);
       std::vector<Node> argsc;
       for (size_t i = 0, nchild = body.getNumChildren(); i < nchild; i++)
       {
@@ -1645,8 +1646,8 @@ Node QuantifiersRewriter::computeMiniscoping(Node q, QAttributes& qa)
       // aggressive miniscoping implies that free variable miniscoping should
       // be applied first
       Node newBody = body;
-      NodeBuilder<> body_split(kind::OR);
-      NodeBuilder<> tb(kind::OR);
+      NodeBuilder body_split(kind::OR);
+      NodeBuilder tb(kind::OR);
       for (const Node& trm : body)
       {
         if (expr::hasSubterm(trm, args))
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 5ea8352d0..c45bc9e88 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -140,7 +140,7 @@ class QuantifiersRewriter : public TheoryRewriter
                                 Kind k,
                                 std::map<Node, bool>& lit_pol,
                                 bool& childrenChanged);
-  static void addNodeToOrBuilder(Node n, NodeBuilder<>& t);
+  static void addNodeToOrBuilder(Node n, NodeBuilder& t);
   static void computeArgs(const std::vector<Node>& args,
                           std::map<Node, bool>& activeMap,
                           Node n,
diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp
index 2a19824ac..51b400dbe 100644
--- a/src/theory/quantifiers/skolemize.cpp
+++ b/src/theory/quantifiers/skolemize.cpp
@@ -85,7 +85,7 @@ TrustNode Skolemize::process(Node q)
     // otherwise, we use the more general skolemization with inductive
     // strengthening, which does not support proofs
     Node body = getSkolemizedBody(q);
-    NodeBuilder<> nb(kind::OR);
+    NodeBuilder nb(kind::OR);
     nb << q << body.notNode();
     lem = nb;
   }
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 1d9620dab..c247d8f08 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -89,7 +89,7 @@ struct RewriteStackElement {
   /** Index of the child this node is done rewriting */
   unsigned d_nextChild : 32;
   /** Builder for this node */
-  NodeBuilder<> d_builder;
+  NodeBuilder d_builder;
 };
 
 RewriteResponse identityRewrite(RewriteEnvironment* re, TNode n)
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 8d005c6fe..87a3ae9af 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1210,7 +1210,7 @@ Node mkAnd(const std::vector<TNode>& conjunctions)
     return conjunctions[0];
   }
 
-  NodeBuilder<> conjunction(kind::AND);
+  NodeBuilder conjunction(kind::AND);
   std::set<TNode>::const_iterator it = all.begin();
   std::set<TNode>::const_iterator it_end = all.end();
   while (it != it_end)
diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp
index cc4027aad..04e0fe2e5 100644
--- a/src/theory/strings/regexp_entail.cpp
+++ b/src/theory/strings/regexp_entail.cpp
@@ -639,7 +639,7 @@ Node RegExpEntail::getFixedLengthForRegexp(Node n)
   }
   else if (n.getKind() == REGEXP_CONCAT)
   {
-    NodeBuilder<> nb(PLUS);
+    NodeBuilder nb(PLUS);
     for (const Node& nc : n)
     {
       Node flc = getFixedLengthForRegexp(nc);
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 302f7dc0b..a7bbb68e3 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -1184,7 +1184,7 @@ Node SequencesRewriter::rewriteMembership(TNode node)
         Node one = nm->mkConst(Rational(1));
         if (flr == one)
         {
-          NodeBuilder<> nb(AND);
+          NodeBuilder nb(AND);
           for (const Node& xc : x)
           {
             nb << nm->mkNode(STRING_IN_REGEXP, xc, r);
@@ -1926,7 +1926,7 @@ Node SequencesRewriter::rewriteContains(Node node)
       {
         std::vector<Node> vec = Word::getChars(node[0]);
         Node emp = Word::mkEmptyWord(t.getType());
-        NodeBuilder<> nb(OR);
+        NodeBuilder nb(OR);
         nb << emp.eqNode(t);
         for (const Node& c : vec)
         {
@@ -1970,7 +1970,7 @@ Node SequencesRewriter::rewriteContains(Node node)
       {
         std::vector<Node> nc1;
         utils::getConcat(node[0], nc1);
-        NodeBuilder<> nb(OR);
+        NodeBuilder nb(OR);
         for (const Node& ncc : nc1)
         {
           nb << nm->mkNode(STRING_STRCTN, ncc, node[1]);
@@ -2057,7 +2057,7 @@ Node SequencesRewriter::rewriteContains(Node node)
         if (nc2.size() > 1)
         {
           Node emp = Word::mkEmptyWord(stype);
-          NodeBuilder<> nb2(kind::AND);
+          NodeBuilder nb2(kind::AND);
           for (const Node& n2 : nc2)
           {
             if (n2 == n)
@@ -3283,7 +3283,7 @@ Node SequencesRewriter::canonicalStrForSymbolicLength(Node len, TypeNode stype)
   else if (len.getKind() == PLUS)
   {
     // x + y -> norm(x) + norm(y)
-    NodeBuilder<> concatBuilder(STRING_CONCAT);
+    NodeBuilder concatBuilder(STRING_CONCAT);
     for (const auto& n : len)
     {
       Node sn = canonicalStrForSymbolicLength(n, stype);
@@ -3312,7 +3312,7 @@ Node SequencesRewriter::canonicalStrForSymbolicLength(Node len, TypeNode stype)
     }
     std::vector<Node> nRepChildren;
     utils::getConcat(nRep, nRepChildren);
-    NodeBuilder<> concatBuilder(STRING_CONCAT);
+    NodeBuilder concatBuilder(STRING_CONCAT);
     for (size_t i = 0, reps = intReps.getUnsignedInt(); i < reps; i++)
     {
       concatBuilder.append(nRepChildren);
diff --git a/src/theory/strings/strings_entail.cpp b/src/theory/strings/strings_entail.cpp
index 62ba41743..fc5a0a52c 100644
--- a/src/theory/strings/strings_entail.cpp
+++ b/src/theory/strings/strings_entail.cpp
@@ -842,7 +842,7 @@ Node StringsEntail::getMultisetApproximation(Node a)
   }
   else if (a.getKind() == STRING_CONCAT)
   {
-    NodeBuilder<> nb(STRING_CONCAT);
+    NodeBuilder nb(STRING_CONCAT);
     for (const Node& ac : a)
     {
       nb << getMultisetApproximation(ac);
@@ -974,7 +974,7 @@ Node StringsEntail::inferEqsFromContains(Node x, Node y)
     cs.push_back(yiLen[0]);
   }
 
-  NodeBuilder<> nb(AND);
+  NodeBuilder nb(AND);
   // (= x (str.++ y1' ... ym'))
   if (!cs.empty())
   {
diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp
index 1a7ca7f6a..2a3da149c 100644
--- a/src/theory/strings/strings_rewriter.cpp
+++ b/src/theory/strings/strings_rewriter.cpp
@@ -179,7 +179,7 @@ Node StringsRewriter::rewriteStrConvert(Node node)
   }
   else if (node[0].getKind() == STRING_CONCAT)
   {
-    NodeBuilder<> concatBuilder(STRING_CONCAT);
+    NodeBuilder concatBuilder(STRING_CONCAT);
     for (const Node& nc : node[0])
     {
       concatBuilder << nm->mkNode(nk, nc);
diff --git a/src/theory/subs_minimize.cpp b/src/theory/subs_minimize.cpp
index a61f2d49c..9102b6188 100644
--- a/src/theory/subs_minimize.cpp
+++ b/src/theory/subs_minimize.cpp
@@ -224,7 +224,7 @@ bool SubstitutionMinimize::findInternal(Node n,
       if (cur.getNumChildren() > 0)
       {
         std::vector<Node> children;
-        NodeBuilder<> nb(cur.getKind());
+        NodeBuilder nb(cur.getKind());
         if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
         {
           if (cur.getKind() == APPLY_UF)
diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index 7a4516996..1a45f467c 100644
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -81,7 +81,7 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) {
     if (stackHead.d_children_added)
     {
       // Children have been processed, so substitute
-      NodeBuilder<> builder(current.getKind());
+      NodeBuilder builder(current.getKind());
       if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
         builder << Node(cache[current.getOperator()]);
       }
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 4b06a5fa8..4c0d14346 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -686,7 +686,7 @@ class Theory {
    * *never* clear it.  It is a conjunction to add to the formula at
    * the top-level and may contain other theories' contributions.
    */
-  virtual void ppStaticLearn(TNode in, NodeBuilder<>& learned) { }
+  virtual void ppStaticLearn(TNode in, NodeBuilder& learned) {}
 
   enum PPAssertStatus {
     /** Atom has been solved  */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 6271f0afb..e4b05a3c2 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -727,7 +727,8 @@ void TheoryEngine::notifyRestart() {
   CVC4_FOR_EACH_THEORY;
 }
 
-void TheoryEngine::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
+void TheoryEngine::ppStaticLearn(TNode in, NodeBuilder& learned)
+{
   // Reset the interrupt flag
   d_interrupted = false;
 
@@ -1638,7 +1639,7 @@ theory::TrustNode TheoryEngine::getExplanation(
   }
   else
   {
-    NodeBuilder<> conjunction(kind::AND);
+    NodeBuilder conjunction(kind::AND);
     std::set<TNode>::const_iterator it = exp.begin();
     std::set<TNode>::const_iterator it_end = exp.end();
     while (it != it_end)
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 7b91191f9..731e362ef 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -498,7 +498,7 @@ class TheoryEngine {
    * Calls ppStaticLearn() on all theories, accumulating their
    * combined contributions in the "learned" builder.
    */
-  void ppStaticLearn(TNode in, NodeBuilder<>& learned);
+  void ppStaticLearn(TNode in, NodeBuilder& learned);
 
   /**
    * Calls presolve() on all theories and returns true
diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index 78a4e6526..a28cb19f7 100644
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -320,7 +320,7 @@ TrustNode TheoryPreprocessor::theoryPreprocess(
     if (stackHead.children_added)
     {
       // Children have been processed, so substitute
-      NodeBuilder<> builder(current.getKind());
+      NodeBuilder builder(current.getKind());
       if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
       {
         builder << current.getOperator();
@@ -396,7 +396,7 @@ Node TheoryPreprocessor::ppTheoryRewrite(TNode term,
   Node newTerm = term;
   if (!term.isClosure())
   {
-    NodeBuilder<> newNode(term.getKind());
+    NodeBuilder newNode(term.getKind());
     if (term.getMetaKind() == kind::metakind::PARAMETERIZED)
     {
       newNode << term.getOperator();
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 8f006d8ff..5fbbd3700 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -1841,7 +1841,7 @@ void EqualityEngine::addTriggerEqualityInternal(TNode t1, TNode t2, TNode trigge
 
 Node EqualityEngine::evaluateTerm(TNode node) {
   Debug("equality::evaluation") << d_name << "::eq::evaluateTerm(" << node << ")" << std::endl;
-  NodeBuilder<> builder;
+  NodeBuilder builder;
   builder << node.getKind();
   if (node.getMetaKind() == kind::metakind::PARAMETERIZED) {
     builder << node.getOperator();
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index 558838bd8..0586da6a0 100644
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -525,7 +525,7 @@ void SymmetryBreaker::apply(std::vector<Node>& newClauses) {
           Debug("ufsymm") << "UFSYMM p == " << p << endl;
           if(i != p.end() || p.size() != cts.size()) {
             Debug("ufsymm") << "UFSYMM cts != p" << endl;
-            NodeBuilder<> disj(kind::OR);
+            NodeBuilder disj(kind::OR);
             NodeManager* nm = NodeManager::currentNM();
             for (const Node& nn : cts)
             {
diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h
index b4ea3640d..e38a1f67b 100644
--- a/src/theory/uf/symmetry_breaker.h
+++ b/src/theory/uf/symmetry_breaker.h
@@ -65,7 +65,7 @@ class SymmetryBreaker : public context::ContextNotifyObj {
 
   class Template {
     Node d_template;
-    NodeBuilder<> d_assertions;
+    NodeBuilder d_assertions;
     std::unordered_map<TNode, std::set<TNode>, TNodeHashFunction> d_sets;
     std::unordered_map<TNode, TNode, TNodeHashFunction> d_reps;
 
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index f3c0a0ba0..6969da194 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -112,7 +112,7 @@ static Node mkAnd(const std::vector<TNode>& conjunctions) {
     return conjunctions[0];
   }
 
-  NodeBuilder<> conjunction(kind::AND);
+  NodeBuilder conjunction(kind::AND);
   std::set<TNode>::const_iterator it = all.begin();
   std::set<TNode>::const_iterator it_end = all.end();
   while (it != it_end) {
@@ -347,7 +347,8 @@ void TheoryUF::presolve() {
   Debug("uf") << "uf: end presolve()" << endl;
 }
 
-void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
+void TheoryUF::ppStaticLearn(TNode n, NodeBuilder& learned)
+{
   //TimerStat::CodeTimer codeTimer(d_staticLearningTimer);
 
   vector<TNode> workList;
@@ -466,7 +467,7 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
   if(options::ufSymmetryBreaker()) {
     d_symb.assertFormula(n);
   }
-}/* TheoryUF::ppStaticLearn() */
+} /* TheoryUF::ppStaticLearn() */
 
 EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) {
 
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index f6f4b3ee9..66cf36ead 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -144,8 +144,7 @@ private:
   void preRegisterTerm(TNode term) override;
   TrustNode explain(TNode n) override;
 
-
-  void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
+  void ppStaticLearn(TNode in, NodeBuilder& learned) override;
   void presolve() override;
 
   void computeCareGraph() override;
diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp
index 5177ff453..02bd50b75 100644
--- a/test/unit/node/node_black.cpp
+++ b/test/unit/node/node_black.cpp
@@ -76,7 +76,7 @@ class TestNodeBlackNode : public TestNode
 
   void testNaryExpForSize(Kind k, uint32_t n)
   {
-    NodeBuilder<> nbz(k);
+    NodeBuilder nbz(k);
     Node trueNode = d_nodeManager->mkConst(true);
     for (uint32_t i = 0; i < n; ++i)
     {
@@ -459,7 +459,7 @@ TEST_F(TestNodeBlackNode, getNumChildren)
 
 TEST_F(TestNodeBlackNode, iterator)
 {
-  NodeBuilder<> b;
+  NodeBuilder b;
   Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
   Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType());
   Node z = d_nodeManager->mkSkolem("z", d_nodeManager->booleanType());
@@ -518,8 +518,8 @@ TEST_F(TestNodeBlackNode, toString)
       "y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
   Node z = d_nodeManager->mkSkolem(
       "z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
-  Node m = NodeBuilder<>() << w << x << kind::OR;
-  Node n = NodeBuilder<>() << m << y << z << kind::AND;
+  Node m = NodeBuilder() << w << x << kind::OR;
+  Node n = NodeBuilder() << m << y << z << kind::AND;
 
   ASSERT_EQ(n.toString(), "(AND (OR w x) y z)");
 }
@@ -536,9 +536,9 @@ TEST_F(TestNodeBlackNode, toStream)
       "y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
   Node z = d_nodeManager->mkSkolem(
       "z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
-  Node m = NodeBuilder<>() << x << y << kind::OR;
-  Node n = NodeBuilder<>() << w << m << z << kind::AND;
-  Node o = NodeBuilder<>() << n << n << kind::XOR;
+  Node m = NodeBuilder() << x << y << kind::OR;
+  Node n = NodeBuilder() << w << m << z << kind::AND;
+  Node o = NodeBuilder() << n << n << kind::XOR;
 
   std::stringstream sstr;
   sstr << Node::dag(false);
@@ -764,7 +764,7 @@ TEST_F(TestNodeBlackNode, isConst)
 namespace {
 Node level0(NodeManager* nm)
 {
-  NodeBuilder<> nb(kind::AND);
+  NodeBuilder nb(kind::AND);
   Node x = nm->mkSkolem("x", nm->booleanType());
   nb << x;
   nb << x;
diff --git a/test/unit/node/node_builder_black.cpp b/test/unit/node/node_builder_black.cpp
index 39c5552df..8c6145940 100644
--- a/test/unit/node/node_builder_black.cpp
+++ b/test/unit/node/node_builder_black.cpp
@@ -39,8 +39,7 @@ namespace test {
 class TestNodeBlackNodeBuilder : public TestNode
 {
  protected:
-  template <unsigned N>
-  void push_back(NodeBuilder<N>& nb, uint32_t n)
+  void push_back(NodeBuilder& nb, uint32_t n)
   {
     for (uint32_t i = 0; i < n; ++i)
     {
@@ -54,189 +53,43 @@ class TestNodeBlackNodeBuilder : public TestNode
 TEST_F(TestNodeBlackNodeBuilder, ctors)
 {
   /* Default size tests. */
-  NodeBuilder<> def;
+  NodeBuilder def;
   ASSERT_EQ(def.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
   ASSERT_DEATH(def.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-  ASSERT_DEATH(def.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-  ASSERT_DEATH(def.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
 #endif
 
-  NodeBuilder<> spec(d_specKind);
+  NodeBuilder spec(d_specKind);
   ASSERT_EQ(spec.getKind(), d_specKind);
   ASSERT_EQ(spec.getNumChildren(), 0u);
-  ASSERT_EQ(spec.begin(), spec.end());
 
-  NodeBuilder<> from_nm(d_nodeManager.get());
+  NodeBuilder from_nm(d_nodeManager.get());
   ASSERT_EQ(from_nm.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
   ASSERT_DEATH(from_nm.getNumChildren(),
                "getKind\\(\\) != kind::UNDEFINED_KIND");
-  ASSERT_DEATH(from_nm.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-  ASSERT_DEATH(from_nm.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
 #endif
 
-  NodeBuilder<> from_nm_kind(d_nodeManager.get(), d_specKind);
+  NodeBuilder from_nm_kind(d_nodeManager.get(), d_specKind);
   ASSERT_EQ(from_nm_kind.getKind(), d_specKind);
   ASSERT_EQ(from_nm_kind.getNumChildren(), 0u);
-  ASSERT_EQ(from_nm_kind.begin(), from_nm_kind.end());
-
-  /* Non-default size tests */
-  NodeBuilder<K> ws;
-  ASSERT_EQ(ws.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
-  ASSERT_DEATH(ws.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-  ASSERT_DEATH(ws.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-  ASSERT_DEATH(ws.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-#endif
-
-  NodeBuilder<K> ws_kind(d_specKind);
-  ASSERT_EQ(ws_kind.getKind(), d_specKind);
-  ASSERT_EQ(ws_kind.getNumChildren(), 0u);
-  ASSERT_EQ(ws_kind.begin(), ws_kind.end());
-
-  NodeBuilder<K> ws_from_nm(d_nodeManager.get());
-  ASSERT_EQ(ws_from_nm.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
-  ASSERT_DEATH(ws_from_nm.getNumChildren(),
-               "getKind\\(\\) != kind::UNDEFINED_KIND");
-  ASSERT_DEATH(ws_from_nm.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-  ASSERT_DEATH(ws_from_nm.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-#endif
-
-  NodeBuilder<K> ws_from_nm_kind(d_nodeManager.get(), d_specKind);
-  ASSERT_EQ(ws_from_nm_kind.getKind(), d_specKind);
-  ASSERT_EQ(ws_from_nm_kind.getNumChildren(), 0u);
-  ASSERT_EQ(ws_from_nm_kind.begin(), ws_from_nm_kind.end());
-
-  /* Extreme size tests */
-  NodeBuilder<0> ws_size_0;
-
-  /* Allocating on the heap instead of the stack. */
-  NodeBuilder<LARGE_K>* ws_size_large = new NodeBuilder<LARGE_K>;
-  delete ws_size_large;
 
   /* Copy constructors */
-  NodeBuilder<> copy(def);
+  NodeBuilder copy(def);
   ASSERT_EQ(copy.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
   ASSERT_DEATH(copy.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-  ASSERT_DEATH(copy.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-  ASSERT_DEATH(copy.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-#endif
-
-  NodeBuilder<K> cp_ws(ws);
-  ASSERT_EQ(cp_ws.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
-  ASSERT_DEATH(cp_ws.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-  ASSERT_DEATH(cp_ws.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-  ASSERT_DEATH(cp_ws.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-#endif
-
-  NodeBuilder<K - 10> cp_from_larger(ws);
-  ASSERT_EQ(cp_from_larger.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
-  ASSERT_DEATH(cp_from_larger.getNumChildren(),
-               "getKind\\(\\) != kind::UNDEFINED_KIND");
-  ASSERT_DEATH(cp_from_larger.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-  ASSERT_DEATH(cp_from_larger.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-#endif
-
-  NodeBuilder<K + 10> cp_from_smaller(ws);
-  ASSERT_EQ(cp_from_smaller.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
-  ASSERT_DEATH(cp_from_smaller.getNumChildren(),
-               "getKind\\(\\) != kind::UNDEFINED_KIND");
-  ASSERT_DEATH(cp_from_smaller.begin(),
-               "getKind\\(\\) != kind::UNDEFINED_KIND");
-  ASSERT_DEATH(cp_from_smaller.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
 #endif
 }
 
 TEST_F(TestNodeBlackNodeBuilder, dtor)
 {
-  NodeBuilder<K>* nb = new NodeBuilder<K>();
-  delete nb;
-}
-
-TEST_F(TestNodeBlackNodeBuilder, begin_end)
-{
-  /* Test begin() and end() without resizing. */
-  NodeBuilder<K> ws(d_specKind);
-  ASSERT_EQ(ws.begin(), ws.end());
-
-  push_back(ws, K);
-  ASSERT_NE(ws.begin(), ws.end());
-
-  NodeBuilder<K>::iterator iter = ws.begin();
-  for (uint32_t i = 0; i < K; ++i)
-  {
-    ASSERT_NE(iter, ws.end());
-    ++iter;
-  }
-  ASSERT_EQ(iter, ws.end());
-
-  NodeBuilder<K>::const_iterator citer = ws.begin();
-  for (uint32_t i = 0; i < K; ++i)
-  {
-    ASSERT_NE(citer, ws.end());
-    ++citer;
-  }
-  ASSERT_EQ(citer, ws.end());
-
-  /* Repeat same tests and make sure that resizing occurs. */
-  NodeBuilder<> smaller(d_specKind);
-  ASSERT_EQ(smaller.begin(), smaller.end());
-
-  push_back(smaller, K);
-  ASSERT_NE(smaller.begin(), smaller.end());
-
-  NodeBuilder<>::iterator smaller_iter = smaller.begin();
-  for (uint32_t i = 0; i < K; ++i)
-  {
-    ASSERT_NE(smaller_iter, smaller.end());
-    ++smaller_iter;
-  }
-  ASSERT_EQ(iter, ws.end());
-
-  NodeBuilder<>::const_iterator smaller_citer = smaller.begin();
-  for (uint32_t i = 0; i < K; ++i)
-  {
-    ASSERT_NE(smaller_citer, smaller.end());
-    ++smaller_citer;
-  }
-  ASSERT_EQ(smaller_citer, smaller.end());
-}
-
-TEST_F(TestNodeBlackNodeBuilder, iterator)
-{
-  NodeBuilder<> b;
-  Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode);
-  Node y = d_nodeManager->mkSkolem("z", *d_boolTypeNode);
-  Node z = d_nodeManager->mkSkolem("y", *d_boolTypeNode);
-  b << x << y << z << AND;
-
-  {
-    NodeBuilder<>::iterator i = b.begin();
-    ASSERT_EQ(*i++, x);
-    ASSERT_EQ(*i++, y);
-    ASSERT_EQ(*i++, z);
-    ASSERT_EQ(i, b.end());
-  }
-
-  {
-    const NodeBuilder<>& c = b;
-    NodeBuilder<>::const_iterator i = c.begin();
-    ASSERT_EQ(*i++, x);
-    ASSERT_EQ(*i++, y);
-    ASSERT_EQ(*i++, z);
-    ASSERT_EQ(i, b.end());
-  }
+  std::unique_ptr<NodeBuilder> nb(new NodeBuilder());
 }
 
 TEST_F(TestNodeBlackNodeBuilder, getKind)
 {
-  NodeBuilder<> noKind;
+  NodeBuilder noKind;
   ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND);
 
   Node x(d_nodeManager->mkSkolem("x", *d_intTypeNode));
@@ -244,16 +97,14 @@ TEST_F(TestNodeBlackNodeBuilder, getKind)
   ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND);
 
   noKind << PLUS;
-
   ASSERT_EQ(noKind.getKind(), PLUS);
 
   Node n = noKind;
-
 #ifdef CVC4_ASSERTIONS
   ASSERT_DEATH(noKind.getKind(), "!isUsed\\(\\)");
 #endif
 
-  NodeBuilder<> spec(PLUS);
+  NodeBuilder spec(PLUS);
   ASSERT_EQ(spec.getKind(), PLUS);
   spec << x << x;
   ASSERT_EQ(spec.getKind(), PLUS);
@@ -263,12 +114,12 @@ TEST_F(TestNodeBlackNodeBuilder, getNumChildren)
 {
   Node x(d_nodeManager->mkSkolem("x", *d_intTypeNode));
 
-  NodeBuilder<> nb;
+  NodeBuilder nb;
 #ifdef CVC4_ASSERTIONS
   ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
 #endif
-  nb << PLUS << x << x;
 
+  nb << PLUS << x << x;
   ASSERT_EQ(nb.getNumChildren(), 2u);
 
   nb << x << x;
@@ -278,10 +129,11 @@ TEST_F(TestNodeBlackNodeBuilder, getNumChildren)
 #ifdef CVC4_ASSERTIONS
   ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
 #endif
+
   nb.clear(PLUS);
   ASSERT_EQ(nb.getNumChildren(), 0u);
-  nb << x << x << x;
 
+  nb << x << x << x;
   ASSERT_EQ(nb.getNumChildren(), 3u);
 
   nb << x << x << x;
@@ -296,7 +148,7 @@ TEST_F(TestNodeBlackNodeBuilder, getNumChildren)
 
 TEST_F(TestNodeBlackNodeBuilder, operator_square)
 {
-  NodeBuilder<> arr(d_specKind);
+  NodeBuilder arr(d_specKind);
 
   Node i_0 = d_nodeManager->mkConst(false);
   Node i_2 = d_nodeManager->mkConst(true);
@@ -308,18 +160,14 @@ TEST_F(TestNodeBlackNodeBuilder, operator_square)
 #endif
 
   arr << i_0;
-
   ASSERT_EQ(arr[0], i_0);
 
   push_back(arr, 1);
-
   arr << i_2;
-
   ASSERT_EQ(arr[0], i_0);
   ASSERT_EQ(arr[2], i_2);
 
   push_back(arr, K - 3);
-
   ASSERT_EQ(arr[0], i_0);
   ASSERT_EQ(arr[2], i_2);
   for (unsigned i = 3; i < K; ++i)
@@ -328,7 +176,6 @@ TEST_F(TestNodeBlackNodeBuilder, operator_square)
   }
 
   arr << i_K;
-
   ASSERT_EQ(arr[0], i_0);
   ASSERT_EQ(arr[2], i_2);
   for (unsigned i = 3; i < K; ++i)
@@ -345,72 +192,57 @@ TEST_F(TestNodeBlackNodeBuilder, operator_square)
 
 TEST_F(TestNodeBlackNodeBuilder, clear)
 {
-  NodeBuilder<> nb;
-
+  NodeBuilder nb;
   ASSERT_EQ(nb.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
   ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-  ASSERT_DEATH(nb.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-  ASSERT_DEATH(nb.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
 #endif
 
   nb << d_specKind;
   push_back(nb, K);
-
   ASSERT_EQ(nb.getKind(), d_specKind);
   ASSERT_EQ(nb.getNumChildren(), K);
-  ASSERT_NE(nb.begin(), nb.end());
 
   nb.clear();
-
   ASSERT_EQ(nb.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
   ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-  ASSERT_DEATH(nb.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-  ASSERT_DEATH(nb.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
 #endif
 
   nb << d_specKind;
   push_back(nb, K);
-
   ASSERT_EQ(nb.getKind(), d_specKind);
   ASSERT_EQ(nb.getNumChildren(), K);
-  ASSERT_NE(nb.begin(), nb.end());
 
   nb.clear(d_specKind);
-
   ASSERT_EQ(nb.getKind(), d_specKind);
   ASSERT_EQ(nb.getNumChildren(), 0u);
-  ASSERT_EQ(nb.begin(), nb.end());
 
   push_back(nb, K);
   nb.clear();
-
   ASSERT_EQ(nb.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
   ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-  ASSERT_DEATH(nb.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-  ASSERT_DEATH(nb.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
 #endif
 }
 
 TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_kind)
 {
 #ifdef CVC4_ASSERTIONS
-  NodeBuilder<> spec(d_specKind);
+  NodeBuilder spec(d_specKind);
   ASSERT_DEATH(spec << PLUS, "can't redefine the Kind of a NodeBuilder");
 #endif
 
-  NodeBuilder<> noSpec;
+  NodeBuilder noSpec;
   noSpec << d_specKind;
   ASSERT_EQ(noSpec.getKind(), d_specKind);
 
-  NodeBuilder<> modified;
+  NodeBuilder modified;
   push_back(modified, K);
   modified << d_specKind;
   ASSERT_EQ(modified.getKind(), d_specKind);
 
-  NodeBuilder<> nb(d_specKind);
+  NodeBuilder nb(d_specKind);
   nb << d_nodeManager->mkConst(true) << d_nodeManager->mkConst(false);
   nb.clear(PLUS);
 
@@ -424,20 +256,20 @@ TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_kind)
   ASSERT_DEATH(nb << PLUS, "can't redefine the Kind of a NodeBuilder");
 #endif
 
-  NodeBuilder<> testRef;
+  NodeBuilder testRef;
   ASSERT_EQ((testRef << d_specKind).getKind(), d_specKind);
 
 #ifdef CVC4_ASSERTIONS
-  NodeBuilder<> testTwo;
+  NodeBuilder testTwo;
   ASSERT_DEATH(testTwo << d_specKind << PLUS,
                "can't redefine the Kind of a NodeBuilder");
 #endif
 
-  NodeBuilder<> testMixOrder1;
+  NodeBuilder testMixOrder1;
   ASSERT_EQ(
       (testMixOrder1 << d_specKind << d_nodeManager->mkConst(true)).getKind(),
       d_specKind);
-  NodeBuilder<> testMixOrder2;
+  NodeBuilder testMixOrder2;
   ASSERT_EQ(
       (testMixOrder2 << d_nodeManager->mkConst(true) << d_specKind).getKind(),
       d_specKind);
@@ -445,30 +277,25 @@ TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_kind)
 
 TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_node)
 {
-  NodeBuilder<K> nb(d_specKind);
+  NodeBuilder nb(d_specKind);
   ASSERT_EQ(nb.getKind(), d_specKind);
   ASSERT_EQ(nb.getNumChildren(), 0u);
-  ASSERT_EQ(nb.begin(), nb.end());
   push_back(nb, K);
   ASSERT_EQ(nb.getKind(), d_specKind);
   ASSERT_EQ(nb.getNumChildren(), K);
-  ASSERT_NE(nb.begin(), nb.end());
 
 #ifdef CVC4_ASSERTIONS
   Node n = nb;
   ASSERT_DEATH(nb << n, "!isUsed\\(\\)");
 #endif
 
-  NodeBuilder<> overflow(d_specKind);
+  NodeBuilder overflow(d_specKind);
   ASSERT_EQ(overflow.getKind(), d_specKind);
   ASSERT_EQ(overflow.getNumChildren(), 0u);
-  ASSERT_EQ(overflow.begin(), overflow.end());
 
   push_back(overflow, 5 * K + 1);
-
   ASSERT_EQ(overflow.getKind(), d_specKind);
   ASSERT_EQ(overflow.getNumChildren(), 5 * K + 1);
-  ASSERT_NE(overflow.begin(), overflow.end());
 }
 
 TEST_F(TestNodeBlackNodeBuilder, append)
@@ -495,7 +322,7 @@ TEST_F(TestNodeBlackNodeBuilder, append)
                "Nodes with kind XOR must have at most 2 children");
 #endif
 
-  NodeBuilder<> b(d_specKind);
+  NodeBuilder b(d_specKind);
 
   /* test append(TNode) */
   b.append(n).append(o).append(q);
@@ -538,8 +365,8 @@ TEST_F(TestNodeBlackNodeBuilder, append)
 
 TEST_F(TestNodeBlackNodeBuilder, operator_node_cast)
 {
-  NodeBuilder<K> implicit(d_specKind);
-  NodeBuilder<K> explic(d_specKind);
+  NodeBuilder implicit(d_specKind);
+  NodeBuilder explic(d_specKind);
 
   push_back(implicit, K);
   push_back(explic, K);
@@ -560,7 +387,7 @@ TEST_F(TestNodeBlackNodeBuilder, operator_node_cast)
 
 TEST_F(TestNodeBlackNodeBuilder, leftist_building)
 {
-  NodeBuilder<> nb;
+  NodeBuilder nb;
 
   Node a = d_nodeManager->mkSkolem("a", *d_boolTypeNode);
 
diff --git a/test/unit/node/node_manager_white.cpp b/test/unit/node/node_manager_white.cpp
index dcdbc074f..66ac65cb5 100644
--- a/test/unit/node/node_manager_white.cpp
+++ b/test/unit/node/node_manager_white.cpp
@@ -41,7 +41,7 @@ TEST_F(TestNodeWhiteNodeManager, mkConst_rational)
 
 TEST_F(TestNodeWhiteNodeManager, oversized_node_builder)
 {
-  NodeBuilder<> nb;
+  NodeBuilder nb;
 
   ASSERT_NO_THROW(nb.realloc(15));
   ASSERT_NO_THROW(nb.realloc(25));
diff --git a/test/unit/node/node_white.cpp b/test/unit/node/node_white.cpp
index 20de9d3e4..9e3c4bb7d 100644
--- a/test/unit/node/node_white.cpp
+++ b/test/unit/node/node_white.cpp
@@ -17,6 +17,7 @@
 #include <string>
 
 #include "base/check.h"
+#include "expr/node_builder.h"
 #include "test_node.h"
 
 namespace cvc5 {
@@ -36,7 +37,7 @@ TEST_F(TestNodeWhiteNode, copy_ctor) { Node e(Node::s_null); }
 
 TEST_F(TestNodeWhiteNode, builder)
 {
-  NodeBuilder<> b;
+  NodeBuilder b;
   ASSERT_TRUE(b.d_nv->getId() == 0);
   ASSERT_TRUE(b.d_nv->getKind() == UNDEFINED_KIND);
   ASSERT_EQ(b.d_nv->d_nchildren, 0u);
diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp
index d313e01c7..6f0398439 100644
--- a/test/unit/preprocessing/pass_bv_gauss_white.cpp
+++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp
@@ -2046,16 +2046,16 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_nary_partial)
           bv::utils::mkExtract(
               d_nodeManager->mkNode(kind::BITVECTOR_CONCAT, zero, zz), 7, 0)));
 
-  NodeBuilder<> nbx(d_nodeManager.get(), kind::BITVECTOR_MULT);
+  NodeBuilder nbx(d_nodeManager.get(), kind::BITVECTOR_MULT);
   nbx << d_x << d_one << x;
   Node x_mul_one_mul_xx = nbx.constructNode();
-  NodeBuilder<> nby(d_nodeManager.get(), kind::BITVECTOR_MULT);
+  NodeBuilder nby(d_nodeManager.get(), kind::BITVECTOR_MULT);
   nby << d_y << y << d_one;
   Node y_mul_yy_mul_one = nby.constructNode();
-  NodeBuilder<> nbz(d_nodeManager.get(), kind::BITVECTOR_MULT);
+  NodeBuilder nbz(d_nodeManager.get(), kind::BITVECTOR_MULT);
   nbz << d_three << d_z << z;
   Node three_mul_z_mul_zz = nbz.constructNode();
-  NodeBuilder<> nbz2(d_nodeManager.get(), kind::BITVECTOR_MULT);
+  NodeBuilder nbz2(d_nodeManager.get(), kind::BITVECTOR_MULT);
   nbz2 << d_z << d_nine << z;
   Node z_mul_nine_mul_zz = nbz2.constructNode();
 
@@ -2671,20 +2671,20 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw1)
   Node mult2x = d_nodeManager->mkNode(kind::BITVECTOR_MULT, zext40x, zext40x);
   ASSERT_EQ(BVGauss::getMinBwExpr(mult2x), 32);
 
-  NodeBuilder<> nbmult3p(kind::BITVECTOR_MULT);
+  NodeBuilder nbmult3p(kind::BITVECTOR_MULT);
   nbmult3p << zext48p << zext48p << zext48p;
   Node mult3p = nbmult3p;
   ASSERT_EQ(BVGauss::getMinBwExpr(mult3p), 11);
-  NodeBuilder<> nbmult3x(kind::BITVECTOR_MULT);
+  NodeBuilder nbmult3x(kind::BITVECTOR_MULT);
   nbmult3x << zext48x << zext48x << zext48x;
   Node mult3x = nbmult3x;
   ASSERT_EQ(BVGauss::getMinBwExpr(mult3x), 48);
 
-  NodeBuilder<> nbmult4p(kind::BITVECTOR_MULT);
+  NodeBuilder nbmult4p(kind::BITVECTOR_MULT);
   nbmult4p << zext48p << zext48p8 << zext48p;
   Node mult4p = nbmult4p;
   ASSERT_EQ(BVGauss::getMinBwExpr(mult4p), 11);
-  NodeBuilder<> nbmult4x(kind::BITVECTOR_MULT);
+  NodeBuilder nbmult4x(kind::BITVECTOR_MULT);
   nbmult4x << zext48x << zext48x8 << zext48x;
   Node mult4x = nbmult4x;
   ASSERT_EQ(BVGauss::getMinBwExpr(mult4x), 40);
@@ -2739,29 +2739,29 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw1)
   Node add3x = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, zext48x8, zext48x);
   ASSERT_EQ(BVGauss::getMinBwExpr(add3x), 17);
 
-  NodeBuilder<> nbadd4p(kind::BITVECTOR_PLUS);
+  NodeBuilder nbadd4p(kind::BITVECTOR_PLUS);
   nbadd4p << zext48p << zext48p << zext48p;
   Node add4p = nbadd4p;
   ASSERT_EQ(BVGauss::getMinBwExpr(add4p), 6);
-  NodeBuilder<> nbadd4x(kind::BITVECTOR_PLUS);
+  NodeBuilder nbadd4x(kind::BITVECTOR_PLUS);
   nbadd4x << zext48x << zext48x << zext48x;
   Node add4x = nbadd4x;
   ASSERT_EQ(BVGauss::getMinBwExpr(add4x), 18);
 
-  NodeBuilder<> nbadd5p(kind::BITVECTOR_PLUS);
+  NodeBuilder nbadd5p(kind::BITVECTOR_PLUS);
   nbadd5p << zext48p << zext48p8 << zext48p;
   Node add5p = nbadd5p;
   ASSERT_EQ(BVGauss::getMinBwExpr(add5p), 6);
-  NodeBuilder<> nbadd5x(kind::BITVECTOR_PLUS);
+  NodeBuilder nbadd5x(kind::BITVECTOR_PLUS);
   nbadd5x << zext48x << zext48x8 << zext48x;
   Node add5x = nbadd5x;
   ASSERT_EQ(BVGauss::getMinBwExpr(add5x), 18);
 
-  NodeBuilder<> nbadd6p(kind::BITVECTOR_PLUS);
+  NodeBuilder nbadd6p(kind::BITVECTOR_PLUS);
   nbadd6p << zext48p << zext48p << zext48p << zext48p;
   Node add6p = nbadd6p;
   ASSERT_EQ(BVGauss::getMinBwExpr(add6p), 6);
-  NodeBuilder<> nbadd6x(kind::BITVECTOR_PLUS);
+  NodeBuilder nbadd6x(kind::BITVECTOR_PLUS);
   nbadd6x << zext48x << zext48x << zext48x << zext48x;
   Node add6x = nbadd6x;
   ASSERT_EQ(BVGauss::getMinBwExpr(add6x), 18);
diff --git a/test/unit/util/boolean_simplification_black.cpp b/test/unit/util/boolean_simplification_black.cpp
index baacbce5a..97bbb1bcf 100644
--- a/test/unit/util/boolean_simplification_black.cpp
+++ b/test/unit/util/boolean_simplification_black.cpp
@@ -152,8 +152,8 @@ TEST_F(TestUtilBlackBooleanSimplification, simplifyClause)
                              d_hfc,
                              d_ac,
                              d_d.andNode(d_b));
-  out = NodeBuilder<>(kind::OR) << d_fa << d_ga.orNode(d_c).notNode() << d_hfc
-                                << d_ac << d_d.andNode(d_b);
+  out = NodeBuilder(kind::OR) << d_fa << d_ga.orNode(d_c).notNode() << d_hfc
+                              << d_ac << d_d.andNode(d_b);
   test_nodes_equal(out, BooleanSimplification::simplifyClause(in));
 
   in = d_nodeManager->mkNode(kind::OR,
@@ -162,8 +162,8 @@ TEST_F(TestUtilBlackBooleanSimplification, simplifyClause)
                              d_hfc,
                              d_ac,
                              d_d.andNode(d_b));
-  out = NodeBuilder<>(kind::OR) << d_fa << d_ga.notNode() << d_c.notNode()
-                                << d_hfc << d_ac << d_d.andNode(d_b);
+  out = NodeBuilder(kind::OR) << d_fa << d_ga.notNode() << d_c.notNode()
+                              << d_hfc << d_ac << d_d.andNode(d_b);
   test_nodes_equal(out, BooleanSimplification::simplifyClause(in));
 
 #ifdef CVC4_ASSERTIONS
@@ -207,7 +207,7 @@ TEST_F(TestUtilBlackBooleanSimplification, simplifyHornClause)
                             d_ga.orNode(d_c).notNode(),
                             d_hfc.orNode(d_ac),
                             d_d.andNode(d_b).notNode()));
-  out = NodeBuilder<>(kind::OR)
+  out = NodeBuilder(kind::OR)
         << d_a.notNode() << d_b.notNode() << d_fa << d_ga.orNode(d_c).notNode()
         << d_hfc << d_ac << d_d.notNode();
   test_nodes_equal(out, BooleanSimplification::simplifyHornClause(in));
@@ -237,8 +237,8 @@ TEST_F(TestUtilBlackBooleanSimplification, simplifyConflict)
                              d_fa,
                              d_hfc.orNode(d_ac),
                              d_d.andNode(d_b));
-  out = NodeBuilder<>(kind::AND) << d_fa << d_ga.notNode() << d_c.notNode()
-                                 << d_hfc.orNode(d_ac) << d_d << d_b;
+  out = NodeBuilder(kind::AND) << d_fa << d_ga.notNode() << d_c.notNode()
+                               << d_hfc.orNode(d_ac) << d_d << d_b;
   test_nodes_equal(out, BooleanSimplification::simplifyConflict(in));
 
 #ifdef CVC4_ASSERTIONS