From: Morgan Deters <mdeters@gmail.com>
Date: Sun, 4 Apr 2010 23:03:52 +0000 (+0000)
Subject: * Addressed issues brought up in Chris's review of Morgan's
X-Git-Tag: cvc5-1.0.0~9138
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ff53861016427723a7c29e9bbca6f497b4556164;p=cvc5.git

* Addressed issues brought up in Chris's review of Morgan's
  NodeManager (bug #65).  Better documentation, etc.

* As part of this, removed NodeManager::mkVar() (which created a
  variable of unknown type).  This requires changes to lots of unit
  tests, which were using this function.

* Performed some review of parser code (my code review #73).

  + I changed the way exceptions were caught and rethrown in
    src/parser/input.cpp.

  + ParserExceptions weren't being properly constructed (d_line and
    d_column weren't intiialized and could contain junk, leading to
    weird error messages).  Fixed.

* Fix to the current working directory used by run_regression script.
  Makes exceptional output easier to match against (in expected error
  output).

* (configure.ac) Ensure that CFLAGS has -fexceptions in it, in case we
  compile any C code and don't use the C++ compiler.
---

diff --git a/configure.ac b/configure.ac
index 7007ba47f..d23cf4a6d 100644
--- a/configure.ac
+++ b/configure.ac
@@ -165,7 +165,8 @@ fi
 # Unpack standard build types. Any particular options can be overriden with
 # --enable/disable-X options
 if test -z "${OPTLEVEL+set}"; then OPTLEVEL=3; fi
-# our defaults for CXXFLAGS are better than autoconf's
+# our defaults for CFLAGS/CXXFLAGS are better than autoconf's
+if test -z "${CFLAGS+set}"; then CFLAGS=; fi
 if test -z "${CXXFLAGS+set}"; then CXXFLAGS=; fi
 case "$with_build" in
   production) # highly optimized, no assertions, no tracing
@@ -477,7 +478,7 @@ AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full releas
 
 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }$CVC4CPPFLAGS"
 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
-CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated"
+CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions"
 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
 
 FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 213a4cb35..5c0cfb987 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -241,7 +241,8 @@ class MultNodeBuilder;
 /**
  * A base class for NodeBuilders.  When extending this class, use:
  *
- *   class MyExtendedNodeBuilder : public NodeBuilderBase<MyExtendedNodeBuilder> { ... };
+ *   class MyExtendedNodeBuilder :
+ *       public NodeBuilderBase<MyExtendedNodeBuilder> { ... };
  *
  * This ensures that certain member functions return the right
  * (derived) class type.
@@ -396,13 +397,14 @@ protected:
       expr::NodeValue* newBlock = (expr::NodeValue*)
         std::realloc(d_nv,
                      sizeof(expr::NodeValue) +
-                     ( sizeof(expr::NodeValue*) * (d_nvMaxChildren = d_nv->d_nchildren) ));
+                     ( 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_nvMaxChildren = d_nv->d_nchildren;
       d_nv = newBlock;
     }
   }
@@ -446,37 +448,43 @@ public:
 
   /** 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(!isUsed(), "NodeBuilder is one-shot only; "
+           "attempt to access it after conversion");
     return d_nv->begin<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(!isUsed(), "NodeBuilder is one-shot only; "
+           "attempt to access it after conversion");
     return d_nv->end<true>();
   }
 
   /** 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");
+    Assert(!isUsed(), "NodeBuilder is one-shot only; "
+           "attempt to access it after conversion");
     return d_nv->getKind();
   }
 
   /** 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(!isUsed(), "NodeBuilder is one-shot only; "
+           "attempt to access it after conversion");
     return d_nv->getMetaKind();
   }
 
   /** 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(!isUsed(), "NodeBuilder is one-shot only; "
+           "attempt to access it after conversion");
     return 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(!isUsed(), "NodeBuilder is one-shot only; "
+           "attempt to access it after conversion");
     Assert(i >= 0 && unsigned(i) < d_nv->getNumChildren(),
            "index out of range for NodeBuilder[]");
     return Node(d_nv->getChild(i));
@@ -500,7 +508,8 @@ public:
 
   /** 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(!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");
     AssertArgument(k != kind::UNDEFINED_KIND &&
@@ -518,7 +527,8 @@ public:
    * 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");
+    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();
@@ -529,15 +539,19 @@ public:
   }
 
   /** 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");
+  template <bool ref_count>
+  inline Builder&
+  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());
   }
 
   /** Append a sequence of children to this Node-under-construction. */
   template <class Iterator>
   Builder& append(const Iterator& begin, const Iterator& end) {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+    Assert(!isUsed(), "NodeBuilder is one-shot only; "
+           "attempt to access it after conversion");
     for(Iterator i = begin; i != end; ++i) {
       append(*i);
     }
@@ -546,7 +560,8 @@ public:
 
   /** 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");
+    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");
     allocateNvIfNecessaryForAppend();
     expr::NodeValue* nv = n.d_nv;
@@ -561,7 +576,8 @@ public:
   operator Node() const;
 
   inline void toStream(std::ostream& out, int depth = -1) const {
-    Assert(!isUsed(), "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, depth);
   }
 
@@ -596,7 +612,9 @@ public:
     NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) {
   }
 
-  inline BackedNodeBuilder(expr::NodeValue* buf, unsigned maxChildren, NodeManager* nm) :
+  inline BackedNodeBuilder(expr::NodeValue* buf,
+                           unsigned maxChildren,
+                           NodeManager* nm) :
     NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) {
   }
 
@@ -627,8 +645,12 @@ private:
  */
 #define makeStackNodeBuilder(__v, __n)                                  \
   const size_t __cvc4_backednodebuilder_nchildren__ ## __v = (__n);     \
-  ::CVC4::expr::NodeValue __cvc4_backednodebuilder_buf__ ## __v[1 + (((sizeof(::CVC4::expr::NodeValue) + sizeof(::CVC4::expr::NodeValue*) + 1) / sizeof(::CVC4::expr::NodeValue*)) * __cvc4_backednodebuilder_nchildren__ ## __v)]; \
-  ::CVC4::BackedNodeBuilder __v(__cvc4_backednodebuilder_buf__ ## __v, \
+  ::CVC4::expr::NodeValue __cvc4_backednodebuilder_buf__ ## __v         \
+      [1 + ( ( ( sizeof(::CVC4::expr::NodeValue) +                      \
+                sizeof(::CVC4::expr::NodeValue*) + 1 ) /                \
+               sizeof(::CVC4::expr::NodeValue*) ) *                     \
+             __cvc4_backednodebuilder_nchildren__ ## __v)];             \
+  ::CVC4::BackedNodeBuilder __v(__cvc4_backednodebuilder_buf__ ## __v,  \
                                 __cvc4_backednodebuilder_nchildren__ ## __v)
 // IF THE ABOVE ASSERTION FAILS, write another compiler-specific
 // version of makeStackNodeBuilder() that works for your compiler
@@ -718,7 +740,8 @@ public:
   // 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
+  // This is needed for copy constructors of different sizes to access
+  // private fields
   template <unsigned N>
   friend class NodeBuilder;
 
@@ -845,7 +868,8 @@ inline Builder& NodeBuilderBase<Builder>::operator+=(TNode e) {
 
 template <class Builder>
 inline Builder& NodeBuilderBase<Builder>::operator-=(TNode e) {
-  return collapseTo(kind::PLUS).append(NodeManager::currentNM()->mkNode(kind::UMINUS, e));
+  return collapseTo(kind::PLUS).
+    append(NodeManager::currentNM()->mkNode(kind::UMINUS, e));
 }
 
 template <class Builder>
@@ -1171,12 +1195,13 @@ void NodeBuilderBase<Builder>::realloc(size_t toSize) {
     // 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 = toSize) ));
+                   ( 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;
     // Here, the copy (between two heap-allocated buffers) has already
     // been done for us by the std::realloc().
     d_nv = newBlock;
@@ -1184,10 +1209,11 @@ void NodeBuilderBase<Builder>::realloc(size_t toSize) {
     // Ensure d_nv is not modified on allocation failure
     expr::NodeValue* newBlock = (expr::NodeValue*)
       std::malloc(sizeof(expr::NodeValue) +
-                  ( sizeof(expr::NodeValue*) * (d_nvMaxChildren = toSize) ));
+                  ( sizeof(expr::NodeValue*) * toSize ));
     if(newBlock == NULL) {
       throw std::bad_alloc();
     }
+    d_nvMaxChildren = toSize;
 
     d_nv = newBlock;
     d_nv->d_id = 0;
@@ -1239,7 +1265,8 @@ void NodeBuilderBase<Builder>::decrRefCounts() {
 // 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(!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!");
 
@@ -1410,7 +1437,8 @@ NodeBuilderBase<Builder>::operator Node() {
 // 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(!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!");
 
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 8f254ed9f..e735b7f09 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -58,33 +58,41 @@ NodeManager::~NodeManager() {
 }
 
 /**
- * This class ensure that NodeManager::d_reclaiming gets set to false
+ * This class ensures 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;
   }
 };
 
+/**
+ * Similarly, ensure d_nodeUnderDeletion gets set to NULL even on
+ * exceptional exit from NodeManager::reclaimZombies().
+ */
 struct NVReclaim {
-  NodeValue*& d_reclaimField;
-  NVReclaim(NodeValue*& reclaim) :
-    d_reclaimField(reclaim) {
+  NodeValue*& d_deletionField;
+
+  NVReclaim(NodeValue*& deletionField) :
+    d_deletionField(deletionField) {
 
     Debug("gc") << ">> setting NVRECLAIM field\n";
   }
+
   ~NVReclaim() {
     Debug("gc") << "<< clearing NVRECLAIM field\n";
-    d_reclaimField = NULL;
+    d_deletionField = NULL;
   }
 };
 
@@ -107,11 +115,11 @@ void NodeManager::reclaimZombies() {
   // 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.
+  // One way to handle B's zombification would be simply to put it
+  // into d_zombies.  This is what we do.  However, if we were to
+  // concurrently process d_zombies in the loop below, such addition
+  // may be invisible to us (B is leaked) or even invalidate our
+  // iterator, causing a crash.  So we need to copy the set away.
 
   vector<NodeValue*> zombies;
   zombies.reserve(d_zombies.size());
@@ -149,6 +157,6 @@ void NodeManager::reclaimZombies() {
       free(nv);
     }
   }
-}
+}/* NodeManager::reclaimZombies() */
 
 }/* CVC4 namespace */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 71242f2e1..04d2ddac7 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -65,25 +65,100 @@ class NodeManager {
 
   expr::attr::AttributeManager d_attrManager;
 
+  /**
+   * The node value we're currently freeing.  This unique node value
+   * is permitted to have outstanding TNodes to it (in "soft"
+   * contexts, like as a key in attribute tables), even though
+   * normally it's an error to have a TNode to a node value with a
+   * reference count of 0.  Being "under deletion" also enables
+   * assertions that inc() is not called on it.  (A poorly-behaving
+   * attribute cleanup function could otherwise create a "Node" that
+   * points to the node value that is in the process of being deleted,
+   * springing it back to life.)
+   */
   expr::NodeValue* d_nodeUnderDeletion;
+
+  /**
+   * True iff we are in reclaimZombies().  This avoids unnecessary
+   * recursion; a NodeValue being deleted might zombify other
+   * NodeValues, but these shouldn't trigger a (recursive) call to
+   * reclaimZombies().
+   */
   bool d_reclaiming;
+
+  /**
+   * The set of zombie nodes.  We may want to revisit this design, as
+   * we might like to delete nodes in least-recently-used order.  But
+   * we also need to avoid processing a zombie twice.
+   */
   ZombieSet d_zombies;
 
+  /**
+   * A set of operator singletons (w.r.t.  to this NodeManager
+   * instance) for operators.  Conceptually, Nodes with kind, say,
+   * PLUS, are APPLYs of a PLUS operator to arguments.  This array
+   * holds the set of operators for these things.  A PLUS operator is
+   * a Node with kind "BUILTIN", and if you call
+   * plusOperator->getConst<CVC4::Kind>(), you get kind::PLUS back.
+   */
+  Node d_operators[kind::LAST_KIND];
+
+  /**
+   * Look up a NodeValue in the pool associated to this NodeManager.
+   * The NodeValue argument need not be a "completely-constructed"
+   * NodeValue.  In particular, "non-inlined" constants are permited
+   * (see below).
+   *
+   * For non-CONSTANT metakinds, nv's d_kind and d_nchildren should be
+   * correctly set, and d_children[0..n-1] should be valid (extant)
+   * NodeValues for lookup.
+   *
+   * For CONSTANT metakinds, nv's d_kind should be set correctly.
+   * Normally a CONSTANT would have d_nchildren == 0 and the constant
+   * value inlined in the d_children space.  However, here we permit
+   * "non-inlined" NodeValues to avoid unnecessary copying.  For
+   * these, d_nchildren == 1, and d_nchildren is a pointer to the
+   * constant value.
+   *
+   * The point of this complex design is to permit efficient lookups
+   * (without fully constructing a NodeValue).  In the case that the
+   * argument is not fully constructed, and this function returns
+   * NULL, the caller should fully construct an equivalent one before
+   * calling poolInsert().  NON-FULLY-CONSTRUCTED NODEVALUES are not
+   * permitted in the pool!
+   */
   inline expr::NodeValue* poolLookup(expr::NodeValue* nv) const;
-  void poolInsert(expr::NodeValue* nv);
+
+  /**
+   * Insert a NodeValue into the NodeManager's pool.
+   *
+   * It is an error to insert a NodeValue already in the pool.
+   * Enquire first with poolLookup().
+   */
+  inline void poolInsert(expr::NodeValue* nv);
+
+  /**
+   * Remove a NodeValue from the NodeManager's pool.
+   *
+   * It is an error to request the removal of a NodeValue from the
+   * pool that is not in the pool.
+   */
   inline void poolRemove(expr::NodeValue* nv);
 
-  bool isCurrentlyDeleting(const expr::NodeValue* nv) const{
+  /**
+   * Determine if nv is currently being deleted by the NodeManager.
+   */
+  inline bool isCurrentlyDeleting(const expr::NodeValue* nv) const {
     return d_nodeUnderDeletion == nv;
   }
 
-  Node d_operators[kind::LAST_KIND];
-
   /**
    * Register a NodeValue as a zombie.
    */
   inline void gc(expr::NodeValue* nv) {
     Assert(nv->d_rc == 0);
+    // if d_reclaiming is set, make sure we don't call
+    // reclaimZombies(), because it's already running.
     if(d_reclaiming) {// FIXME multithreading
       // currently reclaiming zombies; just push onto the list
       Debug("gc") << "zombifying node value " << nv
@@ -169,6 +244,7 @@ public:
   static NodeManager* currentNM() { return s_current; }
 
   // general expression-builders
+
   /** Create a node with no children. */
   Node mkNode(Kind kind);
 
@@ -182,33 +258,45 @@ public:
   Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3);
 
   /** Create a node with four children. */
-  Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4);
+  Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3,
+              TNode child4);
 
   /** Create a node with five children. */
-  Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4, TNode child5);
+  Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3,
+              TNode child4, TNode child5);
 
   /** Create a node with an arbitrary number of children. */
-  Node mkNode(Kind kind, const std::vector<Node>& children);
-
-  // NOTE: variables are special, because duplicates are permitted
+  template <bool ref_count>
+  Node mkNode(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
 
-  /** Create a variable with the given type and name. */
+  /**
+   * Create a variable with the given type and name.  NOTE that no
+   * lookup is done on the name.  If you mkVar(type, "a") and then
+   * mkVar(type, "a") again, you have two variables.
+   */
   Node mkVar(Type* type, const std::string& name);
 
   /** Create a variable with the given type. */
   Node mkVar(Type* type);
 
-  /** Create a variable of unknown type (?). */
-  Node mkVar();
-
-  /** Create a constant of type T */
+  /**
+   * Create a constant of type T.  It will have the appropriate
+   * CONST_* kind defined for T.
+   */
   template <class T>
   Node mkConst(const T&);
 
-  /** Determine whether Nodes of a particular Kind have operators. */
-  static inline bool hasOperator(Kind mk);
+  /**
+   * Determine whether Nodes of a particular Kind have operators.
+   * @returns true if Nodes of Kind k have operators.
+   */
+  static inline bool hasOperator(Kind k);
 
-  /** Get the (singleton) operator of an OPERATOR-kinded kind. */
+  /**
+   * Get the (singleton) operator of an OPERATOR-kinded kind.  The
+   * returned node n will have kind BUILTIN, and calling
+   * n.getConst<CVC4::Kind>() will yield k.
+   */
   inline TNode operatorOf(Kind k) {
     AssertArgument( kind::metaKindOf(k) == kind::metakind::OPERATOR, k,
                     "Kind is not an OPERATOR-kinded kind "
@@ -216,7 +304,8 @@ public:
     return d_operators[k];
   }
 
-  /** Retrieve an attribute for a node.
+  /**
+   * Retrieve an attribute for a node.
    *
    * @param nv the node value
    * @param attr an instance of the attribute kind to retrieve.
@@ -227,43 +316,52 @@ public:
   inline typename AttrKind::value_type getAttribute(expr::NodeValue* nv,
                                                     const AttrKind& attr) const;
 
-  /** Check whether an attribute is set for a node.
+  /**
+   * Check whether an attribute is set for a node.
    *
    * @param nv the node value
    * @param attr an instance of the attribute kind to check
-   * @returns <code>true</code> iff <code>attr</code> is set for <code>nv</code>.
+   * @returns <code>true</code> iff <code>attr</code> is set for
+   * <code>nv</code>.
    */
   template <class AttrKind>
   inline bool hasAttribute(expr::NodeValue* nv,
                            const AttrKind& attr) const;
 
-  /** Check whether an attribute is set for a node.
+  /**
+   * Check whether an attribute is set for a node, and, if so,
+   * retrieve it.
    *
    * @param nv the node value
    * @param attr an instance of the attribute kind to check
    * @param value a reference to an object of the attribute's value type.
    * <code>value</code> will be set to the value of the attribute, if it is
-   * set for <code>nv</code>; otherwise, it will be set to the default value of
-   * the attribute.
-   * @returns <code>true</code> iff <code>attr</code> is set for <code>nv</code>.
+   * set for <code>nv</code>; otherwise, it will be set to the default
+   * value of the attribute.
+   * @returns <code>true</code> iff <code>attr</code> is set for
+   * <code>nv</code>.
    */
   template <class AttrKind>
   inline bool getAttribute(expr::NodeValue* nv,
                            const AttrKind& attr,
                            typename AttrKind::value_type& value) const;
 
-  /** Set an attribute for a node.
-    *
-    * @param nv the node value
-    * @param attr an instance of the attribute kind to set
-    * @param value the value of <code>attr</code> for <code>nv</code>
-    */
+  /**
+   * Set an attribute for a node.  If the node doesn't have the
+   * attribute, this function assigns one.  If the node has one, this
+   * overwrites it.
+   *
+   * @param nv the node value
+   * @param attr an instance of the attribute kind to set
+   * @param value the value of <code>attr</code> for <code>nv</code>
+   */
   template <class AttrKind>
   inline void setAttribute(expr::NodeValue* nv,
                            const AttrKind&,
                            const typename AttrKind::value_type& value);
 
-  /** Retrieve an attribute for a TNode.
+  /**
+   * Retrieve an attribute for a TNode.
    *
    * @param n the node
    * @param attr an instance of the attribute kind to retrieve.
@@ -274,12 +372,8 @@ public:
   inline typename AttrKind::value_type getAttribute(TNode n,
                                                     const AttrKind&) const;
 
-  /* NOTE: 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. */
-
-  /** Check whether an attribute is set for a TNode.
+  /**
+   * Check whether an attribute is set for a TNode.
    *
    * @param n the node
    * @param attr an instance of the attribute kind to check
@@ -289,7 +383,9 @@ public:
   inline bool hasAttribute(TNode n,
                            const AttrKind& attr) const;
 
-  /** Check whether an attribute is set for a TNode.
+  /**
+   * Check whether an attribute is set for a TNode and, if so, retieve
+   * it.
    *
    * @param n the node
    * @param attr an instance of the attribute kind to check
@@ -304,33 +400,46 @@ public:
                            const AttrKind& attr,
                            typename AttrKind::value_type& value) const;
 
-  /** Set an attribute for a TNode.
-    *
-    * @param n the node
-    * @param attr an instance of the attribute kind to set
-    * @param value the value of <code>attr</code> for <code>n</code>
-    */
+  /**
+   * Set an attribute for a node.  If the node doesn't have the
+   * attribute, this function assigns one.  If the node has one, this
+   * overwrites it.
+   *
+   * @param n the node
+   * @param attr an instance of the attribute kind to set
+   * @param value the value of <code>attr</code> for <code>n</code>
+   */
   template <class AttrKind>
   inline void setAttribute(TNode n,
                            const AttrKind&,
                            const typename AttrKind::value_type& value);
 
-  /** Get the type for booleans. */
+  /** Get the (singleton) type for booleans. */
   inline BooleanType* booleanType() const {
     return BooleanType::getInstance();
   }
 
-  /** Get the type for sorts. */
+  /** Get the (singleton) type for sorts. */
   inline KindType* kindType() const {
     return KindType::getInstance();
   }
 
-  /** Make a function type from domain to range. */
+  /**
+   * Make a function type from domain to range.
+   *
+   * @param domain the domain type
+   * @param range the range type
+   * @returns the functional type domain -> range
+   */
   inline FunctionType* mkFunctionType(Type* domain, Type* range) const;
 
   /**
    * Make a function type with input types from
    * argTypes. <code>argTypes</code> must have at least one element.
+   *
+   * @param argTypes the domain is a tuple (argTypes[0], ..., argTypes[n])
+   * @param range the range type
+   * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range
    */
   inline FunctionType* mkFunctionType(const std::vector<Type*>& argTypes,
                                       Type* range) const;
@@ -399,24 +508,37 @@ public:
 
   NodeManagerScope(NodeManager* nm) : d_oldNodeManager(NodeManager::s_current) {
     NodeManager::s_current = nm;
-    Debug("current") << "node manager scope: " << NodeManager::s_current << "\n";
+    Debug("current") << "node manager scope: "
+                     << NodeManager::s_current << "\n";
   }
 
   ~NodeManagerScope() {
     NodeManager::s_current = d_oldNodeManager;
-    Debug("current") << "node manager scope: returning to " << NodeManager::s_current << "\n";
+    Debug("current") << "node manager scope: "
+                     << "returning to " << NodeManager::s_current << "\n";
   }
 };
 
 /**
- * Creates
- * a <code>NodeManagerScope</code> with the underlying <code>NodeManager</code>
- * of a given <code>Expr</code> or <code>ExprManager</code>.
- * The <code>NodeManagerScope</code> is destroyed when the <code>ExprManagerScope</code>
- * is destroyed. See <code>NodeManagerScope</code> for more information.
+ * Creates a <code>NodeManagerScope</code> with the underlying
+ * <code>NodeManager</code> of a given <code>Expr</code> or
+ * <code>ExprManager</code>.  The <code>NodeManagerScope</code> is
+ * destroyed when the <code>ExprManagerScope</code> is destroyed. See
+ * <code>NodeManagerScope</code> for more information.
  */
-// NOTE: Without this, we'd need Expr to be a friend of ExprManager.
-// [chris 3/25/2010] Why?
+// NOTE: Here, it seems ExprManagerScope is redundant, since we have
+// NodeManagerScope already.  However, without this class, we'd need
+// Expr to be a friend of ExprManager, because in the implementation
+// of Expr functions, it needs to set the current NodeManager
+// correctly (and to do that it needs access to
+// ExprManager::getNodeManager()).  So, we make ExprManagerScope a
+// friend of ExprManager's, since it's implementation is simple to
+// read and understand (and verify that it doesn't do any mischief).
+//
+// ExprManager::getNodeManager() can't just be made public, since
+// ExprManager is exposed to clients of the library and NodeManager is
+// not.  Similarly, ExprManagerScope shouldn't go in expr_manager.h,
+// since that's a public header.
 class ExprManagerScope {
   NodeManagerScope d_nms;
 public:
@@ -431,8 +553,8 @@ public:
 };
 
 template <class AttrKind>
-inline typename AttrKind::value_type NodeManager::getAttribute(expr::NodeValue* nv,
-                                                               const AttrKind&) const {
+inline typename AttrKind::value_type
+NodeManager::getAttribute(expr::NodeValue* nv, const AttrKind&) const {
   return d_attrManager.getAttribute(nv, AttrKind());
 }
 
@@ -443,42 +565,42 @@ inline bool NodeManager::hasAttribute(expr::NodeValue* nv,
 }
 
 template <class AttrKind>
-inline bool NodeManager::getAttribute(expr::NodeValue* nv,
-                                      const AttrKind&,
-                                      typename AttrKind::value_type& ret) const {
+inline bool
+NodeManager::getAttribute(expr::NodeValue* nv, const AttrKind&,
+                          typename AttrKind::value_type& ret) const {
   return d_attrManager.getAttribute(nv, AttrKind(), ret);
 }
 
 template <class AttrKind>
-inline void NodeManager::setAttribute(expr::NodeValue* nv,
-                                      const AttrKind&,
-                                      const typename AttrKind::value_type& value) {
+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 {
+inline typename AttrKind::value_type
+NodeManager::getAttribute(TNode n, const AttrKind&) const {
   return d_attrManager.getAttribute(n.d_nv, AttrKind());
 }
 
 template <class AttrKind>
-inline bool NodeManager::hasAttribute(TNode n,
-                                      const AttrKind&) const {
+inline bool
+NodeManager::hasAttribute(TNode n, const AttrKind&) const {
   return d_attrManager.hasAttribute(n.d_nv, AttrKind());
 }
 
 template <class AttrKind>
-inline bool NodeManager::getAttribute(TNode n,
-                                      const AttrKind&,
-                                      typename AttrKind::value_type& ret) const {
+inline bool
+NodeManager::getAttribute(TNode n, const AttrKind&,
+                          typename AttrKind::value_type& ret) const {
   return d_attrManager.getAttribute(n.d_nv, AttrKind(), ret);
 }
 
 template <class AttrKind>
-inline void NodeManager::setAttribute(TNode n,
-                                      const AttrKind&,
-                                      const typename AttrKind::value_type& value) {
+inline void
+NodeManager::setAttribute(TNode n, const AttrKind&,
+                          const typename AttrKind::value_type& value) {
   d_attrManager.setAttribute(n.d_nv, AttrKind(), value);
 }
 
@@ -574,6 +696,7 @@ inline void NodeManager::poolInsert(expr::NodeValue* nv) {
 inline void NodeManager::poolRemove(expr::NodeValue* nv) {
   Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end(),
          "NodeValue is not in the pool!");
+
   d_nodeValuePool.erase(nv);// FIXME multithreading
 }
 
@@ -620,20 +743,27 @@ inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2) {
   return NodeBuilder<>(this, kind) << child1 << child2;
 }
 
-inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3) {
+inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
+                                TNode child3) {
   return NodeBuilder<>(this, kind) << child1 << child2 << child3;
 }
 
-inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4) {
+inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
+                                TNode child3, TNode child4) {
   return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4;
 }
 
-inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4, TNode child5) {
-  return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4 << child5;
+inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
+                                TNode child3, TNode child4, TNode child5) {
+  return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4
+                                   << child5;
 }
 
 // N-ary version
-inline Node NodeManager::mkNode(Kind kind, const std::vector<Node>& children) {
+template <bool ref_count>
+inline Node NodeManager::mkNode(Kind kind,
+                                const std::vector<NodeTemplate<ref_count> >&
+                                children) {
   return NodeBuilder<>(this, kind).append(children);
 }
 
@@ -644,17 +774,12 @@ inline Node NodeManager::mkVar(Type* type, const std::string& name) {
 }
 
 inline Node NodeManager::mkVar(Type* type) {
-  Node n = mkVar();
+  Node n = Node(NodeBuilder<>(this, kind::VARIABLE));
   type->inc();// reference-count the type
   n.setAttribute(TypeAttr(), type);
   return n;
 }
 
-inline Node NodeManager::mkVar() {
-  // TODO: rewrite to not use NodeBuilder
-  return NodeBuilder<>(this, kind::VARIABLE);
-}
-
 template <class T>
 Node NodeManager::mkConst(const T& val) {
   // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t;
diff --git a/src/parser/input.cpp b/src/parser/input.cpp
index 4d5f348d8..fd1a4cbd6 100644
--- a/src/parser/input.cpp
+++ b/src/parser/input.cpp
@@ -43,7 +43,7 @@ void Input::enableChecks() {
   d_parserState->enableChecks();
 }
 
-Command* Input::parseNextCommand() throw (ParserException) {
+Command* Input::parseNextCommand() throw(ParserException) {
   Debug("parser") << "parseNextCommand()" << std::endl;
   Command* cmd = NULL;
   if(!done()) {
@@ -54,14 +54,14 @@ Command* Input::parseNextCommand() throw (ParserException) {
       }
     } catch(ParserException& e) {
       d_parserState->setDone();
-      throw ParserException(e.toString());
+      throw;
     }
   }
   Debug("parser") << "parseNextCommand() => " << cmd << std::endl;
   return cmd;
 }
 
-Expr Input::parseNextExpression() throw (ParserException) {
+Expr Input::parseNextExpression() throw(ParserException) {
   Debug("parser") << "parseNextExpression()" << std::endl;
   Expr result;
   if(!done()) {
@@ -71,7 +71,7 @@ Expr Input::parseNextExpression() throw (ParserException) {
         d_parserState->setDone();
     } catch(ParserException& e) {
       d_parserState->setDone();
-      throw ParserException(e.toString());
+      throw;
     }
   }
   Debug("parser") << "parseNextExpression() => " << result << std::endl;
diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h
index 7b0f8bda9..dfca01ce2 100644
--- a/src/parser/parser_exception.h
+++ b/src/parser/parser_exception.h
@@ -30,9 +30,26 @@ namespace parser {
 class CVC4_PUBLIC ParserException : public Exception {
 public:
   // Constructors
-  ParserException() { }
-  ParserException(const std::string& msg): Exception(msg) { }
-  ParserException(const char* msg): Exception(msg) { }
+  ParserException() :
+    d_filename(),
+    d_line(0),
+    d_column(0) {
+  }
+
+  ParserException(const std::string& msg) :
+    Exception(msg),
+    d_filename(),
+    d_line(0),
+    d_column(0) {
+  }
+
+  ParserException(const char* msg) :
+    Exception(msg),
+    d_filename(),
+    d_line(0),
+    d_column(0) {
+  }
+
   ParserException(const std::string& msg, const std::string& filename,
                   unsigned long line, unsigned long column) :
     Exception(msg),
@@ -43,11 +60,12 @@ public:
 
   // Destructor
   virtual ~ParserException() throw() {}
+
   virtual std::string toString() const {
     if( d_line > 0 ) {
       std::stringstream ss;
-      ss <<  "Parser Error: " << d_filename << ":" << d_line << "."
-           << d_column << ": " << d_msg;
+      ss <<  "Parse Error: " << d_filename << ":" << d_line << "."
+         << d_column << ": " << d_msg;
       return ss.str();
     } else {
       return "Parse Error: " + d_msg;
diff --git a/test/regress/regress0/error.cvc b/test/regress/regress0/error.cvc
index 09a69e212..982731b34 100644
--- a/test/regress/regress0/error.cvc
+++ b/test/regress/regress0/error.cvc
@@ -1,4 +1,4 @@
 % EXPECT-ERROR: CVC4 Error:
-% EXPECT-ERROR: Parse Error: Parser Error: error.cvc:3.9: Symbol BOOL not declared
+% EXPECT-ERROR: Parse Error: error.cvc:3.9: Symbol BOOL not declared
 p : BOOL;
 % EXIT: 1
diff --git a/test/regress/run_regression b/test/regress/run_regression
index 65ab6c31a..439c8e6c9 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -77,7 +77,17 @@ else
   echo "$expected_error" >"$experrfile"
 fi
 
-("$cvc4" --segv-nospin "$benchmark"; echo $? >"$exitstatusfile") > "$outfile" 2> "$errfile"
+cvc4dir=`dirname "$cvc4"`
+cvc4dirfull=`cd "$cvc4dir" && pwd`
+if [ -z "$cvc4dirfull" ]; then
+  error "getting directory of \`$cvc4 !?"
+fi
+cvc4base=`basename "$cvc4"`
+cvc4full="$cvc4dirfull/$cvc4base"
+( cd `dirname "$benchmark"`;
+  "$cvc4full" --segv-nospin `basename "$benchmark"`;
+  echo $? >"$exitstatusfile"
+) > "$outfile" 2> "$errfile"
 
 diffs=`diff -u "$expoutfile" "$outfile"`
 diffexit=$?
diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h
index eb728c62c..e87c8d708 100644
--- a/test/unit/expr/attribute_black.h
+++ b/test/unit/expr/attribute_black.h
@@ -70,7 +70,8 @@ public:
   typedef expr::Attribute<MyDataAttributeId, MyData*, MyDataCleanupFunction> MyDataAttribute;
 
   void testDeallocation() {
-    Node* node = new Node(d_nodeManager->mkVar());
+    Type* booleanType = d_nodeManager->booleanType();
+    Node* node = new Node(d_nodeManager->mkVar(booleanType));
     MyData* data;
     MyData* data1;
     MyDataAttribute attr;
diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index 64c768a13..e0d9d6bf4 100644
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -60,6 +60,7 @@ class AttributeWhite : public CxxTest::TestSuite {
   Context* d_ctxt;
   NodeManager* d_nm;
   NodeManagerScope* d_scope;
+  Type* d_booleanType;
 
 public:
 
@@ -67,6 +68,8 @@ public:
     d_ctxt = new Context;
     d_nm = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nm);
+
+    d_booleanType = d_nm->booleanType();
   }
 
   void tearDown() {
@@ -150,9 +153,9 @@ public:
 
     //Debug.on("boolattr");
 
-    Node a = d_nm->mkVar();
-    Node b = d_nm->mkVar();
-    Node c = d_nm->mkVar();
+    Node a = d_nm->mkVar(d_booleanType);
+    Node b = d_nm->mkVar(d_booleanType);
+    Node c = d_nm->mkVar(d_booleanType);
 
     Debug("boolattr", "get flag 1 on a (should be F)\n");
     TS_ASSERT(! a.getAttribute(TestFlag1cd()));
@@ -280,10 +283,10 @@ public:
 
     //Debug.on("boolattr");
 
-    Node a = d_nm->mkVar();
-    Node b = d_nm->mkVar();
-    Node c = d_nm->mkVar();
-    Node unnamed = d_nm->mkVar();
+    Node a = d_nm->mkVar(d_booleanType);
+    Node b = d_nm->mkVar(d_booleanType);
+    Node c = d_nm->mkVar(d_booleanType);
+    Node unnamed = d_nm->mkVar(d_booleanType);
 
     a.setAttribute(VarNameAttr(), "a");
     b.setAttribute(VarNameAttr(), "b");
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index d420c6e26..9e199aa9a 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -36,6 +36,7 @@ private:
   Context* d_ctxt;
   NodeManager* d_nodeManager;
   NodeManagerScope* d_scope;
+  Type* d_booleanType;
 
 public:
 
@@ -43,6 +44,8 @@ public:
     d_ctxt = new Context;
     d_nodeManager = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nodeManager);
+
+    d_booleanType = d_nodeManager->booleanType();
   }
 
   void tearDown() {
@@ -94,12 +97,12 @@ public:
   void testOperatorEquals() {
     Node a, b, c;
 
-    b = d_nodeManager->mkVar();
+    b = d_nodeManager->mkVar(d_booleanType);
 
     a = b;
     c = a;
 
-    Node d = d_nodeManager->mkVar();
+    Node d = d_nodeManager->mkVar(d_booleanType);
 
     TS_ASSERT(a==a);
     TS_ASSERT(a==b);
@@ -134,12 +137,12 @@ public:
 
     Node a, b, c;
 
-    b = d_nodeManager->mkVar();
+    b = d_nodeManager->mkVar(d_booleanType);
 
     a = b;
     c = a;
 
-    Node d = d_nodeManager->mkVar();
+    Node d = d_nodeManager->mkVar(d_booleanType);
 
     /*structed assuming operator == works */
     TS_ASSERT(iff(a!=a, !(a==a)));
@@ -196,7 +199,7 @@ public:
   /*tests:   Node& operator=(const Node&); */
   void testOperatorAssign() {
     Node a, b;
-    Node c = d_nodeManager->mkNode(NOT, d_nodeManager->mkVar());
+    Node c = d_nodeManager->mkNode(NOT, d_nodeManager->mkVar(d_booleanType));
 
     b = c;
     TS_ASSERT(b==c);
@@ -317,8 +320,8 @@ public:
   void testIteNode() {
     /*Node iteNode(const Node& thenpart, const Node& elsepart) const;*/
 
-    Node a = d_nodeManager->mkVar();
-    Node b = d_nodeManager->mkVar();
+    Node a = d_nodeManager->mkVar(d_booleanType);
+    Node b = d_nodeManager->mkVar(d_booleanType);
 
     Node cnd = d_nodeManager->mkNode(PLUS, a, b);
     Node thenBranch = d_nodeManager->mkConst(true);
@@ -380,8 +383,8 @@ public:
   void testGetKind() {
     /*inline Kind getKind() const; */
 
-    Node a = d_nodeManager->mkVar();
-    Node b = d_nodeManager->mkVar();
+    Node a = d_nodeManager->mkVar(d_booleanType);
+    Node b = d_nodeManager->mkVar(d_booleanType);
 
     Node n = d_nodeManager->mkNode(NOT, a);
     TS_ASSERT(NOT == n.getKind());
@@ -463,9 +466,9 @@ public:
 
   void testIterator() {
     NodeBuilder<> b;
-    Node x = d_nodeManager->mkVar();
-    Node y = d_nodeManager->mkVar();
-    Node z = d_nodeManager->mkVar();
+    Node x = d_nodeManager->mkVar(d_booleanType);
+    Node y = d_nodeManager->mkVar(d_booleanType);
+    Node z = d_nodeManager->mkVar(d_booleanType);
     Node n = b << x << y << z << kind::AND;
 
     { // iterator
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index 2a7b3623e..eec6949f0 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -37,6 +37,7 @@ private:
   Context* d_ctxt;
   NodeManager* d_nm;
   NodeManagerScope* d_scope;
+  Type* d_booleanType;
 
 public:
 
@@ -44,7 +45,9 @@ public:
     d_ctxt = new Context;
     d_nm = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nm);
+
     specKind = PLUS;
+    d_booleanType = d_nm->booleanType();
   }
 
   void tearDown() {
@@ -209,9 +212,9 @@ public:
 
   void testIterator() {
     NodeBuilder<> b;
-    Node x = d_nm->mkVar();
-    Node y = d_nm->mkVar();
-    Node z = d_nm->mkVar();
+    Node x = d_nm->mkVar(d_booleanType);
+    Node y = d_nm->mkVar(d_booleanType);
+    Node z = d_nm->mkVar(d_booleanType);
     b << x << y << z << AND;
 
     {
@@ -460,9 +463,9 @@ public:
   }
 
   void testAppend() {
-    Node x = d_nm->mkVar();
-    Node y = d_nm->mkVar();
-    Node z = d_nm->mkVar();
+    Node x = d_nm->mkVar(d_booleanType);
+    Node y = d_nm->mkVar(d_booleanType);
+    Node z = d_nm->mkVar(d_booleanType);
     Node m = d_nm->mkNode(AND, y, z, x);
     Node n = d_nm->mkNode(OR, d_nm->mkNode(NOT, x), y, z);
     Node o = d_nm->mkNode(XOR, y, x);
@@ -587,12 +590,12 @@ public:
   }
 
   void testConvenienceBuilders() {
-    Node a = d_nm->mkVar();
-    Node b = d_nm->mkVar();
-    Node c = d_nm->mkVar();
-    Node d = d_nm->mkVar();
-    Node e = d_nm->mkVar();
-    Node f = d_nm->mkVar();
+    Node a = d_nm->mkVar(d_booleanType);
+    Node b = d_nm->mkVar(d_booleanType);
+    Node c = d_nm->mkVar(d_booleanType);
+    Node d = d_nm->mkVar(d_booleanType);
+    Node e = d_nm->mkVar(d_booleanType);
+    Node f = d_nm->mkVar(d_booleanType);
 
     Node m = a && b;
     Node n = a && b || c;
diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h
index a204d79b7..369be5a16 100644
--- a/test/unit/theory/theory_uf_white.h
+++ b/test/unit/theory/theory_uf_white.h
@@ -31,7 +31,6 @@ using namespace CVC4::context;
 
 using namespace std;
 
-
 /**
  * Very basic OutputChannel for testing simple Theory Behaviour.
  * Stores a call sequence for the output channel
@@ -95,6 +94,8 @@ class TheoryUFWhite : public CxxTest::TestSuite {
 
   TheoryUF* d_euf;
 
+  Type* d_booleanType;
+
 public:
 
   TheoryUFWhite() : d_level(Theory::FULL_EFFORT) {}
@@ -105,6 +106,8 @@ public:
     d_scope = new NodeManagerScope(d_nm);
     d_outputChannel.clear();
     d_euf = new TheoryUF(d_ctxt, d_outputChannel);
+
+    d_booleanType = d_nm->booleanType();
   }
 
   void tearDown() {
@@ -116,8 +119,8 @@ public:
   }
 
   void testPushPopChain() {
-    Node x = d_nm->mkVar();
-    Node f = d_nm->mkVar();
+    Node x = d_nm->mkVar(d_booleanType);
+    Node f = d_nm->mkVar(d_booleanType);
     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
     Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
     Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x);
@@ -171,8 +174,8 @@ public:
 
   /* test that {f(f(x)) == x, f(f(f(x))) != f(x)} is inconsistent */
   void testSimpleChain() {
-    Node x = d_nm->mkVar();
-    Node f = d_nm->mkVar();
+    Node x = d_nm->mkVar(d_booleanType);
+    Node f = d_nm->mkVar(d_booleanType);
     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
     Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
     Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x);
@@ -196,7 +199,7 @@ public:
 
   /* test that !(x == x) is inconsistent */
   void testSelfInconsistent() {
-    Node x = d_nm->mkVar();
+    Node x = d_nm->mkVar(d_booleanType);
     Node x_neq_x = (x.eqNode(x)).notNode();
 
     d_euf->assertFact(x_neq_x);
@@ -209,7 +212,7 @@ public:
 
   /* test that (x == x) is consistent */
   void testSelfConsistent() {
-    Node x = d_nm->mkVar();
+    Node x = d_nm->mkVar(d_booleanType);
     Node x_eq_x = x.eqNode(x);
 
     d_euf->assertFact(x_eq_x);
@@ -225,8 +228,8 @@ public:
       f(x) != x
      } is inconsistent */
   void testChain() {
-    Node x = d_nm->mkVar();
-    Node f = d_nm->mkVar();
+    Node x = d_nm->mkVar(d_booleanType);
+    Node f = d_nm->mkVar(d_booleanType);
     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
     Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
     Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x);
@@ -256,7 +259,7 @@ public:
 
 
   void testPushPopA() {
-    Node x = d_nm->mkVar();
+    Node x = d_nm->mkVar(d_booleanType);
     Node x_eq_x = x.eqNode(x);
 
     d_ctxt->push();
@@ -267,8 +270,8 @@ public:
   }
 
   void testPushPopB() {
-    Node x = d_nm->mkVar();
-    Node f = d_nm->mkVar();
+    Node x = d_nm->mkVar(d_booleanType);
+    Node f = d_nm->mkVar(d_booleanType);
     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
     Node f_x_eq_x = f_x.eqNode(x);