This fixes regressions at levels >= 1 which were failing

* implement zombification and garbage collection of NodeValues
  (but GC not turned on yet)

* implement removal of key nodes from all attribute tables

* audit NodeBuilder and fix memory leaks and improper reference-count
  management.  This is in many places a re-write.  Clearly documented
  invariants on NodeBuilder state.  (Closes Bug 38)

* created a "BackedNodeBuilder" that can be used to construct
  NodeBuilders with a stack-based backing store for a size that's not
  a compile-time constant.

* NodeValues no longer depend on Node for toStream()'ing

* make unit test-building "silent" with --enable-silent-rules

* (Makefile.am, Makefile.builds.in) fix top-level build system so that
  "make regressN" works with unbuilt/out-of-date source trees in the
  expected way.

* (various) code cleanup, documentation, formatting

16 files changed, 1289 insertions, 458 deletions

diff --git a/Makefile.am b/Makefile.am
index 6f077bb47..5aec4e904 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -8,6 +8,6 @@ ACLOCAL_AMFLAGS = -I config
 SUBDIRS = src test contrib
 
 .PHONY: regress0 regress1 regress2 regress3
-regress0 regress1 regress2 regress3:
+regress0 regress1 regress2 regress3: all
 	(cd test && $(MAKE) $(AM_MAKEFLAGS) $@) || exit 1
 
diff --git a/Makefile.builds.in b/Makefile.builds.in
index f26111c4f..1cf9c1a52 100644
--- a/Makefile.builds.in
+++ b/Makefile.builds.in
@@ -85,6 +85,9 @@ endif
 	test -e lib || ln -sfv ".$(libdir)" lib
 	test -e bin || ln -sfv ".$(bindir)" bin
 
+regress0 regress1 regress2 regress3: all
+	(cd $(CURRENT_BUILD) && $(MAKE) $@)
+
 # any other target than the default doesn't do the extra stuff above
 %:
 	(cd $(CURRENT_BUILD) && $(MAKE) $@)
diff --git a/src/context/cdmap.h b/src/context/cdmap.h
index 994ff76b4..dc3448e52 100644
--- a/src/context/cdmap.h
+++ b/src/context/cdmap.h
@@ -244,16 +244,17 @@ public:
     emptyTrash();
 
     typename __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn>::iterator
-      i(d_map.find(k));
+      i = d_map.find(k);
 
-    if(i == d_map.end()) { // Create new object
+    if(i == d_map.end()) {// create new object
       CDOmap<Key, Data, HashFcn>*
-	obj(new(true) CDOmap<Key, Data, HashFcn>(d_context, this, k, d));
+	obj = new(true) CDOmap<Key, Data, HashFcn>(d_context, this, k, d);
       d_map[k] = obj;
     } else {
       (*i).second->set(d);
     }
   }
+
   // FIXME: no erase(), too much hassle to implement efficiently...
 
   // Iterator for CDMap: points to pair<const Key, CDOMap<Key, Data, HashFcn>&>;
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index bd02cf452..3deed9a52 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -15,6 +15,7 @@ libexpr_la_SOURCES = \
 	node_manager.h \
 	expr_manager.h \
 	attribute.h \
+	attribute.cpp \
 	@srcdir@/kind.h \
 	node_builder.cpp \
 	node_manager.cpp \
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
new file mode 100644
index 000000000..e8e93f6ff
--- /dev/null
+++ b/src/expr/attribute.cpp
@@ -0,0 +1,61 @@
+/*********************                                                        */
+/** attribute.cpp
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** AttributeManager implementation.
+ **/
+
+#include "expr/attribute.h"
+#include "expr/node_value.h"
+#include "util/output.h"
+
+namespace CVC4 {
+namespace expr {
+namespace attr {
+
+void AttributeManager::deleteAllAttributes(NodeValue* nv) {
+  d_bools.erase(nv);
+  for(unsigned id = 0; id < attr::LastAttributeId<uint64_t, false>::s_id; ++id) {
+    d_ints.erase(std::make_pair(id, nv));
+  }
+  for(unsigned id = 0; id < attr::LastAttributeId<TNode, false>::s_id; ++id) {
+    d_exprs.erase(std::make_pair(id, nv));
+  }
+  for(unsigned id = 0; id < attr::LastAttributeId<std::string, false>::s_id; ++id) {
+    d_strings.erase(std::make_pair(id, nv));
+  }
+  for(unsigned id = 0; id < attr::LastAttributeId<void*, false>::s_id; ++id) {
+    d_ptrs.erase(std::make_pair(id, nv));
+  }
+
+  // FIXME CD-bools in optimized table
+        /*
+  for(unsigned id = 0; id < attr::LastAttributeId<bool, true>::s_id; ++id) {
+    d_cdbools.erase(std::make_pair(id, nv));
+  }
+  for(unsigned id = 0; id < attr::LastAttributeId<uint64_t, true>::s_id; ++id) {
+    d_cdints.erase(std::make_pair(id, nv));
+  }
+  for(unsigned id = 0; id < attr::LastAttributeId<TNode, true>::s_id; ++id) {
+    d_cdexprs.erase(std::make_pair(id, nv));
+  }
+  for(unsigned id = 0; id < attr::LastAttributeId<std::string, true>::s_id; ++id) {
+    d_cdstrings.erase(std::make_pair(id, nv));
+  }
+  for(unsigned id = 0; id < attr::LastAttributeId<void*, true>::s_id; ++id) {
+    d_cdptrs.erase(std::make_pair(id, nv));
+  }
+        */
+}
+
+}/* CVC4::expr::attr namespace */
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 285c7ce87..4dc050648 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -342,6 +342,14 @@ public:
     uint64_t& word = super::operator[](k.second);
     return BitAccessor(word, k.first);
   }
+
+  /**
+   * Delete all flags from the given node.
+   */
+  void erase(NodeValue* nv) {
+    super::erase(nv);
+  }
+
 };/* class AttrHash<bool> */
 
 /**
@@ -363,6 +371,17 @@ public:
   }
 };
 
+/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
+/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
+/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
+/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
+/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
+/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
+/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
+/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
+/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
+/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
+
 }/* CVC4::expr::attr namespace */
 
 // ATTRIBUTE CLEANUP FUNCTIONS =================================================
@@ -562,6 +581,9 @@ namespace attr {
  */
 class AttributeManager {
 
+  // IF YOU ADD ANY TABLES, don't forget to add them also to the
+  // implementation of deleteAllAttributes().
+
   /** Underlying hash table for boolean-valued attributes */
   AttrHash<bool> d_bools;
   /** Underlying hash table for integral-valued attributes */
@@ -573,6 +595,9 @@ class AttributeManager {
   /** Underlying hash table for pointer-valued attributes */
   AttrHash<void*> d_ptrs;
 
+  // IF YOU ADD ANY TABLES, don't forget to add them also to the
+  // implementation of deleteAllAttributes().
+
   /** Underlying hash table for context-dependent boolean-valued attributes */
   CDAttrHash<bool> d_cdbools;
   /** Underlying hash table for context-dependent integral-valued attributes */
@@ -605,7 +630,7 @@ public:
   /**
    * Get a particular attribute on a particular node.
    *
-   * @param n the node about which to inquire
+   * @param nv the node about which to inquire
    *
    * @param const AttrKind& the attribute kind to get
    *
@@ -613,7 +638,7 @@ public:
    * AttrKind::value_type if not.
    */
   template <class AttrKind>
-  typename AttrKind::value_type getAttribute(TNode n,
+  typename AttrKind::value_type getAttribute(NodeValue* nv,
                                              const AttrKind&) const;
 
   // Note that there are two, distinct hasAttribute() declarations for
@@ -624,21 +649,21 @@ public:
   /**
    * Determine if a particular attribute exists for a particular node.
    *
-   * @param n the node about which to inquire
+   * @param nv the node about which to inquire
    *
    * @param const AttrKind& the attribute kind to inquire about
    *
    * @return true if the given node has the given attribute
    */
   template <class AttrKind>
-  bool hasAttribute(TNode n,
+  bool hasAttribute(NodeValue* nv,
                     const AttrKind&) const;
 
   /**
    * Determine if a particular attribute exists for a particular node,
    * and get it if it does.
    *
-   * @param n the node about which to inquire
+   * @param nv the node about which to inquire
    *
    * @param const AttrKind& the attribute kind to inquire about
    *
@@ -648,14 +673,14 @@ public:
    * @return true if the given node has the given attribute
    */
   template <class AttrKind>
-  bool hasAttribute(TNode n,
+  bool hasAttribute(NodeValue* nv,
                     const AttrKind&,
                     typename AttrKind::value_type& ret) const;
 
   /**
    * Set a particular attribute on a particular node.
    *
-   * @param n the node for which to set the attribute
+   * @param nv the node for which to set the attribute
    *
    * @param const AttrKind& the attribute kind to set
    *
@@ -665,9 +690,16 @@ public:
    * @return true if the given node has the given attribute
    */
   template <class AttrKind>
-  void setAttribute(TNode n,
+  void setAttribute(NodeValue* nv,
                     const AttrKind&,
                     const typename AttrKind::value_type& value);
+
+  /**
+   * Remove all attributes associated to the given node.
+   *
+   * @param nv the node from which to delete attributes
+   */
+  void deleteAllAttributes(NodeValue* nv);
 };
 
 }/* CVC4::expr::attr namespace */
@@ -835,7 +867,7 @@ namespace attr {
 
 // implementation for AttributeManager::getAttribute()
 template <class AttrKind>
-typename AttrKind::value_type AttributeManager::getAttribute(TNode n,
+typename AttrKind::value_type AttributeManager::getAttribute(NodeValue* nv,
                                                              const AttrKind&) const {
 
   typedef typename AttrKind::value_type value_type;
@@ -843,7 +875,7 @@ typename AttrKind::value_type AttributeManager::getAttribute(TNode n,
   typedef typename getTable<value_type, AttrKind::context_dependent>::table_type table_type;
 
   const table_type& ah = getTable<value_type, AttrKind::context_dependent>::get(*this);
-  typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), n.d_nv));
+  typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv));
 
   if(i == ah.end()) {
     return typename AttrKind::value_type();
@@ -937,20 +969,20 @@ struct HasAttribute<false, AttrKind> {
 };
 
 template <class AttrKind>
-bool AttributeManager::hasAttribute(TNode n,
+bool AttributeManager::hasAttribute(NodeValue* nv,
                                     const AttrKind&) const {
-  return HasAttribute<AttrKind::has_default_value, AttrKind>::hasAttribute(this, n.d_nv);
+  return HasAttribute<AttrKind::has_default_value, AttrKind>::hasAttribute(this, nv);
 }
 
 template <class AttrKind>
-bool AttributeManager::hasAttribute(TNode n,
+bool AttributeManager::hasAttribute(NodeValue* nv,
                                     const AttrKind&,
                                     typename AttrKind::value_type& ret) const {
-  return HasAttribute<AttrKind::has_default_value, AttrKind>::hasAttribute(this, n.d_nv, ret);
+  return HasAttribute<AttrKind::has_default_value, AttrKind>::hasAttribute(this, nv, ret);
 }
 
 template <class AttrKind>
-inline void AttributeManager::setAttribute(TNode n,
+inline void AttributeManager::setAttribute(NodeValue* nv,
                                            const AttrKind&,
                                            const typename AttrKind::value_type& value) {
 
@@ -959,7 +991,7 @@ inline void AttributeManager::setAttribute(TNode n,
   typedef typename getTable<value_type, AttrKind::context_dependent>::table_type table_type;
 
   table_type& ah = getTable<value_type, AttrKind::context_dependent>::get(*this);
-  ah[std::make_pair(AttrKind::getId(), n.d_nv)] = mapping::convert(value);
+  ah[std::make_pair(AttrKind::getId(), nv)] = mapping::convert(value);
 }
 
 }/* CVC4::expr::attr namespace */
diff --git a/src/expr/node.h b/src/expr/node.h
index f9bbcb5a5..c1df399a1 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -99,8 +99,8 @@ class NodeTemplate {
   friend class NodeTemplate<false>;
   friend class NodeManager;
 
-  template <unsigned>
-  friend class NodeBuilder;
+  template <class Builder>
+  friend class NodeBuilderBase;
 
   friend class ::CVC4::expr::attr::AttributeManager;
 
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 5c01a3b0f..a92c3a872 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -10,7 +10,195 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** A builder interface for nodes.
+ ** A builder interface for Nodes.
+ **
+ ** The idea is to permit a flexible and efficient (in the common
+ ** case) interface for building Nodes.  The general pattern of use is
+ ** to create a NodeBuilder, set its kind, append children to it, then
+ ** "extract" the resulting Node.  This resulting Node may be one that
+ ** already exists (the NodeManager keeps a table of all Nodes in the
+ ** system), or may be entirely new.
+ **
+ ** This implementation gets a bit hairy for a handful of reasons.  We
+ ** want a user-supplied "in-line" buffer (probably on the stack, see
+ ** below) to hold the children, but then the number of children must
+ ** be known ahead of time.  Therefore, if this buffer is overrun, we
+ ** need to heap-allocate a new buffer to hold the children.
+ **
+ ** Note that as children are added to a NodeBuilder, they are stored
+ ** as raw pointers-to-NodeValue.  However, their reference counts are
+ ** carefully maintained.
+ **
+ ** When the "in-line" buffer "d_inlineNv" is superceded by a
+ ** heap-allocated buffer, we allocate the new buffer (a NodeValue
+ ** large enough to hold more children), copy the elements to it, and
+ ** mark d_inlineNv as having zero children.  We do this last bit so
+ ** that we don't have to modify any child reference counts.  The new
+ ** heap-allocated buffer "takes over" the reference counts of the old
+ ** "in-line" buffer.  (If we didn't mark it as having zero children,
+ ** the destructor may improperly decrement the children's reference
+ ** counts.)
+ **
+ ** There are then four normal cases at the end of a NodeBuilder's
+ ** life cycle:
+ **
+ **   0. We have a VARIABLE-kinded Node.  These are special (they have
+ **      no children and are all distinct by definition).  They are
+ **      really a subcase of 1(b), below.
+ **   1. d_nv points to d_inlineNv: it is the backing store supplied
+ **      by the user (or derived class).
+ **      (a) The Node under construction already exists in the
+ **          NodeManager's pool.
+ **      (b) The Node under construction is NOT already in the
+ **          NodeManager's pool.
+ **   2. d_nv does NOT point to d_inlineNv: it is a new, larger buffer
+ **      that was heap-allocated by this NodeBuilder.
+ **      (a) The Node under construction already exists in the
+ **          NodeManager's pool.
+ **      (b) The Node under construction is NOT already in the
+ **          NodeManager's pool.
+ **
+ ** When a Node is extracted (see the non-const version of
+ ** NodeBuilderBase<>::operator Node()), we convert the NodeBuilder to
+ ** a Node and make sure the reference counts are properly maintained.
+ ** That means we must ensure there are no reference-counting errors
+ ** among the node's children, that the children aren't re-decremented
+ ** on clear() or NodeBuilder destruction, and that the returned Node
+ ** wraps a NodeValue with a reference count of 1.
+ **
+ **   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.
+ **
+ **   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.
+ **
+ **   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.
+ **
+ **   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.
+ **
+ **   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.
+ **
+ ** NOTE IN 1(b) AND 2(b) THAT we can NOT create Node wrapper
+ ** temporary for the NodeValue in the NodeBuilderBase<>::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, which makes it eligible for collection before the
+ ** builder has even returned it!  So this is a no-no.
+ **
+ ** For the _const_ version of NodeBuilderBase<>::operator Node(), no
+ ** reference-count modifications or anything else can take place!
+ ** Therefore, we have a slightly more expensive version:
+ **
+ **   0.    If a VARIABLE, treat similarly to 1(b), except that we
+ **         know there are no children, and we don't keep
+ **         VARIABLE-kinded Nodes in the NodeManager pool.
+ **
+ **   1(a). The existing NodeManager pool entry is returned; we leave
+ **         child reference counts alone and get them at NodeBuilder
+ **         destruction time.
+ **
+ **   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.
+ **
+ **   2(a). The existing NodeManager pool entry is returned; we leave
+ **         child reference counts alone and get them at NodeBuilder
+ **         destruction time.
+ **
+ **   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.
+ **
+ ** There are also two cases when the NodeBuilder is clear()'ed:
+ **
+ **   1. d_nv == &d_inlineNv (NodeBuilder using the user-supplied
+ **      backing store): all d_inlineNv children have their reference
+ **      counts decremented, d_inlineNv.d_nchildren is set to zero,
+ **      and its kind is set to UNDEFINED_KIND.
+ **
+ **   2. d_nv != &d_inlineNv (d_nv heap-allocated by NodeBuilder): all
+ **      d_nv children have their reference counts decremented, d_nv
+ **      is deallocated, and d_nv is set to &d_inlineNv.  d_inlineNv's
+ **      kind is set to UNDEFINED_KIND.
+ **
+ ** ... destruction is similar:
+ **
+ **   1. d_nv == &d_inlineNv (NodeBuilder using the user-supplied
+ **      backing store): all d_inlineNv children have their reference
+ **      counts decremented.
+ **
+ **   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 three classes (two of them are templates):
+ **
+ **   template <class Builder> class NodeBuilderBase;
+ **
+ **     This is the base class for node builders.  It can not be used
+ **     directly.  It contains a shared implementation but is intended
+ **     to be subclassed.  Derived classes supply its "in-line" buffer.
+ **
+ **   class BackedNodeBuilder;
+ **
+ **     This is the usable form for a user-supplied-backing-store node
+ **     builder.  A user can allocate a buffer large enough for a
+ **     NodeValue with N children (say, on the stack), then pass a
+ **     pointer to this buffer, and the parameter N, to a
+ **     BackedNodeBuilder.  It will use this buffer to build its
+ **     NodeValue until the number of children exceeds N; then it will
+ **     allocate d_nv on the heap.
+ **
+ **     To ensure that the buffer is properly-sized, it is recommended
+ **     to use the makeStackNodeBuilder(b, N) macro to make a
+ **     BackedNodeBuilder "b" with a stack-allocated buffer large
+ **     enough to hold N children.
+ **
+ **   template <unsigned nchild_thresh> class NodeBuilder;
+ **
+ **     This is the conceptually easiest form of NodeBuilder to use.
+ **     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 (which is why the BackedNodeBuilder
+ **     creator-macro "makeStackNodeBuilder(b, N)" is sometimes
+ **     preferred).
  **/
 
 #include "cvc4_private.h"
@@ -28,8 +216,8 @@
 namespace CVC4 {
   static const unsigned default_nchild_thresh = 10;
 
-  template <unsigned nchild_thresh = default_nchild_thresh>
-  class NodeBuilder;
+  template <class Builder>
+  class NodeBuilderBase;
 
   class NodeManager;
 }/* CVC4 namespace */
@@ -41,196 +229,459 @@ namespace CVC4 {
 
 namespace CVC4 {
 
-template <unsigned nchild_thresh>
-inline std::ostream& operator<<(std::ostream&, const NodeBuilder<nchild_thresh>&);
+template <class Builder>
+inline std::ostream& operator<<(std::ostream&, const NodeBuilderBase<Builder>&);
 
 class AndNodeBuilder;
 class OrNodeBuilder;
 class PlusNodeBuilder;
 class MultNodeBuilder;
 
-template <unsigned nchild_thresh>
-class NodeBuilder {
+/**
+ * A base class for NodeBuilders.  When extending this class, use:
+ *
+ *   class MyExtendedNodeBuilder : public NodeBuilderBase<MyExtendedNodeBuilder> { ... };
+ *
+ * This ensures that certain member functions return the right
+ * (derived) class type.
+ *
+ * There are no virtual functions here, and that should remain the
+ * case!  This class is just used for sharing of implementation.  Two
+ * types derive from it: BackedNodeBuilder (which allows for an
+ * external buffer), and the NodeBuilder<> template, which requires
+ * that you give it a compile-time constant backing-store size.
+ */
+template <class Builder>
+class NodeBuilderBase {
+protected:
 
-  unsigned d_size;
+  /**
+   * A reference to an "in-line" stack-allocated buffer for use by the
+   * NodeBuilder.
+   */
+  expr::NodeValue& d_inlineNv;
 
-  uint64_t d_hash;
+  /**
+   * 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;
 
-  // initially false, when you extract the Node this is set and you can't
-  // extract another
-  bool d_used;
+  /**
+   * The maximum number of children that can be held in this "in-line"
+   * buffer.
+   */
+  const uint16_t d_inlineNvMaxChildren;
 
-  expr::NodeValue* d_nv;
-  expr::NodeValue d_inlineNv;
-  expr::NodeValue *d_childrenStorage[nchild_thresh];
+  /**
+   * The number of children allocated in d_nv.
+   */
+  uint16_t d_nvMaxChildren;
 
-  bool nvIsAllocated() const {
-    return d_nv->d_nchildren > nchild_thresh;
+  /**
+   * Returns whether or not this NodeBuilder has been "used"---i.e.,
+   * whether a Node has been extracted with [the non-const version of]
+   * operator Node().  Internally, this state is represented by d_nv
+   * pointing to NULL.
+   */
+  inline bool isUsed() const {
+    return EXPECT_FALSE( d_nv == NULL );
   }
 
-  template <unsigned N>
-  bool nvIsAllocated(const NodeBuilder<N>& nb) const {
-    return nb.d_nv->d_nchildren > N;
+  /**
+   * 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 == d_inlineNvMaxChildren,
+           "Internal error: bad `inline' state in NodeBuilder!");
+    d_nv = NULL;
   }
 
-  bool evNeedsToBeAllocated() const {
-    return d_nv->d_nchildren == d_size;
+  /**
+   * 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 == d_inlineNvMaxChildren,
+           "Internal error: bad `inline' state in NodeBuilder!");
+    d_nv = &d_inlineNv;
   }
 
-  // realloc in the default way
-  void realloc();
+  /**
+   * Returns true if d_nv is *not* the "in-line" one (it was
+   * heap-allocated by this class).
+   */
+  inline bool nvIsAllocated() const {
+    return EXPECT_FALSE( d_nv != &d_inlineNv ) && EXPECT_TRUE( d_nv != NULL );
+  }
 
-  // realloc to a specific size
-  void realloc(size_t toSize, bool copy = true);
+  /**
+   * Returns true if adding a child requires (re)allocation of d_nv
+   * first.
+   */
+  inline bool nvNeedsToBeAllocated() const {
+    return EXPECT_FALSE( d_nv->d_nchildren == d_nvMaxChildren );
+  }
 
-  void allocateEvIfNecessaryForAppend() {
-    if(EXPECT_FALSE( evNeedsToBeAllocated() )) {
+  /**
+   * (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() {
+    realloc(d_nvMaxChildren * 2);
+  }
+
+  /**
+   * (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(EXPECT_FALSE( nvNeedsToBeAllocated() )) {
       realloc();
     }
   }
 
-  // dealloc: only call this with d_used == false and nvIsAllocated()
-  inline void dealloc();
+  /**
+   * 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() {
-    Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
-    if(EXPECT_FALSE( nvIsAllocated() ) && EXPECT_TRUE( d_size > d_nv->d_nchildren )) {
-      d_nv = (expr::NodeValue*)
-        std::realloc(d_nv, sizeof(expr::NodeValue) +
-                     ( sizeof(expr::NodeValue*) * (d_size = d_nv->d_nchildren) ));
-      if(d_nv == NULL) {
+    if(EXPECT_FALSE( nvIsAllocated() ) &&
+       EXPECT_TRUE( d_nvMaxChildren > d_nv->d_nchildren )) {
+      // 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_nvMaxChildren = 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;
     }
   }
 
-  NodeBuilder& collapseTo(Kind k) {
-    Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
+  Builder& collapseTo(Kind k) {
     AssertArgument(k != kind::UNDEFINED_KIND && k != kind::NULL_EXPR,
                    k, "illegal collapsing kind");
 
     if(getKind() != k) {
-      Node n = *this;
+      Node n = operator Node();
       clear();
-      d_nv->d_kind = k;
-      append(n);
+      d_nv->d_kind = expr::NodeValue::kindToDKind(k);
+      return append(n);
     }
-    return *this;
+    return static_cast<Builder&>(*this);
   }
 
+protected:
+
+  inline NodeBuilderBase(char* buf, unsigned maxChildren,
+                         Kind k = kind::UNDEFINED_KIND);
+  inline NodeBuilderBase(char* buf, unsigned maxChildren,
+                         NodeManager* nm, Kind k = kind::UNDEFINED_KIND);
+
+private:
+  // disallow copy or assignment of these base classes directly (there
+  // would be no backing store!)
+  NodeBuilderBase(const NodeBuilderBase& nb);
+  NodeBuilderBase& operator=(const NodeBuilderBase& nb);
+
 public:
 
-  inline NodeBuilder();
-  inline NodeBuilder(Kind k);
-  inline NodeBuilder(const NodeBuilder<nchild_thresh>& nb);
-  template <unsigned N> inline NodeBuilder(const NodeBuilder<N>& nb);
-  inline NodeBuilder(NodeManager* nm);
-  inline NodeBuilder(NodeManager* nm, Kind k);
-  inline ~NodeBuilder();
+  // Intentionally not virtual; we don't want a vtable.  Don't
+  // override this in a derived class.
+  inline ~NodeBuilderBase();
 
   typedef expr::NodeValue::iterator<true> iterator;
   typedef expr::NodeValue::iterator<true> const_iterator;
 
-  const_iterator begin() const {
-    Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
+  /** 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");
     return d_nv->begin<true>();
   }
 
-  const_iterator end() const {
-    Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
+  /** 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");
     return d_nv->end<true>();
   }
 
-  Kind getKind() const {
-    Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
+  /** 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();
   }
 
-  unsigned getNumChildren() const {
-    Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
+  /** 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");
     return d_nv->getNumChildren();
   }
 
-  Node operator[](int i) const {
-    Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
-    Assert(i >= 0 && i < d_nv->getNumChildren());
+  /** Access to children of this Node-under-construction. */
+  inline Node operator[](int i) const {
+    Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+    Assert(i >= 0 && i < d_nv->getNumChildren(), "index out of range for NodeBuilder[]");
     return Node(d_nv->d_children[i]);
   }
 
   /**
    * "Reset" this node builder (optionally setting a new kind for it),
-   * using the same memory as before.  This should leave the
-   * NodeBuilder<> in the state it was after initial construction.
+   * using the same "inline" memory as at construction time.  This
+   * deallocates NodeBuilder-allocated heap memory, if it was
+   * allocated, and decrements the reference counts of any currently
+   * children in the NodeBuilder.
+   *
+   * This should leave the BackedNodeBuilder in the state it was after
+   * initial construction, except for Kind, which is set to the
+   * argument (if provided), or UNDEFINED_KIND.  In particular, the
+   * associated NodeManager is not affected by clear().
    */
   void clear(Kind k = kind::UNDEFINED_KIND);
 
   // "Stream" expression constructor syntax
 
-  NodeBuilder& operator<<(const Kind& k) {
-    Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
-    Assert(d_nv->getKind() == kind::UNDEFINED_KIND);
-    d_nv->d_kind = k;
-    return *this;
+  /** Set the Kind of this Node-under-construction. */
+  inline Builder& operator<<(const Kind& k) {
+    Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+    Assert(getKind() == kind::UNDEFINED_KIND,
+           "can't redefine the Kind of a NodeBuilder");
+    Assert(k != kind::UNDEFINED_KIND,
+           "can't define the Kind of a NodeBuilder to be UNDEFINED_KIND");
+    d_nv->d_kind = expr::NodeValue::kindToDKind(k);
+    return static_cast<Builder&>(*this);
   }
 
-  NodeBuilder& operator<<(TNode n) {
-    // FIXME: collapse if ! UNDEFINED_KIND
-    Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
+  /**
+   * If this Node-under-construction has a Kind set, collapse it and
+   * append the given Node as a child.  Otherwise, simply append.
+   * FIXME: do we really want that collapse behavior?  We had agreed
+   * on it but then never wrote code like that.
+   */
+  Builder& operator<<(TNode n) {
+    Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+    /* FIXME: disable this "collapsing" for now..
+    if(EXPECT_FALSE( getKind() != kind::UNDEFINED_KIND )) {
+      Node n2 = operator Node();
+      clear();
+      append(n2);
+    }*/
     return append(n);
   }
 
-  // For pushing sequences of children
-  NodeBuilder& append(const std::vector<Node>& children) {
-    Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
+  /** Append a sequence of children to this Node-under-construction. */
+  inline Builder& append(const std::vector<Node>& children) {
+    Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
     return append(children.begin(), children.end());
   }
 
-  NodeBuilder& append(TNode n) {
-    Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
-    Debug("node") << "append: " << this << " " << n << "[" << n.d_nv << "]" << std::endl;
-    allocateEvIfNecessaryForAppend();
-    expr::NodeValue* ev = n.d_nv;
-    ev->inc();
-    d_nv->d_children[d_nv->d_nchildren++] = ev;
-    return *this;
-  }
-
+  /** Append a sequence of children to this Node-under-construction. */
   template <class Iterator>
-  NodeBuilder& append(const Iterator& begin, const Iterator& end) {
-    Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
+  Builder& 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) {
       append(*i);
     }
-    return *this;
+    return static_cast<Builder&>(*this);
+  }
+
+  /** Append a child to this Node-under-construction. */
+  Builder& append(TNode n) {
+    Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+    allocateNvIfNecessaryForAppend();
+    expr::NodeValue* nv = n.d_nv;
+    nv->inc();
+    d_nv->d_children[d_nv->d_nchildren++] = nv;
+    return static_cast<Builder&>(*this);
   }
 
+  // two versions, so we can support extraction from (const)
+  // NodeBuilders which are temporaries appearing as rvalues
   operator Node();
   operator Node() const;
 
   inline void toStream(std::ostream& out) const {
-    Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
+    Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
     d_nv->toStream(out);
   }
 
-  NodeBuilder& operator&=(TNode);
-  NodeBuilder& operator|=(TNode);
-  NodeBuilder& operator+=(TNode);
-  NodeBuilder& operator-=(TNode);
-  NodeBuilder& operator*=(TNode);
+  Builder& operator&=(TNode);
+  Builder& operator|=(TNode);
+  Builder& operator+=(TNode);
+  Builder& operator-=(TNode);
+  Builder& operator*=(TNode);
 
   friend class AndNodeBuilder;
   friend class OrNodeBuilder;
   friend class PlusNodeBuilder;
   friend class MultNodeBuilder;
 
-  // Yet 1 more example of how terrifying C++ is as a language
+};/* class NodeBuilderBase */
+
+/**
+ * Backing-store interface version for NodeBuilders.  To construct one
+ * of these, you need to create a backing store (preferably on the
+ * stack) for it to hold its "inline" NodeValue.  There's a
+ * convenience macro defined below, makeStackNodeBuilder(b, N),
+ * defined below to define a stack-allocated BackedNodeBuilder "b"
+ * with room for N children on the stack.
+ */
+class BackedNodeBuilder : public NodeBuilderBase<BackedNodeBuilder> {
+public:
+  inline BackedNodeBuilder(char* buf, unsigned maxChildren) :
+    NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) {
+  }
+
+  inline BackedNodeBuilder(char* buf, unsigned maxChildren, Kind k) :
+    NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) {
+  }
+
+  inline BackedNodeBuilder(char* buf, unsigned maxChildren, NodeManager* nm) :
+    NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) {
+  }
+
+  inline BackedNodeBuilder(char* buf, unsigned maxChildren, NodeManager* nm, Kind k) :
+    NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) {
+  }
+
+  // we don't want a vtable, so do not declare a dtor!
+  //inline ~NodeBuilder();
+
+private:
+  // disallow copy or assignment (there would be no backing store!)
+  BackedNodeBuilder(const BackedNodeBuilder& nb);
+  BackedNodeBuilder& operator=(const BackedNodeBuilder& nb);
+
+};/* class BackedNodeBuilder */
+
+/**
+ * Stack-allocate a BackedNodeBuilder with a stack-allocated backing
+ * store of size __n.  The BackedNodeBuilder will be named __v.
+ *
+ * __v must be a simple name.  __n must be convertible to size_t, and
+ * will be evaluated only once.  This macro may only be used where
+ * declarations are permitted.
+ */
+#define makeStackNodeBuilder(__v, __n)                                  \
+  size_t __cvc4_backednodebuilder_nchildren__ ## __v = (__n);           \
+  char __cvc4_backednodebuilder_buf__ ## __v                            \
+  [ sizeof(NodeValue) +                                                 \
+    sizeof(NodeValue*) * __cvc4_backednodebuilder_nchildren__ ## __v ]  \
+    __attribute__((aligned(__WORDSIZE / 8)));                           \
+  BackedNodeBuilder __v(__cvc4_backednodebuilder_buf__ ## __v,          \
+                        __cvc4_backednodebuilder_nchildren__ ## __v)
+
+/**
+ * Simple NodeBuilder interface.  This is a template that requires
+ * that the number of children of the "inline"-allocated NodeValue be
+ * specified as a template parameter (which means it must be a
+ * compile-time constant).
+ */
+template <unsigned nchild_thresh = default_nchild_thresh>
+class NodeBuilder : public NodeBuilderBase<NodeBuilder<nchild_thresh> > {
+  char d_backingStore[ sizeof(expr::NodeValue)
+                       + (sizeof(expr::NodeValue*) * nchild_thresh) ]
+    __attribute__((aligned(__WORDSIZE / 8)));
+
+  typedef NodeBuilderBase<NodeBuilder<nchild_thresh> > super;
+
+  template <unsigned N>
+  void internalCopy(const NodeBuilder<N>& nb);
+
+public:
+  inline NodeBuilder() :
+    NodeBuilderBase<NodeBuilder<nchild_thresh> >(d_backingStore, nchild_thresh) {
+  }
+
+  inline NodeBuilder(Kind k) :
+    NodeBuilderBase<NodeBuilder<nchild_thresh> >(d_backingStore, nchild_thresh, k) {
+  }
+
+  inline NodeBuilder(NodeManager* nm) :
+    NodeBuilderBase<NodeBuilder<nchild_thresh> >(d_backingStore, nchild_thresh, nm) {
+  }
+
+  inline NodeBuilder(NodeManager* nm, Kind k) :
+    NodeBuilderBase<NodeBuilder<nchild_thresh> >(d_backingStore, nchild_thresh, nm, k) {
+  }
+
+  // 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) :
+    NodeBuilderBase<NodeBuilder<nchild_thresh> >(d_backingStore,
+                                                 nchild_thresh,
+                                                 nb.d_nm,
+                                                 nb.getKind()) {
+    internalCopy(nb);
+  }
+
+  // technically this is a conversion, not a copy
+  template <unsigned N>
+  inline NodeBuilder(const NodeBuilder<N>& nb) :
+    NodeBuilderBase<NodeBuilder<nchild_thresh> >(d_backingStore,
+                                                 nchild_thresh,
+                                                 nb.d_nm,
+                                                 nb.getKind()) {
+    internalCopy(nb);
+  }
+
+  // we don't want a vtable, so do not declare a dtor!
+  //inline ~NodeBuilder();
+
   // This is needed for copy constructors of different sizes to access private fields
   template <unsigned N>
   friend class NodeBuilder;
 
-};/* class NodeBuilder */
+};/* class NodeBuilder<> */
 
 // TODO: add templatized NodeTemplate<ref_count> to all above and
 // below inlines for 'const [T]Node&' arguments?  Technically a lot of
@@ -336,28 +787,28 @@ public:
 
 };/* class MultNodeBuilder */
 
-template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator&=(TNode e) {
+template <class Builder>
+inline Builder& NodeBuilderBase<Builder>::operator&=(TNode e) {
   return collapseTo(kind::AND).append(e);
 }
 
-template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator|=(TNode e) {
+template <class Builder>
+inline Builder& NodeBuilderBase<Builder>::operator|=(TNode e) {
   return collapseTo(kind::OR).append(e);
 }
 
-template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator+=(TNode e) {
+template <class Builder>
+inline Builder& NodeBuilderBase<Builder>::operator+=(TNode e) {
   return collapseTo(kind::PLUS).append(e);
 }
 
-template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator-=(TNode e) {
+template <class Builder>
+inline Builder& NodeBuilderBase<Builder>::operator-=(TNode e) {
   return collapseTo(kind::PLUS).append(NodeManager::currentNM()->mkNode(kind::UMINUS, e));
 }
 
-template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator*=(TNode e) {
+template <class Builder>
+inline Builder& NodeBuilderBase<Builder>::operator*=(TNode e) {
   return collapseTo(kind::MULT).append(e);
 }
 
@@ -565,391 +1016,481 @@ inline NodeTemplate<true> operator-(const NodeTemplate<rc>& a) {
 #include "expr/node.h"
 #include "expr/node_manager.h"
 
-// template implementations
-
 namespace CVC4 {
 
-template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>::NodeBuilder() :
-  d_size(nchild_thresh),
-  d_hash(0),
-  d_nm(NodeManager::currentNM()),
-  d_used(false),
+template <class Builder>
+inline NodeBuilderBase<Builder>::NodeBuilderBase(char* buf, unsigned maxChildren, Kind k) :
+  d_inlineNv(*reinterpret_cast<expr::NodeValue*>(buf)),
   d_nv(&d_inlineNv),
-  d_inlineNv(0),
-  d_childrenStorage() {}
-
-template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>::NodeBuilder(Kind k) :
-  d_size(nchild_thresh),
-  d_hash(0),
   d_nm(NodeManager::currentNM()),
-  d_used(false),
-  d_nv(&d_inlineNv),
-  d_inlineNv(0),
-  d_childrenStorage() {
+  d_inlineNvMaxChildren(maxChildren),
+  d_nvMaxChildren(maxChildren) {
 
-  d_inlineNv.d_kind = k;
+  d_inlineNv.d_id = 0;
+  d_inlineNv.d_rc = 0;
+  d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k);
+  d_inlineNv.d_nchildren = 0;
 }
 
-template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<nchild_thresh>& nb) :
-  d_size(nchild_thresh),
-  d_hash(0),
-  d_nm(nb.d_nm),
-  d_used(nb.d_used),
-  d_nv(&d_inlineNv),
-  d_inlineNv(0),
-  d_childrenStorage() {
-
-  if(nvIsAllocated(nb)) {
-    realloc(nb.d_size, false);
-    std::copy(nb.d_nv->nv_begin(), nb.d_nv->nv_end(), d_nv->nv_begin());
-  } else {
-    std::copy(nb.d_nv->nv_begin(), nb.d_nv->nv_end(), d_inlineNv.nv_begin());
-  }
-  d_nv->d_kind = nb.d_nv->d_kind;
-  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();
-  }
-}
-
-template <unsigned nchild_thresh>
-template <unsigned N>
-inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<N>& nb) :
-  d_size(nchild_thresh),
-  d_hash(0),
-  d_nm(NodeManager::currentNM()),
-  d_used(nb.d_used),
+template <class Builder>
+inline NodeBuilderBase<Builder>::NodeBuilderBase(char* buf, unsigned maxChildren, NodeManager* nm, Kind k) :
+  d_inlineNv(*reinterpret_cast<expr::NodeValue*>(buf)),
   d_nv(&d_inlineNv),
-  d_inlineNv(0),
-  d_childrenStorage() {
-
-  if(nb.d_nv->d_nchildren > nchild_thresh) {
-    realloc(nb.d_size, false);
-    std::copy(nb.d_nv->nv_begin(), nb.d_nv->nv_end(), d_nv->nv_begin());
-  } else {
-    std::copy(nb.d_nv->nv_begin(), nb.d_nv->nv_end(), d_inlineNv.nv_begin());
-  }
-  d_nv->d_kind = nb.d_nv->d_kind;
-  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();
-  }
-}
-
-template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm) :
-  d_size(nchild_thresh),
-  d_hash(0),
   d_nm(nm),
-  d_used(false),
-  d_nv(&d_inlineNv),
-  d_inlineNv(0),
-  d_childrenStorage() {
-  d_inlineNv.d_kind = expr::NodeValue::kindToDKind(kind::UNDEFINED_KIND);
-}
+  d_inlineNvMaxChildren(maxChildren),
+  d_nvMaxChildren(maxChildren) {
 
-template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm, Kind k) :
-  d_size(nchild_thresh),
-  d_hash(0),
-  d_nm(nm),
-  d_used(false),
-  d_nv(&d_inlineNv),
-  d_inlineNv(0),
-  d_childrenStorage() {
-
-  d_inlineNv.d_kind = k;
+  d_inlineNv.d_id = 0;
+  d_inlineNv.d_rc = 0;
+  d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k);
+  d_inlineNv.d_nchildren = 0;
 }
 
-template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>::~NodeBuilder() {
-  if(!d_used) {
-    // Warning("NodeBuilder unused at destruction\n");
-    // Commented above, as it happens a lot, for example with exceptions
+template <class Builder>
+inline NodeBuilderBase<Builder>::~NodeBuilderBase() {
+  if(EXPECT_FALSE( nvIsAllocated() )) {
     dealloc();
+  } else if(EXPECT_FALSE( !isUsed() )) {
+    decrRefCounts();
   }
 }
 
-template <unsigned nchild_thresh>
-void NodeBuilder<nchild_thresh>::clear(Kind k) {
-  if(!d_used) {
-    Warning("NodeBuilder unused at clear\n");
-
+template <class Builder>
+void NodeBuilderBase<Builder>::clear(Kind k) {
+  if(EXPECT_FALSE( nvIsAllocated() )) {
     dealloc();
+  } else if(EXPECT_FALSE( !isUsed() )) {
+    decrRefCounts();
+  } else {
+    setUnused();
   }
 
-  d_size = nchild_thresh;
-  d_hash = 0;
-  d_nm = NodeManager::currentNM();
-  d_used = false;
-  d_nv = &d_inlineNv;
-  d_inlineNv.d_kind = k;
-  d_inlineNv.d_nchildren = 0;//FIXME leak
-}
-
-template <unsigned nchild_thresh>
-void NodeBuilder<nchild_thresh>::realloc() {
-  if(EXPECT_FALSE( nvIsAllocated() )) {
-    d_nv = (expr::NodeValue*)
-      std::realloc(d_nv,
-                   sizeof(expr::NodeValue) + ( sizeof(expr::NodeValue*) * (d_size *= 2) ));
-    if(d_nv == NULL) {
-      throw std::bad_alloc();
-    }
-  } else {
-    d_nv = (expr::NodeValue*)
-      std::malloc(sizeof(expr::NodeValue) + ( sizeof(expr::NodeValue*) * (d_size *= 2) ));
-    if(d_nv == NULL) {
-      throw std::bad_alloc();
-    }
-    d_nv->d_id = 0;
-    d_nv->d_rc = 0;
-    d_nv->d_kind = d_inlineNv.d_kind;
-    d_nv->d_nchildren = nchild_thresh;
-    std::copy(d_inlineNv.d_children,
-              d_inlineNv.d_children + nchild_thresh,
-              d_nv->d_children);
+  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;
 }
 
-template <unsigned nchild_thresh>
-void NodeBuilder<nchild_thresh>::realloc(size_t toSize, bool copy) {
-  Assert( d_size < toSize );
+template <class Builder>
+void NodeBuilderBase<Builder>::realloc(size_t toSize) {
+  Assert( toSize > d_nvMaxChildren,
+          "attempt to realloc() a NodeBuilder to a smaller/equal size!" );
 
   if(EXPECT_FALSE( nvIsAllocated() )) {
-    d_nv = (expr::NodeValue*)
+    // 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_size = toSize) ));
-    if(d_nv == NULL) {
+                   ( sizeof(expr::NodeValue*) * (d_nvMaxChildren = 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();
     }
+    // Here, the copy (between two heap-allocated buffers) has already
+    // been done for us by the std::realloc().
+    d_nv = newBlock;
   } else {
-    d_nv = (expr::NodeValue*)
+    // Ensure d_nv is not modified on allocation failure
+    expr::NodeValue* newBlock = (expr::NodeValue*)
       std::malloc(sizeof(expr::NodeValue) +
-                  ( sizeof(expr::NodeValue*) * (d_size = toSize) ));
-    if(d_nv == NULL) {
+                  ( sizeof(expr::NodeValue*) * (d_nvMaxChildren = toSize) ));
+    if(newBlock == NULL) {
       throw std::bad_alloc();
     }
+
+    d_nv = newBlock;
     d_nv->d_id = 0;
     d_nv->d_rc = 0;
     d_nv->d_kind = d_inlineNv.d_kind;
-    d_nv->d_nchildren = nchild_thresh;
-    if(copy) {
-      std::copy(d_inlineNv.d_children,
-                d_inlineNv.d_children + nchild_thresh,
-                d_nv->d_children);
-      // inhibit decr'ing refcounts of children in dtor
-      d_inlineNv.d_nchildren = 0;
-    }
+    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>
-inline void NodeBuilder<nchild_thresh>::dealloc() {
-  /* Prefer asserts to if() because usually these conditions have been
-   * checked already, so we don't want to do a double-check in
-   * production; these are just sanity checks for debug builds */
-  Assert(!d_used, "Internal error: NodeBuilder: dealloc() called with d_used");
+template <class Builder>
+void NodeBuilderBase<Builder>::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();
   }
-  if(nvIsAllocated()) {
-    free(d_nv);
+
+  free(d_nv);
+  d_nv = &d_inlineNv;
+  d_nvMaxChildren = d_inlineNvMaxChildren;
+}
+
+template <class Builder>
+void NodeBuilderBase<Builder>::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>
-NodeBuilder<nchild_thresh>::operator Node() const {// const version
-  Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
-  Assert(d_nv->getKind() != kind::UNDEFINED_KIND,
+// NON-CONST VERSION OF NODE EXTRACTOR
+template <class Builder>
+NodeBuilderBase<Builder>::operator Node() {
+  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!");
 
-  if(d_nv->d_kind == kind::VARIABLE) {
-    Assert(d_nv->d_nchildren == 0);
+  // 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(getKind() == kind::VARIABLE) {
+    /* 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) +
-                  (sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));// FIXME :: WTF??
+      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 = kind::VARIABLE;
+    nv->d_kind = expr::NodeValue::kindToDKind(kind::VARIABLE);
     nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
     nv->d_rc = 0;
-    //d_used = true; // const version
-    //d_nv = NULL; // const version
+    setUsed();
+    Debug("gc") << "creating node value " << nv
+                << " [" << nv->d_id << "]: " << nv->toString() << "\n";
     return Node(nv);
   }
 
-  // implementation differs depending on whether the expression value
-  // was malloc'ed or not
+  // 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(EXPECT_TRUE( ! nvIsAllocated() )) {
+    /** Case 1.  d_nv points to d_inlineNv: it is the backing store
+     ** supplied by the user (or derived class) **/
+
+    // Lookup the expression value in the pool we already have
+    expr::NodeValue* nv = d_nm->poolLookup(&d_inlineNv);
+    if(nv != 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();
+      Debug("gc") << "creating node value " << nv
+                  << " [" << nv->d_id << "]: " << nv->toString() << "\n";
+      return Node(nv);
+    } 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
+      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 = expr::NodeValue::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();
+
+      d_nm->poolInsert(nv);
+      Debug("gc") << "creating node value " << nv
+                  << " [" << nv->d_id << "]: " << nv->toString() << "\n";
+      return Node(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. **/
 
-  if(EXPECT_FALSE( nvIsAllocated() )) {
     // Lookup the expression value in the pool we already have (with insert)
     expr::NodeValue* nv = d_nm->poolLookup(d_nv);
     // If something else is there, we reuse it
     if(nv != NULL) {
-      // expression already exists in node manager
-      //dealloc(); // const version
-      //d_used = true; // const version
+      /* 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();
+      Debug("gc") << "creating node value " << nv
+                  << " [" << nv->d_id << "]: " << nv->toString() << "\n";
+      return Node(nv);
+    } 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();
+      nv = d_nv;
+      nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
+      d_nv = &d_inlineNv;
+      d_nvMaxChildren = d_inlineNvMaxChildren;
+      setUsed();
+      d_nm->poolInsert(nv);
+      Debug("gc") << "creating node value " << nv
+                  << " [" << nv->d_id << "]: " << nv->toString() << "\n";
       return Node(nv);
     }
-    // Otherwise copy children out
-    nv = (expr::NodeValue*)
-      std::malloc(sizeof(expr::NodeValue) +
-                  ( sizeof(expr::NodeValue*) * d_nv->d_nchildren ));
-    if(nv == NULL) {
-      throw std::bad_alloc();
-    }
-    nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
-    nv->d_rc = 0;
-    nv->d_kind = d_nv->d_kind;
-    nv->d_nchildren = d_nv->d_nchildren;
-    std::copy(d_nv->d_children,
-              d_nv->d_children + d_nv->d_nchildren,
-              nv->d_children);
-    // inc child refcounts
-    for(expr::NodeValue::nv_iterator i = nv->nv_begin();
-        i != nv->nv_end();
-        ++i) {
-      (*i)->inc();
-    }
-    d_nm->poolInsert(nv);
-    return Node(nv);
   }
-
-  // Lookup the expression value in the pool we already have
-  expr::NodeValue* ev = d_nm->poolLookup(d_nv);
-  //DANGER d_nv should be ptr-to-const in the above line b/c it points to d_inlineNv
-  if(ev != NULL) {
-    // expression already exists in node manager
-    //d_used = true; // const version
-    Debug("node") << "result: " << Node(ev) << std::endl;
-    return Node(ev);
-  }
-
-  // otherwise create the canonical expression value for this node
-  ev = (expr::NodeValue*)
-    std::malloc(sizeof(expr::NodeValue) +
-                ( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));
-  if(ev == NULL) {
-    throw std::bad_alloc();
-  }
-  ev->d_nchildren = d_inlineNv.d_nchildren;
-  ev->d_kind = d_inlineNv.d_kind;
-  ev->d_id = expr::NodeValue::next_id++;// FIXME multithreading
-  ev->d_rc = 0;
-  std::copy(d_inlineNv.d_children,
-            d_inlineNv.d_children + d_inlineNv.d_nchildren,
-            ev->d_children);
-  //d_used = true;
-  //d_nv = NULL;
-  //d_inlineNv.d_nchildren = 0;// inhibit decr'ing refcounts of children in dtor
-  // inc child refcounts
-  for(expr::NodeValue::nv_iterator i = ev->nv_begin();
-      i != ev->nv_end();
-      ++i) {
-    (*i)->inc();
-  }
-
-  // Make the new expression
-  d_nm->poolInsert(ev);
-  return Node(ev);
 }
 
-template <unsigned nchild_thresh>
-NodeBuilder<nchild_thresh>::operator Node() {// not const
-  Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
-  Assert(d_nv->getKind() != kind::UNDEFINED_KIND,
+// CONST VERSION OF NODE EXTRACTOR
+template <class Builder>
+NodeBuilderBase<Builder>::operator Node() 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!");
 
-  if(d_nv->d_kind == kind::VARIABLE) {
-    Assert(d_nv->d_nchildren == 0);
+  // 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(getKind() == kind::VARIABLE) {
+    /* 0. If a VARIABLE, treat similarly to 1(b), except that we know
+     * there are no children, 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) +
-                  (sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));// FIXME :: WTF??
+      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 = kind::VARIABLE;
+    nv->d_kind = expr::NodeValue::kindToDKind(kind::VARIABLE);
     nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
     nv->d_rc = 0;
-    d_used = true;
-    d_nv = NULL;
-    Debug("node") << "result: " << Node(nv) << std::endl;
+    Debug("gc") << "creating node value " << nv
+                << " [" << nv->d_id << "]: " << nv->toString() << "\n";
     return Node(nv);
   }
 
-  // implementation differs depending on whether the expression value
-  // was malloc'ed or not
+  // 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(EXPECT_TRUE( ! nvIsAllocated() )) {
+    /** Case 1.  d_nv points to d_inlineNv: it is the backing store
+     ** supplied by the user (or derived class) **/
+
+    // Lookup the expression value in the pool we already have
+    expr::NodeValue* nv = d_nm->poolLookup(&d_inlineNv);
+    if(nv != 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. */
+
+      Debug("gc") << "creating node value " << nv
+                  << " [" << nv->d_id << "]: " << nv->toString() << "\n";
+      return Node(nv);
+    } 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
+      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 = expr::NodeValue::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);
+
+      for(expr::NodeValue::nv_iterator i = nv->nv_begin();
+          i != nv->nv_end();
+          ++i) {
+        (*i)->inc();
+      }
+
+      d_nm->poolInsert(nv);
+      Debug("gc") << "creating node value " << nv
+                  << " [" << nv->d_id << "]: " << nv->toString() << "\n";
+      return Node(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. **/
 
-  if(EXPECT_FALSE( nvIsAllocated() )) {
     // Lookup the expression value in the pool we already have (with insert)
     expr::NodeValue* nv = d_nm->poolLookup(d_nv);
     // If something else is there, we reuse it
     if(nv != NULL) {
-      // expression already exists in node manager
-      dealloc();
-      d_used = true;
-      Debug("node") << "result: " << Node(nv) << std::endl;
+      /* Subcase (a) The Node under construction already exists in the
+       * NodeManager's pool. */
+
+      /* 2(a). The existing NodeManager pool entry is returned; we
+       * leave child reference counts alone and get them at
+       * NodeBuilder destruction time. */
+
+      Debug("gc") << "creating node value " << nv
+                  << " [" << nv->d_id << "]: " << nv->toString() << "\n";
+      return Node(nv);
+    } else {
+      /* Subcase (b) The Node under construction is NOT already in the
+       * NodeManager's pool. */
+
+      /* 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. */
+
+      // create the canonical expression value for this node
+      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 = expr::NodeValue::next_id++;// FIXME multithreading
+      nv->d_rc = 0;
+
+      std::copy(d_nv->d_children,
+                d_nv->d_children + d_nv->d_nchildren,
+                nv->d_children);
+
+      for(expr::NodeValue::nv_iterator i = nv->nv_begin();
+          i != nv->nv_end();
+          ++i) {
+        (*i)->inc();
+      }
+
+      d_nm->poolInsert(nv);
+      Debug("gc") << "creating node value " << nv
+                  << " [" << nv->d_id << "]: " << nv->toString() << "\n";
       return Node(nv);
     }
-    // Otherwise crop and set the expression value to the allocated one
-    crop();
-    nv = d_nv;
-    nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
-    d_nv = NULL;
-    d_used = true;
-    d_nm->poolInsert(nv);
-    return Node(nv);
   }
+}
 
-  // Lookup the expression value in the pool we already have
-  expr::NodeValue* ev = d_nm->poolLookup(&d_inlineNv);
-  if(ev != NULL) {
-    // expression already exists in node manager
-    d_used = true;
-    Debug("node") << "result: " << Node(ev) << std::endl;
-    return Node(ev);
+template <unsigned nchild_thresh>
+template <unsigned N>
+void NodeBuilder<nchild_thresh>::internalCopy(const NodeBuilder<N>& nb) {
+  if(nb.isUsed()) {
+    super::setUsed();
+    return;
   }
 
-  // otherwise create the canonical expression value for this node
-  ev = (expr::NodeValue*)
-    std::malloc(sizeof(expr::NodeValue) +
-                ( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));
-  if(ev == NULL) {
-    throw std::bad_alloc();
+  if(nb.d_nvMaxChildren > super::d_nvMaxChildren) {
+    super::realloc(nb.d_nvMaxChildren);
   }
-  ev->d_nchildren = d_inlineNv.d_nchildren;
-  ev->d_kind = d_inlineNv.d_kind;
-  ev->d_id = expr::NodeValue::next_id++;// FIXME multithreading
-  ev->d_rc = 0;
-  std::copy(d_inlineNv.d_children,
-            d_inlineNv.d_children + d_inlineNv.d_nchildren,
-            ev->d_children);
-  d_used = true;
-  d_nv = NULL;
-  d_inlineNv.d_nchildren = 0;// inhibit decr'ing refcounts of children in dtor
 
-  // Make the new expression
-  d_nm->poolInsert(ev);
-  return Node(ev);
+  std::copy(nb.d_nv->nv_begin(),
+            nb.d_nv->nv_end(),
+            super::d_nv->nv_begin());
+
+  super::d_nv->d_nchildren = nb.d_nv->d_nchildren;
+
+  for(expr::NodeValue::nv_iterator i = super::d_nv->nv_begin();
+      i != super::d_nv->nv_end();
+      ++i) {
+    (*i)->inc();
+  }
 }
 
-template <unsigned nchild_thresh>
+template <class Builder>
 inline std::ostream& operator<<(std::ostream& out,
-                                const NodeBuilder<nchild_thresh>& b) {
+                                const NodeBuilderBase<Builder>& b) {
   b.toStream(out);
   return out;
 }
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 5b5dfafa9..98171cb2e 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -15,8 +15,11 @@
 
 #include "node_manager.h"
 
+#include <ext/hash_set>
+
 using namespace std;
 using namespace CVC4::expr;
+using __gnu_cxx::hash_set;
 
 namespace CVC4 {
 
@@ -30,4 +33,80 @@ NodeValue* NodeManager::poolLookup(NodeValue* nv) const {
     return *find;
   }
 }
+
+/**
+ * This class ensure that NodeManager::d_reclaiming gets set to false
+ * even on exceptional exit from NodeManager::reclaimZombies().
+ */
+struct Reclaim {
+  bool& d_reclaimField;
+  Reclaim(bool& reclaim) :
+    d_reclaimField(reclaim) {
+
+    Debug("gc") << ">> setting RECLAIM field\n";
+    d_reclaimField = true;
+  }
+  ~Reclaim() {
+    Debug("gc") << "<< clearing RECLAIM field\n";
+    d_reclaimField = false;
+  }
+};
+
+/**
+ * Reclaim a particular zombie.
+ */
+void NodeManager::reclaimZombie(expr::NodeValue* nv) {
+  Debug("gc") << "deleting node value " << nv
+              << " [" << nv->d_id << "]: " << nv->toString() << "\n";
+
+  if(nv->getKind() != kind::VARIABLE) {
+    poolRemove(nv);
+  }
+
+  d_attrManager.deleteAllAttributes(nv);
+
+  // dtor decr's ref counts of children
+  // FIXME: NOT  ACTUALLY GARBAGE COLLECTING  YET (DUE TO  ISSUES WITH
+  // CDMAPs (?) ) delete nv;
+}
+
+void NodeManager::reclaimZombies() {
+  // FIXME multithreading
+
+  Debug("gc") << "reclaiming " << d_zombies.size() << " zombie(s)!\n";
+
+  // during reclamation, reclaimZombies() is never supposed to be called
+  Assert(! d_reclaiming, "NodeManager::reclaimZombies() not re-entrant!");
+  Reclaim r(d_reclaiming);
+
+  // We copy the set away and clear the NodeManager's set of zombies.
+  // This is because reclaimZombie() decrements the RC of the
+  // NodeValue's children, which may (recursively) reclaim them.
+  //
+  // Let's say we're reclaiming zombie NodeValue "A" and its child "B"
+  // then becomes a zombie (NodeManager::gc(B) is called).
+  //
+  // One way to handle B's zombification is simply to put it into
+  // d_zombies.  This is what we do.  However, if we're currently
+  // processing d_zombies in the loop below, such addition may be
+  // invisible to us (B is leaked) or even invalidate our iterator,
+  // causing a crash.
+
+  vector<NodeValue*> zombies;
+  zombies.reserve(d_zombies.size());
+  std::copy(d_zombies.begin(),
+            d_zombies.end(),
+            std::back_inserter(zombies));
+  d_zombies.clear();
+
+  for(vector<NodeValue*>::iterator i = zombies.begin();
+      i != zombies.end();
+      ++i) {
+    // collect ONLY IF still zero
+    if((*i)->d_rc == 0) {
+      reclaimZombie(*i);
+    }
+  }
+}
+
 }/* CVC4 namespace */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index c4f54727a..32c1cd210 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -28,6 +28,7 @@
 
 #include "expr/kind.h"
 #include "expr/expr.h"
+#include "expr/node_value.h"
 #include "context/context.h"
 
 namespace CVC4 {
@@ -50,31 +51,65 @@ typedef Attribute<attr::Type, const CVC4::Type*> TypeAttr;
 class NodeManager {
   static __thread NodeManager* s_current;
 
-  template <unsigned> friend class CVC4::NodeBuilder;
+  template <class Builder> friend class CVC4::NodeBuilderBase;
 
   typedef __gnu_cxx::hash_set<expr::NodeValue*,
                               expr::NodeValueInternalHashFcn,
                               expr::NodeValue::NodeValueEq> NodeValueSet;
+  typedef __gnu_cxx::hash_set<expr::NodeValue*,
+                              expr::NodeValueIDHashFcn,
+                              expr::NodeValue::NodeValueEq> ZombieSet;
+
   NodeValueSet d_nodeValueSet;
 
   expr::attr::AttributeManager d_attrManager;
 
   expr::NodeValue* poolLookup(expr::NodeValue* nv) const;
   void poolInsert(expr::NodeValue* nv);
+  void poolRemove(expr::NodeValue* nv);
 
   friend class NodeManagerScope;
   friend class expr::NodeValue;
 
-  std::vector<expr::NodeValue*> d_zombieList;
+  bool d_reclaiming;
+  ZombieSet d_zombies;
 
+  /**
+   * Register a NodeValue as a zombie.
+   */
   inline void gc(expr::NodeValue* nv) {
     Assert(nv->d_rc == 0);
-    d_zombieList.push_back(nv);
+    if(d_reclaiming) {// FIXME multithreading
+      // currently reclaiming zombies; just push onto the list
+      Debug("gc") << "zombifying node value " << nv
+                  << " [" << nv->d_id << "]: " << nv->toString()
+                  << " [CURRENTLY-RECLAIMING]\n";
+      d_zombies.insert(nv);// FIXME multithreading
+    } else {
+      Debug("gc") << "zombifying node value " << nv
+                  << " [" << nv->d_id << "]: " << nv->toString() << "\n";
+      d_zombies.insert(nv);// FIXME multithreading
+
+      // for now, collect eagerly.  can add heuristic here later..
+      reclaimZombies();
+    }
   }
 
+  /**
+   * Reclaim all zombies.
+   */
+  void reclaimZombies();
+
+  /**
+   * Reclaim a particular zombie.
+   */
+  void reclaimZombie(expr::NodeValue* nv);
+
 public:
 
-  NodeManager(context::Context* ctxt) : d_attrManager(ctxt) {
+  NodeManager(context::Context* ctxt) :
+    d_attrManager(ctxt),
+    d_reclaiming(false) {
     poolInsert( &expr::NodeValue::s_null );
   }
 
@@ -96,6 +131,29 @@ public:
   Node mkVar();
 
   template <class AttrKind>
+  inline typename AttrKind::value_type getAttribute(expr::NodeValue* nv,
+                                                    const AttrKind&) const;
+
+  // Note that there are two, distinct hasAttribute() declarations for
+  // a reason (rather than using a pointer-valued argument with a
+  // default value): they permit more optimized code in the underlying
+  // hasAttribute() implementations.
+
+  template <class AttrKind>
+  inline bool hasAttribute(expr::NodeValue* nv,
+                           const AttrKind&) const;
+
+  template <class AttrKind>
+  inline bool hasAttribute(expr::NodeValue* nv,
+                           const AttrKind&,
+                           typename AttrKind::value_type&) const;
+
+  template <class AttrKind>
+  inline void setAttribute(expr::NodeValue* nv,
+                           const AttrKind&,
+                           const typename AttrKind::value_type& value);
+
+  template <class AttrKind>
   inline typename AttrKind::value_type getAttribute(TNode n,
                                                     const AttrKind&) const;
 
@@ -118,7 +176,6 @@ public:
                            const AttrKind&,
                            const typename AttrKind::value_type& value);
 
-
   /** Get the type for booleans. */
   inline const BooleanType* booleanType() const {
     return BooleanType::getInstance();
@@ -131,16 +188,16 @@ public:
 
   /** Make a function type from domain to range. */
   inline const FunctionType*
-  mkFunctionType(const Type* domain, const Type* range);
+  mkFunctionType(const Type* domain, const Type* range) const;
 
   /** Make a function type with input types from argTypes. */
   inline const FunctionType*
-  mkFunctionType(const std::vector<const Type*>& argTypes, const Type* range);
+  mkFunctionType(const std::vector<const Type*>& argTypes, const Type* range) const;
 
   /** Make a new sort with the given name. */
-  inline const Type* mkSort(const std::string& name);
+  inline const Type* mkSort(const std::string& name) const;
 
-  inline const Type* getType(TNode n);
+  inline const Type* getType(TNode n) const;
 };
 
 /**
@@ -203,36 +260,62 @@ public:
 };
 
 template <class AttrKind>
+inline typename AttrKind::value_type NodeManager::getAttribute(expr::NodeValue* nv,
+                                                               const AttrKind&) const {
+  return d_attrManager.getAttribute(nv, AttrKind());
+}
+
+template <class AttrKind>
+inline bool NodeManager::hasAttribute(expr::NodeValue* nv,
+                                      const AttrKind&) const {
+  return d_attrManager.hasAttribute(nv, AttrKind());
+}
+
+template <class AttrKind>
+inline bool NodeManager::hasAttribute(expr::NodeValue* nv,
+                                      const AttrKind&,
+                                      typename AttrKind::value_type& ret) const {
+  return d_attrManager.hasAttribute(nv, AttrKind(), ret);
+}
+
+template <class AttrKind>
+inline void NodeManager::setAttribute(expr::NodeValue* nv,
+                                      const AttrKind&,
+                                      const typename AttrKind::value_type& value) {
+  d_attrManager.setAttribute(nv, AttrKind(), value);
+}
+
+template <class AttrKind>
 inline typename AttrKind::value_type NodeManager::getAttribute(TNode n,
                                                                const AttrKind&) const {
-  return d_attrManager.getAttribute(n, AttrKind());
+  return d_attrManager.getAttribute(n.d_nv, AttrKind());
 }
 
 template <class AttrKind>
 inline bool NodeManager::hasAttribute(TNode n,
                                       const AttrKind&) const {
-  return d_attrManager.hasAttribute(n, AttrKind());
+  return d_attrManager.hasAttribute(n.d_nv, AttrKind());
 }
 
 template <class AttrKind>
 inline bool NodeManager::hasAttribute(TNode n,
                                       const AttrKind&,
                                       typename AttrKind::value_type& ret) const {
-  return d_attrManager.hasAttribute(n, AttrKind(), ret);
+  return d_attrManager.hasAttribute(n.d_nv, AttrKind(), ret);
 }
 
 template <class AttrKind>
 inline void NodeManager::setAttribute(TNode n,
                                       const AttrKind&,
                                       const typename AttrKind::value_type& value) {
-  d_attrManager.setAttribute(n, AttrKind(), value);
+  d_attrManager.setAttribute(n.d_nv, AttrKind(), value);
 }
 
 /** Make a function type from domain to range.
-  * TODO: Function types should be unique for this manager. */
+ * TODO: Function types should be unique for this manager. */
 const FunctionType*
 NodeManager::mkFunctionType(const Type* domain,
-                            const Type* range) {
+                            const Type* range) const {
   std::vector<const Type*> argTypes;
   argTypes.push_back(domain);
   return new FunctionType(argTypes, range);
@@ -242,23 +325,29 @@ NodeManager::mkFunctionType(const Type* domain,
  * TODO: Function types should be unique for this manager. */
 const FunctionType*
 NodeManager::mkFunctionType(const std::vector<const Type*>& argTypes,
-                            const Type* range) {
+                            const Type* range) const {
   Assert( argTypes.size() > 0 );
   return new FunctionType(argTypes, range);
 }
 
 const Type*
-NodeManager::mkSort(const std::string& name) {
+NodeManager::mkSort(const std::string& name) const {
   return new SortType(name);
 }
-inline const Type* NodeManager::getType(TNode n) {
+inline const Type* NodeManager::getType(TNode n) const {
   return getAttribute(n, CVC4::expr::TypeAttr());
 }
 
 inline void NodeManager::poolInsert(expr::NodeValue* nv) {
   Assert(d_nodeValueSet.find(nv) == d_nodeValueSet.end(),
          "NodeValue already in the pool!");
-  d_nodeValueSet.insert(nv);
+  d_nodeValueSet.insert(nv);// FIXME multithreading
+}
+
+inline void NodeManager::poolRemove(expr::NodeValue* nv) {
+  Assert(d_nodeValueSet.find(nv) != d_nodeValueSet.end(),
+         "NodeValue is not in the pool!");
+  d_nodeValueSet.erase(nv);// FIXME multithreading
 }
 
 }/* CVC4 namespace */
@@ -305,12 +394,13 @@ inline Node NodeManager::mkVar(const Type* type, const std::string& name) {
 }
 
 inline Node NodeManager::mkVar(const Type* type) {
-  Node n = NodeBuilder<>(this, kind::VARIABLE);
+  Node n = mkVar();
   n.setAttribute(expr::TypeAttr(), type);
   return n;
 }
 
 inline Node NodeManager::mkVar() {
+  // TODO: rewrite to not use NodeBuilder
   return NodeBuilder<>(this, kind::VARIABLE);
 }
 
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index 5c5765011..5dbfac169 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -38,9 +38,11 @@ string NodeValue::toString() const {
 
 void NodeValue::toStream(std::ostream& out) const {
   if(d_kind == kind::VARIABLE) {
-    Node n(this);
     string s;
-    if(n.hasAttribute(VarNameAttr(), s)) {
+    // conceptually "this" is const, and hasAttribute() doesn't change
+    // its argument, but it requires a non-const key arg (for now)
+    if(NodeManager::currentNM()->hasAttribute(const_cast<NodeValue*>(this),
+                                              VarNameAttr(), s)) {
       out << s;
     } else {
       out << "var_" << d_id;
@@ -51,7 +53,7 @@ void NodeValue::toStream(std::ostream& out) const {
       if(i != nv_end()) {
         out << " ";
       }
-      Node(*i).toStream(out);
+      (*i)->toStream(out);
     }
     out << ")";
   }
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index bd74fd4d4..a5f68babf 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -32,7 +32,8 @@
 namespace CVC4 {
 
 template <bool ref_count> class NodeTemplate;
-template <unsigned> class NodeBuilder;
+template <class Builder> class NodeBuilderBase;
+template <unsigned N> class NodeBuilder;
 class AndNodeBuilder;
 class OrNodeBuilder;
 class PlusNodeBuilder;
@@ -79,7 +80,8 @@ class NodeValue {
   // todo add exprMgr ref in debug case
 
   template <bool> friend class CVC4::NodeTemplate;
-  template <unsigned> friend class CVC4::NodeBuilder;
+  template <class Builder> friend class CVC4::NodeBuilderBase;
+  template <unsigned N> friend class CVC4::NodeBuilder;
   friend class CVC4::AndNodeBuilder;
   friend class CVC4::OrNodeBuilder;
   friend class CVC4::PlusNodeBuilder;
@@ -94,9 +96,6 @@ class NodeValue {
   /** Private default constructor for the null value. */
   NodeValue();
 
-  /** Private default constructor for the NodeBuilder. */
-  NodeValue(int);
-
   /** Destructor decrements the ref counts of its children */
   ~NodeValue();
 
@@ -226,6 +225,15 @@ struct NodeValueInternalHashFcn {
   }
 };/* struct NodeValueHashFcn */
 
+/**
+ * For hash_maps, hash_sets, etc.
+ */
+struct NodeValueIDHashFcn {
+  inline size_t operator()(const NodeValue* nv) const {
+    return (size_t) nv->getId();
+  }
+};/* struct NodeValueHashFcn */
+
 }/* CVC4::expr namespace */
 }/* CVC4 namespace */
 
@@ -241,13 +249,6 @@ inline NodeValue::NodeValue() :
   d_nchildren(0) {
 }
 
-inline NodeValue::NodeValue(int) :
-  d_id(0),
-  d_rc(0),
-  d_kind(kindToDKind(kind::UNDEFINED_KIND)),
-  d_nchildren(0) {
-}
-
 inline NodeValue::~NodeValue() {
   for(nv_iterator i = nv_begin(); i != nv_end(); ++i) {
     (*i)->dec();
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8def3e279..6e3a1b801 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -10,6 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** The main entry point into the CVC4 library's SMT interface.
  **/
 
 #include "smt/smt_engine.h"
@@ -67,6 +68,7 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () :
   d_exprManager(em),
   d_nodeManager(em->getNodeManager()),
   d_options(opts) {
+
   NodeManagerScope nms(d_nodeManager);
   d_decisionEngine = new DecisionEngine;
   d_theoryEngine = new TheoryEngine(this, d_ctxt);
diff --git a/src/util/Assert.h b/src/util/Assert.h
index 8c230218c..ad3f4b1d3 100644
--- a/src/util/Assert.h
+++ b/src/util/Assert.h
@@ -212,6 +212,7 @@ extern __thread CVC4_PUBLIC const char* s_debugAssertionFailure;
           Warning() << "The propagating exception is:" << std::endl     \
                     << s_debugAssertionFailure << std::endl                  \
                     << "===========================================" << std::endl; \
+          s_debugAssertionFailure = NULL;                               \
         }                                                               \
       } else {                                                          \
         throw AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
diff --git a/test/system/Makefile.am b/test/system/Makefile.am
index 15f781333..59a37a4db 100644
--- a/test/system/Makefile.am
+++ b/test/system/Makefile.am
@@ -22,6 +22,17 @@ TEST_DEPS = \
 EXTRA_DIST = \
 	$(TEST_DEPS_DIST)
 
+if STATIC_BINARY
+system_LINK = $(CXXLINK) -all-static
+else
+system_LINK = $(CXXLINK)
+endif
+
+# WHEN SYSTEM TESTS ARE ADDED, BUILD LIKE THIS:
+# system_test: system_test.cpp
+# 	$(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS) -c -o $@.lo $<
+# 	$(AM_V_CXXLD)$(system_LINK) $(AM_LDFLAGS) $@.lo
+
 # rebuild tests if a library changes
 $(TESTS):: $(TEST_DEPS)
 
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 967d6a8c8..9d1a2995b 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -64,18 +64,24 @@ MOSTLYCLEANFILES = $(UNIT_TESTS) $(UNIT_TESTS:%=%.cpp)
 # that file for comment)
 # TESTS =
 
+if STATIC_BINARY
+unit_LINK = $(CXXLINK) -all-static
+else
+unit_LINK = $(CXXLINK)
+endif
+
 $(UNIT_TESTS:%=%.cpp): %.cpp: %.h
-	mkdir -p `dirname "$@"`
-	$(CXXTESTGEN) --have-eh --have-std --error-printer -o "$@" "$<"
+	$(AM_V_at)mkdir -p `dirname "$@"`
+	$(AM_V_GEN)$(CXXTESTGEN) --have-eh --have-std --error-printer -o "$@" "$<"
 $(WHITE_TESTS): %_white: %_white.cpp $(TEST_DEPS)
-	$(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -c -o $@.lo $<
-	$(CXXLINK) $(AM_LDFLAGS_WHITE) $@.lo
+	$(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -c -o $@.lo $<
+	$(AM_V_CXXLD)$(unit_LINK) $(AM_LDFLAGS_WHITE) $@.lo
 $(BLACK_TESTS): %_black: %_black.cpp $(TEST_DEPS)
-	$(LTCXXCOMPILE) $(AM_CXXFLAGS_BLACK) -c -o $@.lo $<
-	$(CXXLINK) $(AM_LDFLAGS_BLACK) $@.lo
+	$(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_BLACK) -c -o $@.lo $<
+	$(AM_V_CXXLD)$(unit_LINK) $(AM_LDFLAGS_BLACK) $@.lo
 $(PUBLIC_TESTS): %_public: %_public.cpp $(TEST_DEPS)
-	$(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -c -o $@.lo $<
-	$(CXXLINK) $(AM_LDFLAGS_PUBLIC) $@.lo
+	$(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -c -o $@.lo $<
+	$(AM_V_CXXLD)$(unit_LINK) $(AM_LDFLAGS_PUBLIC) $@.lo
 
 else