* public/private code untangled (smt/smt_engine.h no longer #includes

  expr/node.h).  This removes the warnings we had during compilation,
  and heads off a number of potential linking errors due to improper
  inlining of private (library-only) stuff in client (out-of-library)
  code.

* "configure" now takes some options as part of a "bare-option" build
  type (e.g., "./configure debug-coverage" or "./configure production-muzzle").

* split cdo.h, cdlist.h, cdmap.h, and cdset.h from context.h

* split cdlist_black unit test from context_black

* implement CDMap<>.

* give ExprManagers ownership of the context (and have SmtEngine share
  that one)

* fix main driver to properly report file-not-found

* fix MemoryMappedInputBuffer class to report reasons for
  "errno"-returned system errors

* src/expr/attribute.h: context-dependent attribute kinds now
  supported

* test/unit/expr/node_white.h: context-dependent attribute tests

* src/prop/cnf_conversion.h and associated parts of src/util/options.h
  and src/main/getopt.cpp: obsolete command-line option, removed.

* src/util/Assert.h: assertions are now somewhat more useful (in debug
  builds, anyway) during stack unwinding.

* test/unit/theory/theory_black.h: test context-dependent behavior of
  registerTerm() attribute for theories

* src/expr/node_builder.h: formatting, fixes for arithmetic
  convenience node builders, check memory allocations

* test/unit/expr/node_builder_black.h: add tessts for addition,
  subtraction, unary minus, and multiplication convenience node
  builders

* src/expr/attribute.h: more comments

* (various) code formatting, comment cleanup, added throws specifier
  to some destructors

* contrib/code-checker: prototype perl script to test (some) code policy

* contrib/indent-settings: command line for GNU indent to indent using
  CVC4 style (sort of; this is a work in progress)

* COPYING: legal stuff

* DESIGN_QUESTIONS: obsolete, removed

9 files changed, 472 insertions, 165 deletions

diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 522427c03..285c7ce87 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -28,7 +28,7 @@
 #include <ext/hash_map>
 
 #include "config.h"
-#include "context/context.h"
+#include "context/cdmap.h"
 #include "expr/node.h"
 #include "expr/type.h"
 
@@ -344,6 +344,25 @@ public:
   }
 };/* class AttrHash<bool> */
 
+/**
+ * A "CDAttrHash<value_type>"---the hash table underlying
+ * attributes---is simply a context-dependent mapping of
+ * pair<unique-attribute-id, Node> to value_type using our specialized
+ * hash function for these pairs.
+ */
+template <class value_type>
+class CDAttrHash :
+    public CVC4::context::CDMap<std::pair<uint64_t, NodeValue*>,
+                                value_type,
+                                AttrHashFcn> {
+public:
+  CDAttrHash(context::Context* ctxt) :
+    context::CDMap<std::pair<uint64_t, NodeValue*>,
+                   value_type,
+                   AttrHashFcn>(ctxt) {
+  }
+};
+
 }/* CVC4::expr::attr namespace */
 
 // ATTRIBUTE CLEANUP FUNCTIONS =================================================
@@ -353,7 +372,7 @@ namespace attr {
 /** Default cleanup for unmanaged Attribute<> */
 template <class T>
 struct AttributeCleanupFcn {
-  inline void cleanup(const T&) {}
+  static inline void cleanup(const T&) {}
 };
 
 /** Default cleanup for ManagedAttribute<> */
@@ -364,13 +383,13 @@ struct ManagedAttributeCleanupFcn {
 /** Specialization for T* */
 template <class T>
 struct ManagedAttributeCleanupFcn<T*> {
-  inline void cleanup(T* p) { delete p; }
+  static inline void cleanup(T* p) { delete p; }
 };
 
 /** Specialization for const T* */
 template <class T>
 struct ManagedAttributeCleanupFcn<const T*> {
-  inline void cleanup(const T* p) { delete p; }
+  static inline void cleanup(const T* p) { delete p; }
 };
 
 }/* CVC4::expr::attr namespace */
@@ -388,13 +407,13 @@ struct ManagedAttributeCleanupFcn<const T*> {
  * Node goes away.  Useful, e.g., for pointer-valued attributes when
  * the values are "owned" by the table.
  *
- * @param context_dependent whether this attribute kind is
+ * @param context_dep whether this attribute kind is
  * context-dependent
  */
 template <class T,
           class value_t,
           class CleanupFcn = attr::AttributeCleanupFcn<value_t>,
-          bool context_dependent = false>
+          bool context_dep = false>
 struct Attribute {
 
   /** The value type for this attribute. */
@@ -411,6 +430,11 @@ struct Attribute {
    */
   static const bool has_default_value = false;
 
+  /**
+   * Expose this setting to the users of this Attribute kind.
+   */
+  static const bool context_dependent = context_dep;
+
 private:
 
   /**
@@ -423,8 +447,8 @@ private:
 /**
  * An "attribute type" structure for boolean flags (special).
  */
-template <class T, class CleanupFcn, bool context_dependent>
-struct Attribute<T, bool, CleanupFcn, context_dependent> {
+template <class T, class CleanupFcn, bool context_dep>
+struct Attribute<T, bool, CleanupFcn, context_dep> {
 
   /** The value type for this attribute; here, bool. */
   typedef bool value_type;
@@ -447,6 +471,11 @@ struct Attribute<T, bool, CleanupFcn, context_dependent> {
   static const bool default_value = false;
 
   /**
+   * Expose this setting to the users of this Attribute kind.
+   */
+  static const bool context_dependent = context_dep;
+
+  /**
    * Check that the ID is a valid ID for bool-valued attributes.  Fail
    * an assert if not.  Otherwise return the id.
    */
@@ -463,13 +492,28 @@ private:
   static const uint64_t s_id;
 };
 
-// FIXME make context-dependent
+/**
+ * This is a context-dependent attribute kind (the only difference
+ * between CDAttribute<> and Attribute<> (with the fourth argument
+ * "true") is that you cannot supply a cleanup function (a no-op one
+ * is used).
+ */
 template <class T,
           class value_type>
 struct CDAttribute :
     public Attribute<T, value_type, attr::AttributeCleanupFcn<value_type>, true> {};
 
-// FIXME make context-dependent
+/**
+ * This is a managed attribute kind (the only difference between
+ * ManagedAttribute<> and Attribute<> is the default cleanup function
+ * and the fact that ManagedAttributes cannot be context-dependent).
+ * In the default ManagedAttribute cleanup function, the value is
+ * destroyed with the delete operator.  If the value is allocated with
+ * the array version of new[], an alternate cleanup function should be
+ * provided that uses array delete[].  It is an error to create a
+ * ManagedAttribute<> kind with a non-pointer value_type if you don't
+ * also supply a custom cleanup function.
+ */
 template <class T,
           class value_type,
           class CleanupFcn = attr::ManagedAttributeCleanupFcn<value_type> >
@@ -484,29 +528,29 @@ namespace attr {
  * This is the last-attribute-assigner.  IDs are not globally
  * unique; rather, they are unique for each table_value_type.
  */
-template <class T>
+template <class T, bool context_dep>
 struct LastAttributeId {
   static uint64_t s_id;
 };
 
 /** Initially zero. */
-template <class T>
-uint64_t LastAttributeId<T>::s_id = 0;
+template <class T, bool context_dep>
+uint64_t LastAttributeId<T, context_dep>::s_id = 0;
 
 }/* CVC4::expr::attr namespace */
 
 /** Assign unique IDs to attributes at load time. */
-template <class T, class value_t, class CleanupFcn, bool context_dependent>
-const uint64_t Attribute<T, value_t, CleanupFcn, context_dependent>::s_id =
-  attr::LastAttributeId<typename attr::KindValueToTableValueMapping<value_t>::table_value_type>::s_id++;
+template <class T, class value_t, class CleanupFcn, bool context_dep>
+const uint64_t Attribute<T, value_t, CleanupFcn, context_dep>::s_id =
+  attr::LastAttributeId<typename attr::KindValueToTableValueMapping<value_t>::table_value_type, context_dep>::s_id++;
 
 /**
  * Assign unique IDs to bool-valued attributes at load time, checking
  * that they are in range.
  */
-template <class T, class CleanupFcn, bool context_dependent>
-const uint64_t Attribute<T, bool, CleanupFcn, context_dependent>::s_id =
-  Attribute<T, bool, CleanupFcn, context_dependent>::checkID(attr::LastAttributeId<bool>::s_id++);
+template <class T, class CleanupFcn, bool context_dep>
+const uint64_t Attribute<T, bool, CleanupFcn, context_dep>::s_id =
+  Attribute<T, bool, CleanupFcn, context_dep>::checkID(attr::LastAttributeId<bool, context_dep>::s_id++);
 
 // ATTRIBUTE MANAGER ===========================================================
 
@@ -519,27 +563,44 @@ namespace attr {
 class AttributeManager {
 
   /** Underlying hash table for boolean-valued attributes */
-  AttrHash<bool>        d_bools;
+  AttrHash<bool> d_bools;
   /** Underlying hash table for integral-valued attributes */
-  AttrHash<uint64_t>    d_ints;
+  AttrHash<uint64_t> d_ints;
   /** Underlying hash table for node-valued attributes */
-  AttrHash<TNode>       d_exprs;
+  AttrHash<TNode> d_exprs;
   /** Underlying hash table for string-valued attributes */
   AttrHash<std::string> d_strings;
   /** Underlying hash table for pointer-valued attributes */
-  AttrHash<void*>       d_ptrs;
+  AttrHash<void*> d_ptrs;
+
+  /** Underlying hash table for context-dependent boolean-valued attributes */
+  CDAttrHash<bool> d_cdbools;
+  /** Underlying hash table for context-dependent integral-valued attributes */
+  CDAttrHash<uint64_t> d_cdints;
+  /** Underlying hash table for context-dependent node-valued attributes */
+  CDAttrHash<TNode> d_cdexprs;
+  /** Underlying hash table for context-dependent string-valued attributes */
+  CDAttrHash<std::string> d_cdstrings;
+  /** Underlying hash table for context-dependent pointer-valued attributes */
+  CDAttrHash<void*> d_cdptrs;
 
   /**
    * getTable<> is a helper template that gets the right table from an
    * AttributeManager given its type.
    */
-  template <class T>
+  template <class T, bool context_dep>
   friend struct getTable;
 
 public:
 
   /** Construct an attribute manager. */
-  AttributeManager() {}
+  AttributeManager(context::Context* ctxt) :
+    d_cdbools(ctxt),
+    d_cdints(ctxt),
+    d_cdexprs(ctxt),
+    d_cdstrings(ctxt),
+    d_cdptrs(ctxt) {
+  }
 
   /**
    * Get a particular attribute on a particular node.
@@ -619,12 +680,12 @@ namespace attr {
  * The getTable<> template provides (static) access to the
  * AttributeManager field holding the table.
  */
-template <class T>
+template <class T, bool context_dep>
 struct getTable;
 
 /** Access the "d_bools" member of AttributeManager. */
 template <>
-struct getTable<bool> {
+struct getTable<bool, false> {
   typedef AttrHash<bool> table_type;
   static inline table_type& get(AttributeManager& am) {
     return am.d_bools;
@@ -636,7 +697,7 @@ struct getTable<bool> {
 
 /** Access the "d_ints" member of AttributeManager. */
 template <>
-struct getTable<uint64_t> {
+struct getTable<uint64_t, false> {
   typedef AttrHash<uint64_t> table_type;
   static inline table_type& get(AttributeManager& am) {
     return am.d_ints;
@@ -648,7 +709,7 @@ struct getTable<uint64_t> {
 
 /** Access the "d_exprs" member of AttributeManager. */
 template <>
-struct getTable<Node> {
+struct getTable<Node, false> {
   typedef AttrHash<TNode> table_type;
   static inline table_type& get(AttributeManager& am) {
     return am.d_exprs;
@@ -660,7 +721,7 @@ struct getTable<Node> {
 
 /** Access the "d_strings" member of AttributeManager. */
 template <>
-struct getTable<std::string> {
+struct getTable<std::string, false> {
   typedef AttrHash<std::string> table_type;
   static inline table_type& get(AttributeManager& am) {
     return am.d_strings;
@@ -672,7 +733,7 @@ struct getTable<std::string> {
 
 /** Access the "d_ptrs" member of AttributeManager. */
 template <class T>
-struct getTable<T*> {
+struct getTable<T*, false> {
   typedef AttrHash<void*> table_type;
   static inline table_type& get(AttributeManager& am) {
     return am.d_ptrs;
@@ -684,7 +745,7 @@ struct getTable<T*> {
 
 /** Access the "d_ptrs" member of AttributeManager. */
 template <class T>
-struct getTable<const T*> {
+struct getTable<const T*, false> {
   typedef AttrHash<void*> table_type;
   static inline table_type& get(AttributeManager& am) {
     return am.d_ptrs;
@@ -694,6 +755,78 @@ struct getTable<const T*> {
   }
 };
 
+/** Access the "d_cdbools" member of AttributeManager. */
+template <>
+struct getTable<bool, true> {
+  typedef CDAttrHash<bool> table_type;
+  static inline table_type& get(AttributeManager& am) {
+    return am.d_cdbools;
+  }
+  static inline const table_type& get(const AttributeManager& am) {
+    return am.d_cdbools;
+  }
+};
+
+/** Access the "d_cdints" member of AttributeManager. */
+template <>
+struct getTable<uint64_t, true> {
+  typedef CDAttrHash<uint64_t> table_type;
+  static inline table_type& get(AttributeManager& am) {
+    return am.d_cdints;
+  }
+  static inline const table_type& get(const AttributeManager& am) {
+    return am.d_cdints;
+  }
+};
+
+/** Access the "d_cdexprs" member of AttributeManager. */
+template <>
+struct getTable<Node, true> {
+  typedef CDAttrHash<TNode> table_type;
+  static inline table_type& get(AttributeManager& am) {
+    return am.d_cdexprs;
+  }
+  static inline const table_type& get(const AttributeManager& am) {
+    return am.d_cdexprs;
+  }
+};
+
+/** Access the "d_cdstrings" member of AttributeManager. */
+template <>
+struct getTable<std::string, true> {
+  typedef CDAttrHash<std::string> table_type;
+  static inline table_type& get(AttributeManager& am) {
+    return am.d_cdstrings;
+  }
+  static inline const table_type& get(const AttributeManager& am) {
+    return am.d_cdstrings;
+  }
+};
+
+/** Access the "d_cdptrs" member of AttributeManager. */
+template <class T>
+struct getTable<T*, true> {
+  typedef CDAttrHash<void*> table_type;
+  static inline table_type& get(AttributeManager& am) {
+    return am.d_cdptrs;
+  }
+  static inline const table_type& get(const AttributeManager& am) {
+    return am.d_cdptrs;
+  }
+};
+
+/** Access the "d_cdptrs" member of AttributeManager. */
+template <class T>
+struct getTable<const T*, true> {
+  typedef CDAttrHash<void*> table_type;
+  static inline table_type& get(AttributeManager& am) {
+    return am.d_cdptrs;
+  }
+  static inline const table_type& get(const AttributeManager& am) {
+    return am.d_cdptrs;
+  }
+};
+
 }/* CVC4::expr::attr namespace */
 
 // ATTRIBUTE MANAGER IMPLEMENTATIONS ===========================================
@@ -707,9 +840,9 @@ typename AttrKind::value_type AttributeManager::getAttribute(TNode n,
 
   typedef typename AttrKind::value_type value_type;
   typedef KindValueToTableValueMapping<value_type> mapping;
-  typedef typename getTable<value_type>::table_type table_type;
+  typedef typename getTable<value_type, AttrKind::context_dependent>::table_type table_type;
 
-  const table_type& ah = getTable<value_type>::get(*this);
+  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));
 
   if(i == ah.end()) {
@@ -746,9 +879,9 @@ struct HasAttribute<true, AttrKind> {
                                   typename AttrKind::value_type& ret) {
     typedef typename AttrKind::value_type value_type;
     typedef KindValueToTableValueMapping<value_type> mapping;
-    typedef typename getTable<value_type>::table_type table_type;
+    typedef typename getTable<value_type, AttrKind::context_dependent>::table_type table_type;
 
-    const table_type& ah = getTable<value_type>::get(*am);
+    const table_type& ah = getTable<value_type, AttrKind::context_dependent>::get(*am);
     typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv));
 
     if(i == ah.end()) {
@@ -771,9 +904,9 @@ struct HasAttribute<false, AttrKind> {
                                   NodeValue* nv) {
     typedef typename AttrKind::value_type value_type;
     typedef KindValueToTableValueMapping<value_type> mapping;
-    typedef typename getTable<value_type>::table_type table_type;
+    typedef typename getTable<value_type, AttrKind::context_dependent>::table_type table_type;
 
-    const table_type& ah = getTable<value_type>::get(*am);
+    const table_type& ah = getTable<value_type, AttrKind::context_dependent>::get(*am);
     typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv));
 
     if(i == ah.end()) {
@@ -788,9 +921,9 @@ struct HasAttribute<false, AttrKind> {
                                   typename AttrKind::value_type& ret) {
     typedef typename AttrKind::value_type value_type;
     typedef KindValueToTableValueMapping<value_type> mapping;
-    typedef typename getTable<value_type>::table_type table_type;
+    typedef typename getTable<value_type, AttrKind::context_dependent>::table_type table_type;
 
-    const table_type& ah = getTable<value_type>::get(*am);
+    const table_type& ah = getTable<value_type, AttrKind::context_dependent>::get(*am);
     typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv));
 
     if(i == ah.end()) {
@@ -823,9 +956,9 @@ inline void AttributeManager::setAttribute(TNode n,
 
   typedef typename AttrKind::value_type value_type;
   typedef KindValueToTableValueMapping<value_type> mapping;
-  typedef typename getTable<value_type>::table_type table_type;
+  typedef typename getTable<value_type, AttrKind::context_dependent>::table_type table_type;
 
-  table_type& ah = getTable<value_type>::get(*this);
+  table_type& ah = getTable<value_type, AttrKind::context_dependent>::get(*this);
   ah[std::make_pair(AttrKind::getId(), n.d_nv)] = mapping::convert(value);
 }
 
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 01f7205b2..934c405ad 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -21,7 +21,7 @@ using namespace std;
 namespace CVC4 {
 
 ostream& operator<<(ostream& out, const Command* command) {
-  if (command == NULL) {
+  if(command == NULL) {
     out << "null";
   } else {
     command->toStream(out);
diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index 35bdc947a..b6348394c 100644
--- a/src/expr/expr.cpp
+++ b/src/expr/expr.cpp
@@ -60,7 +60,7 @@ Expr& Expr::operator=(const Expr& e) {
 }
 
 bool Expr::operator==(const Expr& e) const {
-  if(d_exprManager != e.d_exprManager){
+  if(d_exprManager != e.d_exprManager) {
     return false;
   }
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
@@ -75,7 +75,7 @@ bool Expr::operator!=(const Expr& e) const {
 bool Expr::operator<(const Expr& e) const {
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
   Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
-  if(d_exprManager != e.d_exprManager){
+  if(d_exprManager != e.d_exprManager) {
     return false;
   }
   return *d_node < *e.d_node;
@@ -181,11 +181,11 @@ Expr BoolExpr::iteExpr(const Expr& then_e, const Expr& else_e) const {
   return d_exprManager->mkExpr(ITE, *this, then_e, else_e);
 }
 
-void Expr::printAst(std::ostream & o, int indent) const{
+void Expr::printAst(std::ostream & o, int indent) const {
   getNode().printAst(o, indent);
 }
 
-void Expr::debugPrint(){
+void Expr::debugPrint() {
 #ifndef CVC4_MUZZLE
   printAst(Warning());
   Warning().flush();
diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp
index 232a903e9..f0a35e5f1 100644
--- a/src/expr/expr_manager.cpp
+++ b/src/expr/expr_manager.cpp
@@ -25,17 +25,21 @@
 #include "expr/type.h"
 #include "expr/node_manager.h"
 #include "expr/expr_manager.h"
+#include "context/context.h"
 
 using namespace std;
+using namespace CVC4::context;
 
 namespace CVC4 {
 
 ExprManager::ExprManager() :
-  d_nodeManager(new NodeManager()) {
+  d_ctxt(new Context),
+  d_nodeManager(new NodeManager(d_ctxt)) {
 }
 
 ExprManager::~ExprManager() {
   delete d_nodeManager;
+  delete d_ctxt;
 }
 
 const BooleanType* ExprManager::booleanType() const {
@@ -136,4 +140,8 @@ NodeManager* ExprManager::getNodeManager() const {
   return d_nodeManager;
 }
 
-} // End namespace CVC4
+Context* ExprManager::getContext() const {
+  return d_ctxt;
+}
+
+}/* CVC4 namespace */
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
index f5edc5464..ff4e0db6b 100644
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager.h
@@ -30,6 +30,10 @@ class KindType;
 class SmtEngine;
 class NodeManager;
 
+namespace context {
+  class Context;
+}/* CVC4::context namespace */
+
 class CVC4_PUBLIC ExprManager {
 
 public:
@@ -97,7 +101,7 @@ public:
 
   /** Make a function type with input types from argTypes. */
   const FunctionType*
-    mkFunctionType(const std::vector<const Type*>& argTypes, 
+    mkFunctionType(const std::vector<const Type*>& argTypes,
                    const Type* range);
 
   /** Make a new sort with the given name. */
@@ -108,16 +112,28 @@ public:
   Expr mkVar(const Type* type);
 
 private:
+  /** The context */
+  context::Context* d_ctxt;
+
   /** The internal node manager */
   NodeManager* d_nodeManager;
-  
+
   /**
-   * Returns the internal node manager. This should only be used by internal
-   * users, i.e. the friend classes.
+   * Returns the internal node manager.  This should only be used by
+   * internal users, i.e. the friend classes.
    */
   NodeManager* getNodeManager() const;
 
-  /** SmtEngine will use all the internals, so it will grab the node manager */
+  /**
+   * Returns the internal Context.  Used by internal users, i.e. the
+   * friend classes.
+   */
+  context::Context* getContext() const;
+
+  /**
+   * SmtEngine will use all the internals, so it will grab the
+   * NodeManager.
+   */
   friend class SmtEngine;
 
   /** ExprManagerScope reaches in to get the NodeManager */
diff --git a/src/expr/node.h b/src/expr/node.h
index e4e57fc62..f9bbcb5a5 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -37,7 +37,8 @@ namespace CVC4 {
 class Type;
 class NodeManager;
 
-template<bool ref_count> class NodeTemplate;
+template <bool ref_count>
+class NodeTemplate;
 
 /**
  * The Node class encapsulates the NodeValue with reference counting.
@@ -64,7 +65,7 @@ class NodeValue;
  * maintained in the NodeValue if ref_count is true.
  * @param ref_count if true reference are counted in the NodeValue
  */
-template<bool ref_count>
+template <bool ref_count>
 class NodeTemplate {
 
   /**
@@ -94,11 +95,11 @@ class NodeTemplate {
    */
   explicit NodeTemplate(const expr::NodeValue*);
 
-  friend class NodeTemplate<true> ;
-  friend class NodeTemplate<false> ;
+  friend class NodeTemplate<true>;
+  friend class NodeTemplate<false>;
   friend class NodeManager;
 
-  template<unsigned>
+  template <unsigned>
   friend class NodeBuilder;
 
   friend class ::CVC4::expr::attr::AttributeManager;
@@ -152,7 +153,7 @@ public:
    * Destructor. If ref_count is true it will decrement the reference count
    * and, if zero, collect the NodeValue.
    */
-  ~NodeTemplate() throw();
+  ~NodeTemplate() throw(AssertionException);
 
   /**
    * Return the null node.
@@ -389,8 +390,9 @@ private:
    * @param indent the numer of spaces
    */
   static void indent(std::ostream& out, int indent) {
-    for(int i = 0; i < indent; i++)
+    for(int i = 0; i < indent; i++) {
       out << ' ';
+    }
   }
 
 };/* class NodeTemplate */
@@ -422,13 +424,13 @@ struct NodeHashFcn {
   }
 };
 
-template<bool ref_count>
+template <bool ref_count>
 inline size_t NodeTemplate<ref_count>::getNumChildren() const {
   return d_nv->d_nchildren;
 }
 
-template<bool ref_count>
-template<class AttrKind>
+template <bool ref_count>
+template <class AttrKind>
 inline typename AttrKind::value_type NodeTemplate<ref_count>::
 getAttribute(const AttrKind&) const {
   Assert( NodeManager::currentNM() != NULL,
@@ -437,8 +439,8 @@ getAttribute(const AttrKind&) const {
   return NodeManager::currentNM()->getAttribute(*this, AttrKind());
 }
 
-template<bool ref_count>
-template<class AttrKind>
+template <bool ref_count>
+template <class AttrKind>
 inline bool NodeTemplate<ref_count>::
 hasAttribute(const AttrKind&) const {
   Assert( NodeManager::currentNM() != NULL,
@@ -447,18 +449,18 @@ hasAttribute(const AttrKind&) const {
   return NodeManager::currentNM()->hasAttribute(*this, AttrKind());
 }
 
-template<bool ref_count>
-template<class AttrKind>
-inline bool NodeTemplate<ref_count>::
-hasAttribute(const AttrKind&, typename AttrKind::value_type& ret) const {
+template <bool ref_count>
+template <class AttrKind>
+inline bool NodeTemplate<ref_count>::hasAttribute(const AttrKind&,
+                                                  typename AttrKind::value_type& ret) const {
   Assert( NodeManager::currentNM() != NULL,
           "There is no current CVC4::NodeManager associated to this thread.\n"
           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
   return NodeManager::currentNM()->hasAttribute(*this, AttrKind(), ret);
 }
 
-template<bool ref_count>
-template<class AttrKind>
+template <bool ref_count>
+template <class AttrKind>
 inline void NodeTemplate<ref_count>::
 setAttribute(const AttrKind&, const typename AttrKind::value_type& value) {
   Assert( NodeManager::currentNM() != NULL,
@@ -467,12 +469,12 @@ setAttribute(const AttrKind&, const typename AttrKind::value_type& value) {
   NodeManager::currentNM()->setAttribute(*this, AttrKind(), value);
 }
 
-template<bool ref_count>
+template <bool ref_count>
 NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(&expr::NodeValue::s_null);
 
 ////FIXME: This function is a major hack! Should be changed ASAP
 ////TODO: Should use positive definition, i.e. what kinds are atomic.
-template<bool ref_count>
+template <bool ref_count>
 bool NodeTemplate<ref_count>::isAtomic() const {
   using namespace kind;
   switch(getKind()) {
@@ -493,7 +495,7 @@ bool NodeTemplate<ref_count>::isAtomic() const {
 // way?  Nodes conceptually don't change their expr values but of
 // course they do modify the refcount.  But it's nice to be able to
 // support node_iterators over const NodeValue*.  So.... hm.
-template<bool ref_count>
+template <bool ref_count>
 NodeTemplate<ref_count>::NodeTemplate(const expr::NodeValue* ev) :
   d_nv(const_cast<expr::NodeValue*> (ev)) {
   Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
@@ -504,7 +506,7 @@ NodeTemplate<ref_count>::NodeTemplate(const expr::NodeValue* ev) :
 
 // the code for these two "conversion/copy constructors" is identical, but
 // apparently we need both.  see comment in the class.
-template<bool ref_count>
+template <bool ref_count>
 NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate<!ref_count>& e) {
   Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!");
   d_nv = e.d_nv;
@@ -513,7 +515,7 @@ NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate<!ref_count>& e) {
   }
 }
 
-template<bool ref_count>
+template <bool ref_count>
 NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate& e) {
   Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!");
   d_nv = e.d_nv;
@@ -522,17 +524,17 @@ NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate& e) {
   }
 }
 
-template<bool ref_count>
-NodeTemplate<ref_count>::~NodeTemplate() throw() {
-  DtorAssert(d_nv != NULL, "Expecting a non-NULL expression value!");
+template <bool ref_count>
+NodeTemplate<ref_count>::~NodeTemplate() throw(AssertionException) {
+  Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
   if(ref_count) {
     d_nv->dec();
   }
-  DtorAssert(ref_count || d_nv->d_rc > 0,
-             "Temporary node pointing to an expired node");
+  Assert(ref_count || d_nv->d_rc > 0,
+         "Temporary node pointing to an expired node");
 }
 
-template<bool ref_count>
+template <bool ref_count>
 void NodeTemplate<ref_count>::assignNodeValue(expr::NodeValue* ev) {
   d_nv = ev;
   if(ref_count) {
@@ -540,7 +542,7 @@ void NodeTemplate<ref_count>::assignNodeValue(expr::NodeValue* ev) {
   }
 }
 
-template<bool ref_count>
+template <bool ref_count>
 NodeTemplate<ref_count>& NodeTemplate<ref_count>::
 operator=(const NodeTemplate& e) {
   Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
@@ -557,7 +559,7 @@ operator=(const NodeTemplate& e) {
   return *this;
 }
 
-template<bool ref_count>
+template <bool ref_count>
 NodeTemplate<ref_count>& NodeTemplate<ref_count>::
 operator=(const NodeTemplate<!ref_count>& e) {
   Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
@@ -574,54 +576,55 @@ operator=(const NodeTemplate<!ref_count>& e) {
   return *this;
 }
 
-template<bool ref_count>
-NodeTemplate<true> NodeTemplate<ref_count>::eqNode(const NodeTemplate<
-                                                   ref_count>& right) const {
+template <bool ref_count>
+NodeTemplate<true>
+NodeTemplate<ref_count>::eqNode(const NodeTemplate<ref_count>& right) const {
   return NodeManager::currentNM()->mkNode(kind::EQUAL, *this, right);
 }
 
-template<bool ref_count>
+template <bool ref_count>
 NodeTemplate<true> NodeTemplate<ref_count>::notNode() const {
   return NodeManager::currentNM()->mkNode(kind::NOT, *this);
 }
 
-template<bool ref_count>
-NodeTemplate<true> NodeTemplate<ref_count>::andNode(const NodeTemplate<
-                                                    ref_count>& right) const {
+template <bool ref_count>
+NodeTemplate<true>
+NodeTemplate<ref_count>::andNode(const NodeTemplate<ref_count>& right) const {
   return NodeManager::currentNM()->mkNode(kind::AND, *this, right);
 }
 
-template<bool ref_count>
-NodeTemplate<true> NodeTemplate<ref_count>::orNode(const NodeTemplate<
-                                                   ref_count>& right) const {
+template <bool ref_count>
+NodeTemplate<true>
+NodeTemplate<ref_count>::orNode(const NodeTemplate<ref_count>& right) const {
   return NodeManager::currentNM()->mkNode(kind::OR, *this, right);
 }
 
-template<bool ref_count>
-NodeTemplate<true> NodeTemplate<ref_count>::iteNode(const NodeTemplate<
-                                                    ref_count>& thenpart, const NodeTemplate<ref_count>& elsepart) const {
+template <bool ref_count>
+NodeTemplate<true>
+NodeTemplate<ref_count>::iteNode(const NodeTemplate<ref_count>& thenpart,
+                                 const NodeTemplate<ref_count>& elsepart) const {
   return NodeManager::currentNM()->mkNode(kind::ITE, *this, thenpart, elsepart);
 }
 
-template<bool ref_count>
-NodeTemplate<true> NodeTemplate<ref_count>::iffNode(const NodeTemplate<
-                                                    ref_count>& right) const {
+template <bool ref_count>
+NodeTemplate<true>
+NodeTemplate<ref_count>::iffNode(const NodeTemplate<ref_count>& right) const {
   return NodeManager::currentNM()->mkNode(kind::IFF, *this, right);
 }
 
-template<bool ref_count>
-NodeTemplate<true> NodeTemplate<ref_count>::impNode(const NodeTemplate<
-                                                    ref_count>& right) const {
+template <bool ref_count>
+NodeTemplate<true>
+NodeTemplate<ref_count>::impNode(const NodeTemplate<ref_count>& right) const {
   return NodeManager::currentNM()->mkNode(kind::IMPLIES, *this, right);
 }
 
-template<bool ref_count>
-NodeTemplate<true> NodeTemplate<ref_count>::xorNode(const NodeTemplate<
-                                                    ref_count>& right) const {
+template <bool ref_count>
+NodeTemplate<true>
+NodeTemplate<ref_count>::xorNode(const NodeTemplate<ref_count>& right) const {
   return NodeManager::currentNM()->mkNode(kind::XOR, *this, right);
 }
 
-template<bool ref_count>
+template <bool ref_count>
 void NodeTemplate<ref_count>::printAst(std::ostream& out, int ind) const {
   indent(out, ind);
   out << '(';
@@ -681,7 +684,8 @@ NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const {
 }
 
 /**
- * Returns true if the node has an operator (i.e., it's not a variable or a constant).
+ * Returns true if the node has an operator (i.e., it's not a variable
+ * or a constant).
  */
 template <bool ref_count>
 bool NodeTemplate<ref_count>::hasOperator() const {
@@ -710,7 +714,7 @@ bool NodeTemplate<ref_count>::hasOperator() const {
   }
 }
 
-template<bool ref_count>
+template <bool ref_count>
 const Type* NodeTemplate<ref_count>::getType() const {
   Assert( NodeManager::currentNM() != NULL,
           "There is no current CVC4::NodeManager associated to this thread.\n"
@@ -718,6 +722,7 @@ const Type* NodeTemplate<ref_count>::getType() const {
   return NodeManager::currentNM()->getType(*this);
 }
 
+#ifdef CVC4_DEBUG
 /**
  * Pretty printer for use within gdb.  This is not intended to be used
  * outside of gdb.  This writes to the Warning() stream and immediately
@@ -725,7 +730,9 @@ const Type* NodeTemplate<ref_count>::getType() const {
  *
  * Note that this function cannot be a template, since the compiler
  * won't instantiate it.  Even if we explicitly instantiate.  (Odd?)
- * So we implement twice.
+ * So we implement twice.  We mark as __attribute__((used)) so that
+ * GCC emits code for it even though static analysis indicates it's
+ * never called.
  *
  * Tim's Note: I moved this into the node.h file because this allows gdb
  * to find the symbol, and use it, which is the first standard this code needs
@@ -740,6 +747,7 @@ static void __attribute__((used)) debugPrintTNode(const NodeTemplate<false>& n)
   n.printAst(Warning(), 0);
   Warning().flush();
 }
+#endif /* CVC4_DEBUG */
 
 }/* CVC4 namespace */
 
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 4dc3c06d0..42ca9db2b 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -47,7 +47,6 @@ inline std::ostream& operator<<(std::ostream&, const NodeBuilder<nchild_thresh>&
 class AndNodeBuilder;
 class OrNodeBuilder;
 class PlusNodeBuilder;
-class MinusNodeBuilder;
 class MultNodeBuilder;
 
 template <unsigned nchild_thresh>
@@ -63,7 +62,7 @@ class NodeBuilder {
   // extract another
   bool d_used;
 
-  expr::NodeValue *d_nv;
+  expr::NodeValue* d_nv;
   expr::NodeValue d_inlineNv;
   expr::NodeValue *d_childrenStorage[nchild_thresh];
 
@@ -93,7 +92,7 @@ class NodeBuilder {
   }
 
   // dealloc: only call this with d_used == false and nvIsAllocated()
-  inline void dealloc() throw();
+  inline void dealloc();
 
   void crop() {
     Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
@@ -101,6 +100,9 @@ class NodeBuilder {
       d_nv = (expr::NodeValue*)
         std::realloc(d_nv, sizeof(expr::NodeValue) +
                      ( sizeof(expr::NodeValue*) * (d_size = d_nv->d_nchildren) ));
+      if(d_nv == NULL) {
+        throw std::bad_alloc();
+      }
     }
   }
 
@@ -126,7 +128,7 @@ public:
   template <unsigned N> inline NodeBuilder(const NodeBuilder<N>& nb);
   inline NodeBuilder(NodeManager* nm);
   inline NodeBuilder(NodeManager* nm, Kind k);
-  inline ~NodeBuilder() throw();
+  inline ~NodeBuilder();
 
   typedef expr::NodeValue::iterator<true> iterator;
   typedef expr::NodeValue::iterator<true> const_iterator;
@@ -223,9 +225,10 @@ public:
   friend class PlusNodeBuilder;
   friend class MultNodeBuilder;
 
-  //Yet 1 more example of how terrifying C++ is as a language
-  //This is needed for copy constructors of different sizes to access private fields
-  template <unsigned N> friend class NodeBuilder;
+  // Yet 1 more example of how terrifying C++ is as a language
+  // This is needed for copy constructors of different sizes to access private fields
+  template <unsigned N>
+  friend class NodeBuilder;
 
 };/* class NodeBuilder */
 
@@ -423,14 +426,24 @@ inline MultNodeBuilder PlusNodeBuilder::operator*(const NodeTemplate<rc>& n) {
   return MultNodeBuilder(Node(d_eb), n);
 }
 
-/*
-inline PlusNodeBuilder& PlusNodeBuilder::operator+(PlusNodeBuilder& b) { return *this + Node(d_eb); }
-inline PlusNodeBuilder& PlusNodeBuilder::operator+(MultNodeBuilder& b) { return *this + Node(d_eb); }
-inline PlusNodeBuilder& PlusNodeBuilder::operator-(PlusNodeBuilder& b) { return *this - Node(d_eb); }
-inline PlusNodeBuilder& PlusNodeBuilder::operator-(MultNodeBuilder& b) { return *this - Node(d_eb); }
-inline MultNodeBuilder PlusNodeBuilder::operator*(PlusNodeBuilder& b) { return *this * Node(d_eb); }
-inline MultNodeBuilder PlusNodeBuilder::operator*(MultNodeBuilder& b) { return *this * Node(d_eb); }
-*/
+inline PlusNodeBuilder& operator+(PlusNodeBuilder& a, const PlusNodeBuilder& b) {
+  return a + Node(b.d_eb);
+}
+inline PlusNodeBuilder& operator+(PlusNodeBuilder& a, const MultNodeBuilder& b) {
+  return a + Node(b.d_eb);
+}
+inline PlusNodeBuilder& operator-(PlusNodeBuilder&a, const PlusNodeBuilder& b) {
+  return a - Node(b.d_eb);
+}
+inline PlusNodeBuilder& operator-(PlusNodeBuilder& a, const MultNodeBuilder& b) {
+  return a - Node(b.d_eb);
+}
+inline MultNodeBuilder operator*(PlusNodeBuilder& a, const PlusNodeBuilder& b) {
+  return a * Node(b.d_eb);
+}
+inline MultNodeBuilder operator*(PlusNodeBuilder& a, const MultNodeBuilder& b) {
+  return a * Node(b.d_eb);
+}
 
 template <bool rc>
 inline PlusNodeBuilder MultNodeBuilder::operator+(const NodeTemplate<rc>& n) {
@@ -439,7 +452,7 @@ inline PlusNodeBuilder MultNodeBuilder::operator+(const NodeTemplate<rc>& n) {
 
 template <bool rc>
 inline PlusNodeBuilder MultNodeBuilder::operator-(const NodeTemplate<rc>& n) {
-  return PlusNodeBuilder(Node(d_eb), n);
+  return PlusNodeBuilder(Node(d_eb), NodeManager::currentNM()->mkNode(kind::UMINUS, n));
 }
 
 template <bool rc>
@@ -448,14 +461,24 @@ inline MultNodeBuilder& MultNodeBuilder::operator*(const NodeTemplate<rc>& n) {
   return *this;
 }
 
-/*
-inline PlusNodeBuilder MultNodeBuilder::operator+(const PlusNodeBuilder& b) { return *this + Node(d_eb); }
-inline PlusNodeBuilder MultNodeBuilder::operator+(const MultNodeBuilder& b) { return *this + Node(d_eb); }
-inline PlusNodeBuilder MultNodeBuilder::operator-(const PlusNodeBuilder& b) { return *this - Node(d_eb); }
-inline PlusNodeBuilder MultNodeBuilder::operator-(const MultNodeBuilder& b) { return *this - Node(d_eb); }
-inline MultNodeBuilder& MultNodeBuilder::operator*(const PlusNodeBuilder& b) { return *this * Node(d_eb); }
-inline MultNodeBuilder& MultNodeBuilder::operator*(const MultNodeBuilder& b) { return *this * Node(d_eb); }
-*/
+inline PlusNodeBuilder operator+(MultNodeBuilder& a, const PlusNodeBuilder& b) {
+  return a + Node(b.d_eb);
+}
+inline PlusNodeBuilder operator+(MultNodeBuilder& a, const MultNodeBuilder& b) {
+  return a + Node(b.d_eb);
+}
+inline PlusNodeBuilder operator-(MultNodeBuilder& a, const PlusNodeBuilder& b) {
+  return a - Node(b.d_eb);
+}
+inline PlusNodeBuilder operator-(MultNodeBuilder& a, const MultNodeBuilder& b) {
+  return a - Node(b.d_eb);
+}
+inline MultNodeBuilder& operator*(MultNodeBuilder& a, const PlusNodeBuilder& b) {
+  return a * Node(b.d_eb);
+}
+inline MultNodeBuilder& operator*(MultNodeBuilder& a, const MultNodeBuilder& b) {
+  return a * Node(b.d_eb);
+}
 
 template <bool rc1, bool rc2>
 inline AndNodeBuilder operator&&(const NodeTemplate<rc1>& a, const NodeTemplate<rc2>& b) {
@@ -502,6 +525,41 @@ inline OrNodeBuilder operator||(const NodeTemplate<rc>& a, const OrNodeBuilder&
   return a || Node(b.d_eb);
 }
 
+template <bool rc>
+inline PlusNodeBuilder operator+(const NodeTemplate<rc>& a, const PlusNodeBuilder& b) {
+  return a + Node(b.d_eb);
+}
+
+template <bool rc>
+inline PlusNodeBuilder operator+(const NodeTemplate<rc>& a, const MultNodeBuilder& b) {
+  return a + Node(b.d_eb);
+}
+
+template <bool rc>
+inline PlusNodeBuilder operator-(const NodeTemplate<rc>& a, const PlusNodeBuilder& b) {
+  return a - Node(b.d_eb);
+}
+
+template <bool rc>
+inline PlusNodeBuilder operator-(const NodeTemplate<rc>& a, const MultNodeBuilder& b) {
+  return a - Node(b.d_eb);
+}
+
+template <bool rc>
+inline MultNodeBuilder operator*(const NodeTemplate<rc>& a, const PlusNodeBuilder& b) {
+  return a * Node(b.d_eb);
+}
+
+template <bool rc>
+inline MultNodeBuilder operator*(const NodeTemplate<rc>& a, const MultNodeBuilder& b) {
+  return a * Node(b.d_eb);
+}
+
+template <bool rc>
+inline NodeTemplate<true> operator-(const NodeTemplate<rc>& a) {
+  return NodeManager::currentNM()->mkNode(kind::UMINUS, a);
+}
+
 }/* CVC4 namespace */
 
 #include "expr/node.h"
@@ -611,7 +669,7 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm, Kind k) :
 }
 
 template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>::~NodeBuilder() throw() {
+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
@@ -642,9 +700,15 @@ void NodeBuilder<nchild_thresh>::realloc() {
     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;
@@ -663,10 +727,16 @@ void NodeBuilder<nchild_thresh>::realloc(size_t toSize, bool copy) {
     d_nv = (expr::NodeValue*)
       std::realloc(d_nv, sizeof(expr::NodeValue) +
                    ( sizeof(expr::NodeValue*) * (d_size = toSize) ));
+    if(d_nv == NULL) {
+      throw std::bad_alloc();
+    }
   } else {
     d_nv = (expr::NodeValue*)
       std::malloc(sizeof(expr::NodeValue) +
                   ( sizeof(expr::NodeValue*) * (d_size = toSize) ));
+    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;
@@ -682,12 +752,11 @@ void NodeBuilder<nchild_thresh>::realloc(size_t toSize, bool copy) {
 }
 
 template <unsigned nchild_thresh>
-inline void NodeBuilder<nchild_thresh>::dealloc() throw() {
+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 */
-  DtorAssert(!d_used,
-             "Internal error: NodeBuilder: dealloc() called with d_used");
+  Assert(!d_used, "Internal error: NodeBuilder: dealloc() called with d_used");
 
   for(expr::NodeValue::nv_iterator i = d_nv->nv_begin();
       i != d_nv->nv_end();
@@ -707,9 +776,12 @@ NodeBuilder<nchild_thresh>::operator Node() const {// const version
 
   if(d_nv->d_kind == kind::VARIABLE) {
     Assert(d_nv->d_nchildren == 0);
-    expr::NodeValue *nv = (expr::NodeValue*)
+    expr::NodeValue* nv = (expr::NodeValue*)
       std::malloc(sizeof(expr::NodeValue) +
                   (sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));// FIXME :: WTF??
+    if(nv == NULL) {
+      throw std::bad_alloc();
+    }
     nv->d_nchildren = 0;
     nv->d_kind = kind::VARIABLE;
     nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
@@ -736,6 +808,9 @@ NodeBuilder<nchild_thresh>::operator Node() const {// const version
     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;
@@ -767,6 +842,9 @@ NodeBuilder<nchild_thresh>::operator Node() const {// const version
   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
@@ -797,9 +875,12 @@ NodeBuilder<nchild_thresh>::operator Node() {// not const
 
   if(d_nv->d_kind == kind::VARIABLE) {
     Assert(d_nv->d_nchildren == 0);
-    expr::NodeValue *nv = (expr::NodeValue*)
+    expr::NodeValue* nv = (expr::NodeValue*)
       std::malloc(sizeof(expr::NodeValue) +
                   (sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));// FIXME :: WTF??
+    if(nv == NULL) {
+      throw std::bad_alloc();
+    }
     nv->d_nchildren = 0;
     nv->d_kind = kind::VARIABLE;
     nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
@@ -847,6 +928,9 @@ NodeBuilder<nchild_thresh>::operator Node() {// not const
   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
@@ -866,7 +950,6 @@ NodeBuilder<nchild_thresh>::operator Node() {// not const
 template <unsigned nchild_thresh>
 inline std::ostream& operator<<(std::ostream& out,
                                 const NodeBuilder<nchild_thresh>& b) {
-
   b.toStream(out);
   return out;
 }
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 62bcc7516..c4f54727a 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 "context/context.h"
 
 namespace CVC4 {
 
@@ -51,7 +52,8 @@ class NodeManager {
 
   template <unsigned> friend class CVC4::NodeBuilder;
 
-  typedef __gnu_cxx::hash_set<expr::NodeValue*, expr::NodeValueHashFcn,
+  typedef __gnu_cxx::hash_set<expr::NodeValue*,
+                              expr::NodeValueInternalHashFcn,
                               expr::NodeValue::NodeValueEq> NodeValueSet;
   NodeValueSet d_nodeValueSet;
 
@@ -61,10 +63,18 @@ class NodeManager {
   void poolInsert(expr::NodeValue* nv);
 
   friend class NodeManagerScope;
+  friend class expr::NodeValue;
+
+  std::vector<expr::NodeValue*> d_zombieList;
+
+  inline void gc(expr::NodeValue* nv) {
+    Assert(nv->d_rc == 0);
+    d_zombieList.push_back(nv);
+  }
 
 public:
 
-  NodeManager() {
+  NodeManager(context::Context* ctxt) : d_attrManager(ctxt) {
     poolInsert( &expr::NodeValue::s_null );
   }
 
@@ -133,6 +143,26 @@ public:
   inline const Type* getType(TNode n);
 };
 
+/**
+ * Resource-acquisition-is-instantiation C++ idiom: create one of
+ * these "scope" objects to temporarily change the thread-specific
+ * notion of the "current" NodeManager for Node creation/deletion,
+ * etc.  On destruction, the previous NodeManager pointer is restored.
+ * Therefore such objects should only be created and destroyed in a
+ * well-scoped manner (such as on the stack).
+ *
+ * This is especially useful on public-interface calls into the CVC4
+ * library, where CVC4's notion of the "current" NodeManager should be
+ * set to match the calling context.  See, for example, the
+ * implementations of public calls in the ExprManager and SmtEngine
+ * classes.
+ *
+ * You may create a NodeManagerScope with "new" and destroy it with
+ * "delete", or place it as a data member of an object that is, but if
+ * the scope of these new/delete pairs isn't properly maintained, the
+ * incorrect "current" NodeManager pointer may be restored after a
+ * delete.
+ */
 class NodeManagerScope {
   NodeManager *d_oldNodeManager;
 
@@ -143,22 +173,32 @@ public:
     Debug("current") << "node manager scope: " << NodeManager::s_current << "\n";
   }
 
-  ~NodeManagerScope() throw() {
+  ~NodeManagerScope() {
     NodeManager::s_current = d_oldNodeManager;
     Debug("current") << "node manager scope: returning to " << NodeManager::s_current << "\n";
   }
 };
 
 /**
- * A wrapper (essentially) for NodeManagerScope.  Without this, we'd
- * need Expr to be a friend of ExprManager.
+ * A wrapper (essentially) for NodeManagerScope.  The current
+ * "NodeManager" pointer is set to this Expr's underlying
+ * ExpressionManager's NodeManager.  When the ExprManagerScope is
+ * destroyed, the previous NodeManager is restored.
+ *
+ * This is especially useful on public-interface calls into the CVC4
+ * library, where CVC4's notion of the "current" NodeManager should be
+ * set to match the calling context.  See, for example, the
+ * implementations of public calls in the Expr class.
+ *
+ * Without this, we'd need Expr to be a friend of ExprManager.
  */
 class ExprManagerScope {
   NodeManagerScope d_nms;
 public:
   inline ExprManagerScope(const Expr& e) :
-    d_nms(e.getExprManager() == NULL ?
-          NodeManager::currentNM() : e.getExprManager()->getNodeManager()) {
+    d_nms(e.getExprManager() == NULL
+          ? NodeManager::currentNM()
+          : e.getExprManager()->getNodeManager()) {
   }
 };
 
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 523c5387b..bd74fd4d4 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -24,7 +24,7 @@
 
 #include "cvc4_config.h"
 #include <stdint.h>
-#include "kind.h"
+#include "expr/kind.h"
 
 #include <string>
 #include <iterator>
@@ -98,7 +98,7 @@ class NodeValue {
   NodeValue(int);
 
   /** Destructor decrements the ref counts of its children */
-  ~NodeValue() throw();
+  ~NodeValue();
 
   typedef NodeValue** nv_iterator;
   typedef NodeValue const* const* const_nv_iterator;
@@ -150,16 +150,19 @@ public:
   }
 
   /**
-   * Hash this expression.
+   * Hash this NodeValue.  For hash_maps, hash_sets, etc.. but this is
+   * for expr package internal use only at present!  This is likely to
+   * be POORLY PERFORMING for other uses!  For example, this gives
+   * collisions for all VARIABLEs.
    * @return the hash value of this expression.
    */
-  size_t hash() const {
+  size_t internalHash() const {
     size_t hash = d_kind;
     const_nv_iterator i = nv_begin();
     const_nv_iterator i_end = nv_end();
-    while (i != i_end) {
+    while(i != i_end) {
       hash ^= (*i)->d_id + 0x9e3779b9 + (hash << 6) + (hash >> 2);
-      ++ i;
+      ++i;
     }
     return hash;
   }
@@ -209,7 +212,27 @@ public:
   static inline Kind dKindToKind(unsigned d) {
     return (d == kindMask) ? kind::UNDEFINED_KIND : Kind(d);
   }
-};
+};/* class NodeValue */
+
+/**
+ * For hash_maps, hash_sets, etc.. but this is for expr package
+ * internal use only at present!  This is likely to be POORLY
+ * PERFORMING for other uses!  NodeValue::internalHash() will lead to
+ * collisions for all VARIABLEs.
+ */
+struct NodeValueInternalHashFcn {
+  inline size_t operator()(const NodeValue* nv) const {
+    return (size_t) nv->internalHash();
+  }
+};/* struct NodeValueHashFcn */
+
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
+
+#include "node_manager.h"
+
+namespace CVC4 {
+namespace expr {
 
 inline NodeValue::NodeValue() :
   d_id(0),
@@ -225,7 +248,7 @@ inline NodeValue::NodeValue(int) :
   d_nchildren(0) {
 }
 
-inline NodeValue::~NodeValue() throw() {
+inline NodeValue::~NodeValue() {
   for(nv_iterator i = nv_begin(); i != nv_end(); ++i) {
     (*i)->dec();
   }
@@ -243,7 +266,10 @@ inline void NodeValue::dec() {
   if(EXPECT_TRUE( d_rc < MAX_RC )) {
     --d_rc;
     if(EXPECT_FALSE( d_rc == 0 )) {
-      // FIXME gc
+      Assert(NodeManager::currentNM() != NULL,
+             "No current NodeManager on destruction of NodeValue: "
+             "maybe a public CVC4 interface function is missing a NodeManagerScope ?");
+      NodeManager::currentNM()->gc(this);
     }
   }
 }
@@ -264,13 +290,6 @@ inline NodeValue::const_nv_iterator NodeValue::nv_end() const {
   return d_children + d_nchildren;
 }
 
-// for hash_maps, hash_sets, ...
-struct NodeValueHashFcn {
-  size_t operator()(const CVC4::expr::NodeValue* nv) const {
-    return (size_t)nv->hash();
-  }
-};/* struct NodeValueHashFcn */
-
 }/* CVC4::expr namespace */
 }/* CVC4 namespace */