* 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

50 files changed, 2147 insertions, 1018 deletions

diff --git a/COPYING b/COPYING
index 551f7fa37..3161a4784 100644
--- a/COPYING
+++ b/COPYING
@@ -1,13 +1,24 @@
-CVC4 is copyright (C) 2009 the ACSys research group at the Courant
+CVC4 is copyright (C) 2009, 2010 the ACSys research group at the Courant
 Institute for Mathematical Sciences, New York University.
 All rights reserved.
 
 This is a prerelease version; distribution is restricted.
 
--- Morgan Deters <mdeters@cs.nyu.edu>  Mon, 02 Nov 2009 17:54:27 -0500
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS ''AS IS'' AND ANY
+EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY
+DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
+ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+-- Morgan Deters <mdeters@cs.nyu.edu>  Thu, 04 Mar 2010 20:46:40 -0500
 
 CVC4 incorporates MiniSat code, excluded from the above copyright.
-See src/sat/minisat.
+See src/sat/minisat.  Its copyright:
 
   MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
 
@@ -30,3 +41,43 @@ See src/sat/minisat.
   OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
   WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 
+CVC4 incorporates the script "autogen.sh", excluded from the above copyright.
+See autogen.sh.  Its copyright:
+
+  Copyright (c) 2005-2009 United States Government as represented by
+  the U.S. Army Research Laboratory.
+ 
+  Redistribution and use in source and binary forms, with or without
+  modification, are permitted provided that the following conditions
+  are met:
+ 
+  1. Redistributions of source code must retain the above copyright
+  notice, this list of conditions and the following disclaimer.
+ 
+  2. Redistributions in binary form must reproduce the above
+  copyright notice, this list of conditions and the following
+  disclaimer in the documentation and/or other materials provided
+  with the distribution.
+ 
+  3. The name of the author may not be used to endorse or promote
+  products derived from this software without specific prior written
+  permission.
+ 
+  THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS
+  OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+  WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+  ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
+  DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+  DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE
+  GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+  INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
+  WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+  NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+  SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+CVC4 incorporates the script "doxygen.am", excluded from the above copyright.
+See config/doxygen.am.  Its copyright:
+
+  Copyright (C) 2004 Oren Ben-Kiki
+  This file is distributed under the same terms as the Automake macro files.
+
diff --git a/DESIGN_QUESTIONS b/DESIGN_QUESTIONS
deleted file mode 100644
index 0e8f50245..000000000
--- a/DESIGN_QUESTIONS
+++ /dev/null
@@ -1,82 +0,0 @@
-vc.h
-
-/* TODO provide way of querying whether you fall into a fragment /
- * returning what fragment you're in */
-
-decision_engine.h
-
-  // TODO: design decision: decision engine should be notified of
-  // propagated lits, and also why(?) (so that it can make decisions
-  // based on the utility of various theories and various theory
-  // literals).  How?  Maybe TheoryEngine has a backdoor into
-  // DecisionEngine "behind the back" of the PropEngine?
-
-result.h
-
-// TODO: perhaps best to templatize Result on its Kind (SAT/Validity),
-// but this requires doing the same for Prover and needs discussion.
-
-// TODO: subclass to provide models, etc.  This is really just
-// intended as a three-valued response code.
-
-expr_builder.h
-
-  // TODO: store some flags here and install into attribute map when
-  // the expr is created?  (we'd have to do that since we don't know
-  // it's hash code yet)
-
-expr_builder.h
-
-  /* TODO design: these modify ExprBuilder */
-  ExprBuilder& operator!() { return notExpr(); }
-  ExprBuilder& operator&&(const Expr& right) { return andExpr(right); }
-  ExprBuilder& operator||(const Expr& right) { return orExpr(right);  }
-
-prover.h
-
-// TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
-// hood): use a type parameter and have check() delegate, or subclass
-// Prover and override check()?
-//
-// Probably better than that is to have a configuration object that
-// indicates which passes are desired.  The configuration occurs
-// elsewhere (and can even occur at runtime).  A simple "pass manager"
-// of sorts determines check()'s behavior.
-//
-// The CNF conversion can go on in PropEngine.
-
-prover.h
-
-  /** (preprocessing)
-   * Pre-process an Expr.  This is expected to be highly-variable,
-   * with a lot of "source-level configurability" to add multiple
-   * passes over the Expr.  TODO: may need to specify a LEVEL of
-   * preprocessing (certain contexts need more/less ?).
-   */
-
-theory.h
-
-  // TODO: these use the current EM (but must be renamed)
-
-  // TODO design decision: instead of returning a set of literals
-  // here, perhaps we have an interface back into the prop engine
-  // where we assert directly.  we might sometimes unknowingly assert
-  // something clearly inconsistent (esp. in a parallel context).
-  // This would allow the PropEngine to cancel our further work since
-  // we're already inconsistent---also could strategize dynamically on
-  // whether enough theory prop work has occurred.
-  virtual void propagate(Effort level = FULL_EFFORT) = 0;
-
-  could provide a continuation (essentially) to propagate literals.
-  argument Propagator prop
-  class Propagator {
-    PropEngine d_pe;
-  public:
-    // may not return due to a longjmp (?) or perhaps an exception
-    // returns next continuation
-    Propagator operator()(Literal l);
-  };
-
-
-==========================
-TODO:  add throw() specifications
diff --git a/config/cvc4.m4 b/config/cvc4.m4
index 1cde462b5..8106f1383 100644
--- a/config/cvc4.m4
+++ b/config/cvc4.m4
@@ -18,10 +18,25 @@ for ac_option
 do
   case $ac_option in
     -*|*=*) ;;
-    production|debug|default|competition)
-       ac_cvc4_build_profile_set=yes
-       AC_MSG_NOTICE([CVC4: building profile $ac_option])
-       ac_option="--with-build=$ac_option" ;;
+    production|production-*|debug|debug-*|default|default-*|competition|competition-*)
+      ac_option_build=`expr "$ac_option" : '\([[^-]]*\)-\?'`
+      ac_cvc4_build_profile_set=yes
+      AC_MSG_NOTICE([CVC4: building profile $ac_option_build])
+      for x in optimized assertions tracing muzzle coverage profiling; do
+        if expr "$ac_option" : '.*-no'$x'-\|.*-no'$x'$' >/dev/null; then
+          eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--disable-$x\""'
+        fi
+        if expr "$ac_option" : '.*-'$x'-\|.*-'$x'$' >/dev/null; then
+          eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--enable-$x\""'
+        fi
+      done
+      if expr "$ac_option" : '.*-nodebugsymbols-\|.*-nodebugsymbols$' >/dev/null; then
+        eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--disable-debug-symbols\""'
+      fi
+      if expr "$ac_option" : '.*-debugsymbols-\|.*-debugsymbols$' >/dev/null; then
+        eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--enable-debug-symbols\""'
+      fi
+      ac_option="--with-build=$ac_option_build"
   esac
   eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"$ac_option\""'
 done
diff --git a/configure.ac b/configure.ac
index d75ce6309..0e08a0752 100644
--- a/configure.ac
+++ b/configure.ac
@@ -166,7 +166,7 @@ case "$with_build" in
     if test -z "${enable_tracing+set}"   ; then enable_tracing=no                ; fi
     if test -z "${enable_muzzle+set}"    ; then enable_muzzle=no                 ; fi
     ;;
-  debug) # Unoptimized, debug symbols, assertions, tracing
+  debug) # unoptimized, debug symbols, assertions, tracing
     CVC4CPPFLAGS=-DCVC4_DEBUG
     CVC4CXXFLAGS='-O0 -fno-inline -ggdb3'
     CVC4LDFLAGS=
@@ -299,6 +299,7 @@ fi
 AC_MSG_RESULT([$enable_coverage])
 
 if test "$enable_coverage" = yes; then
+  CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_COVERAGE"
   CVC4CXXFLAGS="$CVC4CXXFLAGS --coverage"
   CVC4LDFLAGS="$CVC4LDFLAGS --coverage"
 fi
@@ -316,6 +317,7 @@ fi
 AC_MSG_RESULT([$enable_profiling])
 
 if test "$enable_profiling" = yes; then
+  CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_PROFILING"
   CVC4CXXFLAGS="$CVC4CXXFLAGS -pg"
   CVC4LDFLAGS="$CVC4LDFLAGS -pg"
 fi
diff --git a/contrib/code-checker b/contrib/code-checker
new file mode 100755
index 000000000..a40dc61af
--- /dev/null
+++ b/contrib/code-checker
@@ -0,0 +1,96 @@
+#!/usr/bin/perl -w
+
+use strict;
+
+while($#ARGV >= 0) {
+  my %FP;
+  my $file = shift @ARGV;
+
+  local $/ = undef;
+
+  open(FP, $file) || die "can't read $file";
+  print "checking $file...\n";
+  binmode FP;
+  my $buf = <FP>;
+  close FP;
+
+  print "file named incorrectly; use *.h: $file\n" if $file =~ /\.(hpp|H|hh)$/;
+  print "file named incorrectly; use *.cpp: $file\n" if $file =~ /\.(C|cc)$/;
+  if($file =~ /\.(h|hpp|H)$/) {
+    check_as_header($buf);
+  } elsif($file =~ /\.(h|cpp|C)$/) {
+    check_as_source($buf);
+  } else {
+    die "$file not checked (unknown type of file)";
+  }
+  open(FP, "cpp -nostdinc \"$file\" 2>/dev/null |") || die "can't cpp $file";
+  binmode FP;
+  $buf = <FP>;
+  close FP;
+
+  if($file =~ /\.(h|hpp|H)$/) {
+    check_as_header_cpp($buf);
+  } elsif($file =~ /\.(h|cpp|C)$/) {
+    check_as_source_cpp($buf);
+  } else {
+    die "$file not checked (unknown type of file)";
+  }
+}
+
+sub check_as_any {
+  my($buf) = @_;
+
+  print "no file head comment\n" unless $buf =~ m,^/*\*\*\*,;
+}
+
+sub check_as_header {
+  my($buf) = @_;
+  check_as_any($buf);
+}
+
+sub check_as_source {
+  my($buf) = @_;
+  check_as_any($buf);
+}
+
+sub check_as_any_cpp {
+  my($buf) = @_;
+
+  print "need space between tokens ) and {\n" if $buf =~ /\)\{/;
+  print "need space between tokens 'const' and {\n" if $buf =~ /\bconst\{/;
+  print "need space between tokens ) and 'const'\n" if $buf =~ /\)const\b/;
+  print "need space between tokens 'template' and <\n" if $buf =~ /\btemplate</;
+  print "need space between tokens } and 'else'\n" if $buf =~ /\}else\b/;
+  print "need space between tokens 'else' and {\n" if $buf =~ /\belse\{/;
+  print "need space between tokens 'do' and {\n" if $buf =~ /\bdo\{/;
+  print "need space between tokens } and 'while'\n" if $buf =~ /\}while\b/;
+
+  print "no space permitted before ;\n" if $buf =~ /\s+;/;
+  print "no space permitted between tokens 'if' and (\n" if $buf =~ /\bif\s\(/;
+  print "no space permitted between tokens 'while' and (\n" if $buf =~ /\bwhile\s\(/;
+  print "no space permitted between tokens 'for' and (\n" if $buf =~ /\bfor\s\(/;
+
+  my $code = $buf;
+  $code =~ s,\\.,.,g;
+  $code =~ s,"[^"]*","",g;
+
+  #print "'if' blocks must be braced, '{' should be last character on block opening line\n" if $code =~ /\bif\b.*[^{]\s*$/m;
+  #print "'while' blocks must be braced, '{' should be last character on block opening line\n" if $code =~ /\bwhile\b.*[^{]\s*$/m;
+  #print "'for' blocks must be braced, '{' should be last character on block opening line\n" if $code =~ /\bfor\b.*[^{]\s*$/m;
+  print "'else' cannot start a line (should follow preceding '}')\n" if $code =~ /^\s+else\b/m;
+}
+
+sub check_as_header_cpp {
+  my($buf) = @_;
+  check_as_any_cpp($buf);
+}
+
+sub check_as_source_cpp {
+  my($buf) = @_;
+  check_as_any_cpp($buf);
+}
+
+## Local Variables:
+## perl-indent-level: 2
+## perl-brace-offset: 0
+## End:
diff --git a/contrib/indent-settings b/contrib/indent-settings
new file mode 100644
index 000000000..41637fd42
--- /dev/null
+++ b/contrib/indent-settings
@@ -0,0 +1 @@
+indent -l 80 -lc 80 -lps -bli 2 -bbo -nbbb -bap -bad -br -brf -brs -cbi 1 -ce -cdw -cli 0 -hnl -i 2 -il 0 -lp -ci 0 -nut -ss -npro -npcs -nprs -npsl -nsaf -nsai -nsaw -sc -cd0 -dj0
diff --git a/src/context/Makefile.am b/src/context/Makefile.am
index b36d5e69c..54accdd6e 100644
--- a/src/context/Makefile.am
+++ b/src/context/Makefile.am
@@ -9,5 +9,8 @@ libcontext_la_SOURCES = \
 	context.cpp \
 	context.h \
 	context_mm.cpp \
-	context_mm.h
-
+	context_mm.h \
+	cdo.h \
+	cdlist.h \
+	cdmap.h \
+	cdset.h
diff --git a/src/context/cdlist.h b/src/context/cdlist.h
new file mode 100644
index 000000000..5b4ba639a
--- /dev/null
+++ b/src/context/cdlist.h
@@ -0,0 +1,222 @@
+/*********************                                                        */
+/** cdlist.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Context-dependent list class.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__CONTEXT__CDLIST_H
+#define __CVC4__CONTEXT__CDLIST_H
+
+#include "context/context.h"
+#include "util/Assert.h"
+
+namespace CVC4 {
+namespace context {
+
+/**
+ * Generic context-dependent dynamic array.  Note that for efficiency, this
+ * implementation makes the following assumptions:
+ * 1. Over time, objects are only added to the list.  Objects are only
+ *    removed when a pop restores the list to a previous state.
+ * 2. T objects can safely be copied using their copy constructor,
+ *    operator=, and memcpy.
+ */
+template <class T>
+class CDList : public ContextObj {
+  /**
+   * d_list is a dynamic array of objects of type T.
+   */
+  T* d_list;
+
+  /**
+   * Whether to call the destructor when items are popped from the
+   * list.  True by default, but can be set to false by setting the
+   * second argument in the constructor to false.
+   */
+  bool d_callDestructor;
+
+  /**
+   * Number of objects in d_list
+   */
+  unsigned d_size;
+
+  /**
+   * Allocated size of d_list.
+   */
+  unsigned d_sizeAlloc;
+
+  /**
+   * Implementation of mandatory ContextObj method save: simply copies the
+   * current size to a copy using the copy constructor (the pointer and the
+   * allocated size are *not* copied as they are not restored on a pop).
+   * The saved information is allocated using the ContextMemoryManager.
+   */
+  ContextObj* save(ContextMemoryManager* pCMM) {
+    return new(pCMM) CDList<T>(*this);
+  }
+
+  /**
+   * Implementation of mandatory ContextObj method restore: simply restores the
+   * previous size.  Note that the list pointer and the allocated size are not
+   * changed.
+   */
+  void restore(ContextObj* data) {
+    if(d_callDestructor) {
+      unsigned size = ((CDList<T>*)data)->d_size;
+      while(d_size != size) {
+        --d_size;
+        d_list[d_size].~T();
+      }
+    } else {
+      d_size = ((CDList<T>*)data)->d_size;
+    }
+  }
+
+  /**
+   * Privae copy constructor used only by save above.  d_list and d_sizeAlloc
+   * are not copied: only the base class information and d_size are needed in
+   * restore.
+   */
+  CDList(const CDList<T>& l) :
+    ContextObj(l),
+    d_list(NULL),
+    d_size(l.d_size),
+    d_sizeAlloc(0) {
+  }
+
+  /**
+   * Reallocate the array with more space.
+   * Throws bad_alloc if memory allocation fails.
+   */
+  void grow() {
+    if(d_list == NULL) {
+      // Allocate an initial list if one does not yet exist
+      d_sizeAlloc = 10;
+      d_list = (T*) malloc(sizeof(T) * d_sizeAlloc);
+      if(d_list == NULL) {
+        throw std::bad_alloc();
+      }
+    } else {
+      // Allocate a new array with double the size
+      d_sizeAlloc *= 2;
+      T* tmpList = (T*) realloc(d_list, sizeof(T) * d_sizeAlloc);
+      if(tmpList == NULL) {
+        throw std::bad_alloc();
+      }
+      d_list = tmpList;
+    }
+  }
+
+public:
+  /**
+   * Main constructor: d_list starts as NULL, size is 0
+   */
+ CDList(Context* context, bool callDestructor = true)
+   : ContextObj(context), d_list(NULL), d_callDestructor(callDestructor),
+    d_size(0), d_sizeAlloc(0) { }
+
+  /**
+   * Destructor: delete the list
+   */
+  ~CDList() throw() {
+    if(d_list != NULL) {
+      if(d_callDestructor) {
+        while(d_size != 0) {
+          --d_size;
+          d_list[d_size].~T();
+        }
+      }
+      free(d_list);
+    }
+  }
+
+  /**
+   * Return the current size of (i.e. valid number of objects in) the list
+   */
+  unsigned size() const { return d_size; }
+
+
+  /**
+   * Return true iff there are no valid objects in the list.
+   */
+  bool empty() const { return d_size == 0; }
+
+  /**
+   * Add an item to the end of the list.
+   */
+  void push_back(const T& data) {
+    makeCurrent();
+    if(d_size == d_sizeAlloc) grow();
+    ::new((void*)(d_list + d_size)) T(data);
+    ++ d_size;
+  }
+
+  /**
+   * operator[]: return the ith item in the list
+   */
+  const T& operator[](unsigned i) const {
+    Assert(i < d_size, "index out of bounds in CDList::operator[]");
+    return d_list[i];
+  }
+
+  /**
+   * return the most recent item added to the list
+   */
+  const T& back() const {
+    Assert(d_size > 0, "CDList::back() called on empty list");
+    return d_list[d_size-1];
+  }
+
+  /**
+   * Iterator for CDList class.  It has to be const because we don't allow
+   * items in the list to be changed.  It's a straightforward wrapper around a
+   * pointer.  Note that for efficiency, we implement only prefix increment and
+   * decrement.  Also note that it's OK to create an iterator from an empty,
+   * uninitialized list, as begin() and end() will have the same value (NULL).
+   */
+  class const_iterator {
+    friend class CDList<T>;
+    T* d_it;
+    const_iterator(T* it) : d_it(it) {};
+  public:
+    const_iterator() : d_it(NULL) {}
+    bool operator==(const const_iterator& i) const { return d_it == i.d_it; }
+    bool operator!=(const const_iterator& i) const { return d_it != i.d_it; }
+    const T& operator*() const { return *d_it; }
+    /** Prefix increment */
+    const_iterator& operator++() { ++d_it; return *this; }
+    /** Prefix decrement */
+    const_iterator& operator--() { --d_it; return *this; }
+  }; /* class const_iterator */
+
+  /**
+   * Returns an iterator pointing to the first item in the list.
+   */
+  const_iterator begin() const {
+    return const_iterator(d_list);
+  }
+
+  /**
+   * Returns an iterator pointing one past the last item in the list.
+   */
+  const_iterator end() const {
+    return const_iterator(d_list + d_size);
+  }
+
+};/* class CDList */
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CONTEXT__CDLIST_H */
diff --git a/src/context/cdmap.h b/src/context/cdmap.h
new file mode 100644
index 000000000..994ff76b4
--- /dev/null
+++ b/src/context/cdmap.h
@@ -0,0 +1,407 @@
+/*********************                                                        */
+/** cdmap.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Context-dependent map class.  Generic templated class for a map
+ ** which must be saved and restored as contexts are pushed and
+ ** popped.  Requires that operator= be defined for the data class,
+ ** and operator== for the key class.  For key types that don't have a
+ ** __gnu_cxx::hash<>, you should provide an explicit HashFcn.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__CONTEXT__CDMAP_H
+#define __CVC4__CONTEXT__CDMAP_H
+
+#include "context/context.h"
+#include "util/Assert.h"
+
+#include <iterator>
+#include <ext/hash_map>
+
+namespace CVC4 {
+namespace context {
+
+// Auxiliary class: almost the same as CDO (see cdo.h), but on
+// setNull() call it erases itself from the map.
+
+template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> > class CDMap;
+
+template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+class CDOmap : public ContextObj {
+  Key d_key;
+  Data d_data;
+  bool d_inMap; // whether the data must be in the map
+  CDMap<Key, Data, HashFcn>* d_cdmap;
+
+  // Doubly-linked list for keeping track of elements in order of insertion
+  CDOmap<Key, Data, HashFcn>* d_prev;
+  CDOmap<Key, Data, HashFcn>* d_next;
+
+  virtual ContextObj* save(ContextMemoryManager* pCMM) {
+    return new(pCMM) CDOmap<Key, Data, HashFcn>(*this);
+  }
+
+  virtual void restore(ContextObj* data) {
+    CDOmap<Key, Data, HashFcn>* p((CDOmap<Key, Data, HashFcn>*) data);
+    if(p->d_inMap) {
+      d_data = p->d_data;
+      d_inMap = true;
+    } else {
+      // Erase itself from the map and put itself into trash.  We cannot
+      // "delete this" here, because it will break context operations in
+      // a non-trivial way.
+      if(d_cdmap->d_map.count(d_key) > 0) {
+        d_cdmap->d_map.erase(d_key);
+        d_cdmap->d_trash.push_back(this);
+      }
+
+      d_prev->d_next = d_next;
+      d_next->d_prev = d_prev;
+
+      if(d_cdmap->d_first == this) {
+        d_cdmap->d_first = d_next;
+
+        if(d_next == this) {
+          d_cdmap->d_first = NULL;
+        }
+      }
+    }
+  }
+
+public:
+
+  CDOmap(Context* context,
+         CDMap<Key, Data, HashFcn>* cdmap,
+	 const Key& key,
+         const Data& data) :
+    ContextObj(context),
+    d_key(key),
+    d_inMap(false),
+    d_cdmap(cdmap) {
+
+    set(data);
+
+    CDOmap<Key, Data, HashFcn>*& first = d_cdmap->d_first;
+    if(first == NULL) {
+      first = d_next = d_prev = this;
+    } else {
+      d_prev = first->d_prev;
+      d_next = first;
+      d_prev->d_next = first->d_prev = this;
+    }
+  }
+
+  ~CDOmap() throw(AssertionException) {}
+
+  void set(const Data& data) {
+    makeCurrent();
+    d_data = data;
+    d_inMap = true;
+  }
+
+  const Key& getKey() const {
+    return d_key;
+  }
+
+  const Data& get() const {
+    return d_data;
+  }
+
+  operator Data() {
+    return get();
+  }
+
+  CDOmap<Key, Data, HashFcn>& operator=(const Data& data) {
+    set(data);
+    return *this;
+  }
+
+  CDOmap<Key, Data, HashFcn>* next() const {
+    if(d_next == d_cdmap->d_first) {
+      return NULL;
+    } else {
+      return d_next;
+    }
+  }
+};/* class CDOmap */
+
+// Dummy subclass of ContextObj to serve as our data class
+class CDMapData : public ContextObj {
+  // befriend CDMap<> so that it can allocate us
+  template <class Key, class Data, class HashFcn>
+  friend class CDMap;
+
+  ContextObj* save(ContextMemoryManager* pCMM) {
+    return new(pCMM) CDMapData(*this);
+  }
+
+  void restore(ContextObj* data) {}
+
+public:
+
+  CDMapData(Context* context) : ContextObj(context) {}
+  CDMapData(const ContextObj& co) : ContextObj(co) {}
+};
+
+/**
+ * Generic templated class for a map which must be saved and restored
+ * as contexts are pushed and popped.  Requires that operator= be
+ * defined for the data class, and operator== for the key class.
+ */
+template <class Key, class Data, class HashFcn>
+class CDMap : public ContextObj {
+
+  friend class CDOmap<Key, Data, HashFcn>;
+
+  __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn> d_map;
+
+  // The vector of CDOmap objects to be destroyed
+  std::vector<CDOmap<Key, Data, HashFcn>*> d_trash;
+  CDOmap<Key, Data, HashFcn>* d_first;
+  Context* d_context;
+
+  // Nothing to save; the elements take care of themselves
+  virtual ContextObj* save(ContextMemoryManager* pCMM) {
+    return new(pCMM) CDMapData(*this);
+  }
+
+  // Similarly, nothing to restore
+  virtual void restore(ContextObj* data) {}
+
+  // Destroy stale CDOmap objects from trash
+  void emptyTrash() {
+    for(typename std::vector<CDOmap<Key, Data, HashFcn>*>::iterator
+          i = d_trash.begin(), iend = d_trash.end(); i != iend; ++i) {
+      /*
+        delete *i;
+        free(*i);
+      */
+    }
+    d_trash.clear();
+  }
+
+public:
+
+  CDMap(Context* context) :
+    ContextObj(context),
+    d_first(NULL),
+    d_context(context) {
+  }
+
+  ~CDMap() throw(AssertionException) {
+    // Delete all the elements and clear the map
+    for(typename __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn>::iterator
+	  i = d_map.begin(), iend = d_map.end(); i != iend; ++i) {
+      /*
+        delete (*i).second;
+        free((*i).second);
+      */
+    }
+    d_map.clear();
+    emptyTrash();
+  }
+
+  // The usual operators of map
+
+  size_t size() const {
+    return d_map.size();
+  }
+
+  size_t count(const Key& k) const {
+    return d_map.count(k);
+  }
+
+  typedef CDOmap<Key, Data, HashFcn>& ElementReference;
+
+  // If a key is not present, a new object is created and inserted
+  CDOmap<Key, Data, HashFcn>& operator[](const Key& k) {
+    emptyTrash();
+
+    typename __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn>::iterator
+      i(d_map.find(k));
+
+    CDOmap<Key, Data, HashFcn>* obj;
+    if(i == d_map.end()) { // Create new object
+      obj = new(true) CDOmap<Key, Data, HashFcn>(d_context, this, k, Data());
+      d_map[k] = obj;
+    } else {
+      obj = (*i).second;
+    }
+    return *obj;
+  }
+
+  void insert(const Key& k, const Data& d) {
+    emptyTrash();
+
+    typename __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn>::iterator
+      i(d_map.find(k));
+
+    if(i == d_map.end()) { // Create new object
+      CDOmap<Key, Data, HashFcn>*
+	obj(new(true) CDOmap<Key, Data, HashFcn>(d_context, this, k, d));
+      d_map[k] = obj;
+    } else {
+      (*i).second->set(d);
+    }
+  }
+  // FIXME: no erase(), too much hassle to implement efficiently...
+
+  // Iterator for CDMap: points to pair<const Key, CDOMap<Key, Data, HashFcn>&>;
+  // in most cases, this will be functionally similar to pair<const Key, Data>.
+  class iterator : public std::iterator<std::input_iterator_tag, std::pair<const Key, Data>, std::ptrdiff_t> {
+
+    // Private members
+    typename __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn>::const_iterator d_it;
+
+  public:
+
+    // Constructor from __gnu_cxx::hash_map
+    iterator(const typename __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn>::const_iterator& i) : d_it(i) {}
+
+    // Copy constructor
+    iterator(const iterator& i) : d_it(i.d_it) {}
+
+    // Default constructor
+    iterator() {}
+
+    // (Dis)equality
+    bool operator==(const iterator& i) const {
+      return d_it == i.d_it;
+    }
+    bool operator!=(const iterator& i) const {
+      return d_it != i.d_it;
+    }
+
+    // Dereference operators.
+    std::pair<const Key, Data> operator*() const {
+      const std::pair<const Key, CDOmap<Key, Data, HashFcn>*>& p(*d_it);
+      return std::pair<const Key, Data>(p.first, *p.second);
+    }
+
+    // Who needs an operator->() for maps anyway?...
+    // It'd be nice, but not possible by design.
+    //std::pair<const Key, Data>* operator->() const {
+    //  return &(operator*());
+    //}
+
+    // Prefix and postfix increment
+    iterator& operator++() {
+      ++d_it;
+      return *this;
+    }
+
+    // Postfix increment: requires a Proxy object to hold the
+    // intermediate value for dereferencing
+    class Proxy {
+      const std::pair<const Key, Data>* d_pair;
+    public:
+      Proxy(const std::pair<const Key, Data>& p): d_pair(&p) {}
+      std::pair<const Key, Data>& operator*() {
+        return *d_pair;
+      }
+    };/* class CDMap<>::iterator::Proxy */
+
+    // Actual postfix increment: returns Proxy with the old value.
+    // Now, an expression like *i++ will return the current *i, and
+    // then advance the iterator.  However, don't try to use Proxy for
+    // anything else.
+    Proxy operator++(int) {
+      Proxy e(*(*this));
+      ++(*this);
+      return e;
+    }
+  };/* class CDMap<>::iterator */
+
+  typedef iterator const_iterator;
+
+  iterator begin() const {
+    return iterator(d_map.begin());
+  }
+
+  iterator end() const {
+    return iterator(d_map.end());
+  }
+
+  class orderedIterator {
+    const CDOmap<Key, Data, HashFcn>* d_it;
+
+  public:
+
+    orderedIterator(const CDOmap<Key, Data, HashFcn>* p) : d_it(p) {}
+    orderedIterator(const orderedIterator& i) : d_it(i.d_it) {}
+
+    // Default constructor
+    orderedIterator() {}
+
+    // (Dis)equality
+    bool operator==(const orderedIterator& i) const {
+      return d_it == i.d_it;
+    }
+    bool operator!=(const orderedIterator& i) const {
+      return d_it != i.d_it;
+    }
+
+    // Dereference operators.
+    std::pair<const Key, Data> operator*() const {
+      return std::pair<const Key, Data>(d_it->getKey(), d_it->get());
+    }
+
+    // Prefix and postfix increment
+    orderedIterator& operator++() {
+      d_it = d_it->next();
+      return *this;
+    }
+
+    // Postfix increment: requires a Proxy object to hold the
+    // intermediate value for dereferencing
+    class Proxy {
+      const std::pair<const Key, Data>* d_pair;
+
+    public:
+
+      Proxy(const std::pair<const Key, Data>& p): d_pair(&p) {}
+
+      std::pair<const Key, Data>& operator*() {
+        return *d_pair;
+      }
+    };/* class CDMap<>::orderedIterator::Proxy */
+
+    // Actual postfix increment: returns Proxy with the old value.
+    // Now, an expression like *i++ will return the current *i, and
+    // then advance the orderedIterator.  However, don't try to use
+    // Proxy for anything else.
+    Proxy operator++(int) {
+      Proxy e(*(*this));
+      ++(*this);
+      return e;
+    }
+  };/* class CDMap<>::orderedIterator */
+
+  orderedIterator orderedBegin() const {
+    return orderedIterator(d_first);
+  }
+
+  orderedIterator orderedEnd() const {
+    return orderedIterator(NULL);
+  }
+
+  iterator find(const Key& k) const {
+    return iterator(d_map.find(k));
+  }
+
+};/* class CDMap<> */
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CONTEXT__CDMAP_H */
diff --git a/src/context/cdo.h b/src/context/cdo.h
new file mode 100644
index 000000000..6c30a70f4
--- /dev/null
+++ b/src/context/cdo.h
@@ -0,0 +1,122 @@
+/*********************                                                        */
+/** cdo.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** A context-dependent object.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__CONTEXT__CDO_H
+#define __CVC4__CONTEXT__CDO_H
+
+#include "context/context.h"
+#include "util/Assert.h"
+
+namespace CVC4 {
+namespace context {
+
+/**
+ * Most basic template for context-dependent objects.  Simply makes a copy
+ * (using the copy constructor) of class T when saving, and copies it back
+ * (using operator=) during restore.
+ */
+template <class T>
+class CDO : public ContextObj {
+
+  /**
+   * The data of type T being stored in this context-dependent object.
+   */
+  T d_data;
+
+  /**
+   * Implementation of mandatory ContextObj method save: simply copies the
+   * current data to a copy using the copy constructor.  Memory is allocated
+   * using the ContextMemoryManager.
+   */
+  virtual ContextObj* save(ContextMemoryManager* pCMM) {
+    return new(pCMM) CDO<T>(*this);
+  }
+
+  /**
+   * Implementation of mandatory ContextObj method restore: simply copies the
+   * saved data back from the saved copy using operator= for T.
+   */
+  virtual void restore(ContextObj* pContextObj) {
+    d_data = ((CDO<T>*) pContextObj)->d_data;
+  }
+
+  /**
+   * Copy constructor - it's private to ensure it is only used by save().
+   * Basic CDO objects, cannot be copied-they have to be unique.
+   */
+  CDO(const CDO<T>& cdo) : ContextObj(cdo), d_data(cdo.d_data) {}
+
+  /**
+   * operator= for CDO is private to ensure CDO object is not copied.
+   */
+  CDO<T>& operator=(const CDO<T>& cdo) {}
+
+public:
+  /**
+   * Main constructor - uses default constructor for T to create the initial
+   * value of d_data.
+   */
+  CDO(Context* context) : ContextObj(context) {}
+
+  /**
+   * Constructor from object of type T.  Creates a ContextObj and sets the data
+   * to the given data value.  Note that this value is only valid in the
+   * current Scope.  If the Scope is popped, the value will revert to whatever
+   * is assigned by the default constructor for T
+   */
+  CDO(Context* context, const T& data) : ContextObj(context) {
+    makeCurrent();
+    d_data = data;
+  }
+
+  /**
+   * Destructor - no need to do anything.
+   */
+  ~CDO() throw() {}
+
+  /**
+   * Set the data in the CDO.  First call makeCurrent.
+   */
+  void set(const T& data) {
+    makeCurrent();
+    d_data = data;
+  }
+
+  /**
+   * Get the current data from the CDO.  Read-only.
+   */
+  const T& get() const { return d_data; }
+
+  /**
+   * For convenience, define operator T to be the same as get().
+   */
+  operator T() { return get(); }
+
+  /**
+   * For convenience, define operator= that takes an object of type T.
+   */
+  CDO<T>& operator=(const T& data) {
+    set(data);
+    return *this;
+  }
+
+};/* class CDO */
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CONTEXT__CDO_H */
diff --git a/src/context/cdset.h b/src/context/cdset.h
new file mode 100644
index 000000000..48ad12daa
--- /dev/null
+++ b/src/context/cdset.h
@@ -0,0 +1,33 @@
+/*********************                                                        */
+/** cdset.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Context-dependent set class.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__CONTEXT__CDSET_H
+#define __CVC4__CONTEXT__CDSET_H
+
+#include "context/context.h"
+#include "util/Assert.h"
+
+namespace CVC4 {
+namespace context {
+
+template <class K, class HashFcn>
+class CDSet;
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CONTEXT__CDSET_H */
diff --git a/src/context/context.cpp b/src/context/context.cpp
index 5ff377194..8e87741b5 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -29,7 +29,7 @@ Context::Context() : d_pCNOpre(NULL), d_pCNOpost(NULL) {
 }
 
 
-Context::~Context() {
+Context::~Context() throw(AssertionException) {
   // Delete all Scopes
   popto(0);
 
@@ -38,13 +38,13 @@ Context::~Context() {
 
   // Clear ContextNotifyObj lists so there are no dangling pointers
   ContextNotifyObj* pCNO;
-  while (d_pCNOpre != NULL) {
+  while(d_pCNOpre != NULL) {
     pCNO = d_pCNOpre;
     pCNO->d_ppCNOprev = NULL;
     d_pCNOpre = pCNO->d_pCNOnext;
     pCNO->d_pCNOnext = NULL;
   }
-  while (d_pCNOpost != NULL) {
+  while(d_pCNOpost != NULL) {
     pCNO = d_pCNOpost;
     pCNO->d_ppCNOprev = NULL;
     d_pCNOpost = pCNO->d_pCNOnext;
@@ -69,7 +69,7 @@ void Context::pop() {
 
   // Notify the (pre-pop) ContextNotifyObj objects
   ContextNotifyObj* pCNO = d_pCNOpre;
-  while (pCNO != NULL) {
+  while(pCNO != NULL) {
     pCNO->notify();
     pCNO = pCNO->d_pCNOnext;
   }
@@ -88,7 +88,7 @@ void Context::pop() {
 
   // Notify the (post-pop) ContextNotifyObj objects
   pCNO = d_pCNOpost;
-  while (pCNO != NULL) {
+  while(pCNO != NULL) {
     pCNO->notify();
     pCNO = pCNO->d_pCNOnext;
   }
@@ -99,8 +99,8 @@ void Context::pop() {
 
 void Context::popto(int toLevel) {
   // Pop scopes until there are none left or toLevel is reached
-  if (toLevel < 0) toLevel = 0;
-  while (toLevel < getLevel()) pop();
+  if(toLevel < 0) toLevel = 0;
+  while(toLevel < getLevel()) pop();
 }
 
 
@@ -147,19 +147,17 @@ void ContextObj::update() {
 }
 
 
-ContextObj* ContextObj::restoreAndContinue()
-{
+ContextObj* ContextObj::restoreAndContinue() {
   // Variable to hold next object in list
   ContextObj* pContextObjNext;
 
   // Check the restore pointer.  If NULL, this must be the bottom Scope
-  if (d_pContextObjRestore == NULL) {
+  if(d_pContextObjRestore == NULL) {
     Assert(d_pScope == d_pScope->getContext()->getBottomScope(),
            "Expected bottom scope");
     pContextObjNext = d_pContextObjNext;
     // Nothing else to do
-  }
-  else {
+  } else {
     // Call restore to update the subclass data
     restore(d_pContextObjRestore);
 
@@ -177,48 +175,48 @@ ContextObj* ContextObj::restoreAndContinue()
 }
 
 
-ContextObj::ContextObj(Context* pContext)
-  : d_pContextObjRestore(NULL)
-{
+ContextObj::ContextObj(Context* pContext) :
+  d_pContextObjRestore(NULL) {
+
   Assert(pContext != NULL, "NULL context pointer");
+
   d_pScope = pContext->getBottomScope();
   d_pScope->addToChain(this);
 }
 
 
-ContextObj::~ContextObj()
-{
+ContextObj::~ContextObj() throw(AssertionException) {
   for(;;) {
-    if (next() != NULL) {
+    if(next() != NULL) {
       next()->prev() = prev();
     }
     *(prev()) = next();
-    if (d_pContextObjRestore == NULL) break;
+    if(d_pContextObjRestore == NULL) {
+      break;
+    }
     restoreAndContinue();
   }
 }
 
 
 ContextNotifyObj::ContextNotifyObj(Context* pContext, bool preNotify) {
-  if (preNotify) {
+  if(preNotify) {
     pContext->addNotifyObjPre(this);
-  }
-  else {
+  } else {
     pContext->addNotifyObjPost(this);
   }
 }
 
-ContextNotifyObj::~ContextNotifyObj()
-{
-  if (d_pCNOnext != NULL) {
+
+ContextNotifyObj::~ContextNotifyObj() throw(AssertionException) {
+  if(d_pCNOnext != NULL) {
     d_pCNOnext->d_ppCNOprev = d_ppCNOprev;
   }
-  if (d_ppCNOprev != NULL) {
+  if(d_ppCNOprev != NULL) {
     *(d_ppCNOprev) = d_pCNOnext;
   }
 }
 
-} /* CVC4::context namespace */
-
 
+} /* CVC4::context namespace */
 } /* CVC4 namespace */
diff --git a/src/context/context.h b/src/context/context.h
index 6a35945b7..4e10347d7 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -20,6 +20,7 @@
 
 #include "context/context_mm.h"
 #include "util/Assert.h"
+
 #include <cstdlib>
 #include <cstring>
 #include <new>
@@ -32,28 +33,27 @@ class Scope;
 class ContextObj;
 class ContextNotifyObj;
 
-  /**
-   * A Context encapsulates all of the dynamic state of the system.  Its main
-   * methods are push() and pop().  A call to push() saves the current state,
-   * and a call to pop() restores the state saved by the most recent call to
-   * push().
-   *
-   * Objects which want to participate in this global save and restore
-   * mechanism must inherit from ContextObj (see below).
-   *
-   * For more flexible context-dependent behavior, objects may implement the
-   * ContextNotifyObj interface and simply get a notification when a pop has
-   * occurred.
-   *
-   * Context also uses a helper class called Scope which stores information
-   * specific to the portion of the Context since the last call to push() (see
-   * below).
-   *
-   * Memory allocation in Contexts is done with the help of the
-   * ContextMemoryManager.  A copy is stored in each Scope object for quick
-   * access.
-   *
-   */
+/**
+ * A Context encapsulates all of the dynamic state of the system.  Its main
+ * methods are push() and pop().  A call to push() saves the current state,
+ * and a call to pop() restores the state saved by the most recent call to
+ * push().
+ *
+ * Objects which want to participate in this global save and restore
+ * mechanism must inherit from ContextObj (see below).
+ *
+ * For more flexible context-dependent behavior, objects may implement the
+ * ContextNotifyObj interface and simply get a notification when a pop has
+ * occurred.
+ *
+ * Context also uses a helper class called Scope which stores information
+ * specific to the portion of the Context since the last call to push() (see
+ * below).
+ *
+ * Memory allocation in Contexts is done with the help of the
+ * ContextMemoryManager.  A copy is stored in each Scope object for quick
+ * access.
+ */
 class Context {
 
   /**
@@ -87,7 +87,7 @@ public:
   /**
    * Destructor: pop all scopes, delete ContextMemoryManager
    */
-  ~Context();
+  ~Context() throw(AssertionException);
 
   /**
    * Return the current (top) scope
@@ -107,7 +107,7 @@ public:
   /**
    * Return the ContextMemoryManager associated with the context.
    */
-  ContextMemoryManager* getCMM(){ return d_pCMM; }
+  ContextMemoryManager* getCMM() { return d_pCMM; }
 
   /**
    * Save the current state, create a new Scope
@@ -182,15 +182,18 @@ public:
    * Constructor: Create a new Scope; set the level and the previous Scope
    * if any.
    */
-  Scope(Context* pContext, ContextMemoryManager* pCMM, int level)
-    : d_pContext(pContext), d_pCMM(pCMM), d_level(level),
-      d_pContextObjList(NULL) { }
+  Scope(Context* pContext, ContextMemoryManager* pCMM, int level) :
+    d_pContext(pContext),
+    d_pCMM(pCMM),
+    d_level(level),
+    d_pContextObjList(NULL) {
+  }
 
   /**
    * Destructor: Restore all of the objects in ContextObjList.  Defined inline
    * below.
    */
-  ~Scope();
+  ~Scope() throw();
 
   /**
    * Get the Context for this Scope
@@ -223,8 +226,9 @@ public:
    * Overload operator new for use with ContextMemoryManager to allow creation
    * of new Scope objects in the current memory region.
    */
-  static void* operator new(size_t size, ContextMemoryManager* pCMM)
-    { return pCMM->newData(size); }
+  static void* operator new(size_t size, ContextMemoryManager* pCMM) {
+    return pCMM->newData(size);
+  }
 
   /**
    * Overload operator delete for Scope objects allocated using
@@ -232,44 +236,44 @@ public:
    * automatically when the ContextMemoryManager pop() method is called.
    * Include both placement and standard delete for completeness.
    */
-  static void operator delete(void* pMem, ContextMemoryManager* pCMM) { }
-  static void operator delete(void* pMem) { }
+  static void operator delete(void* pMem, ContextMemoryManager* pCMM) {}
+  static void operator delete(void* pMem) {}
 
   //FIXME:  //! Check for memory leaks
   //  void check(void);
 
-}; /* class Scope */
-
-  /**
-   * This is an abstract base class from which all objects that are context-dependent
-   * should inherit.  For any data structure that you want to have be
-   * automatically backtracked, do the following:
-   * 1. Create a class for the data structure that inherits from ContextObj
-   * 2. Implement save()
-   *    The role of save() is to create a new ContexObj object that contains
-   *    enough information to restore the object to its current state, even if
-   *    it gets changed later.  Note that save should call the (default)
-   *    ContextObj Copy Constructor to copy the information in the base class.
-   *    It is recommended that any memory allocated by save() should be done
-   *    through the ContextMemoryManager.  This way, it does not need to be
-   *    explicitly freed when restore is called.  However, it is only required
-   *    that the ContextObj itself be allocated using the
-   *    ContextMemoryManager.  If other memory is allocated not using the
-   *    ContextMemoryManager, it should be freed when restore() is called.  In
-   *    fact, any clean-up work on a saved object must be done by restore().
-   *    This is because the destructor is never called explicitly on saved
-   *    objects.
-   * 3. Implement restore()
-   *    The role of restore() is, given the ContextObj returned by a previous
-   *    call to save(), to restore the current object to the state it was in
-   *    when save() was called.  Note that the implementation of restore does
-   *    *not* need to worry about restoring the base class data.  This is done
-   *    automatically.  Ideally, restore() should not have to free any memory
-   *    as any memory allocated by save() should have been done using the
-   *    ContextMemoryManager (see item 2 above).
-   * 4. In the subclass implementation, any time the state is about to be
-   *    changed, first call makeCurrent().
-   */
+};/* class Scope */
+
+/**
+ * This is an abstract base class from which all objects that are context-dependent
+ * should inherit.  For any data structure that you want to have be
+ * automatically backtracked, do the following:
+ * 1. Create a class for the data structure that inherits from ContextObj
+ * 2. Implement save()
+ *    The role of save() is to create a new ContexObj object that contains
+ *    enough information to restore the object to its current state, even if
+ *    it gets changed later.  Note that save should call the (default)
+ *    ContextObj Copy Constructor to copy the information in the base class.
+ *    It is recommended that any memory allocated by save() should be done
+ *    through the ContextMemoryManager.  This way, it does not need to be
+ *    explicitly freed when restore is called.  However, it is only required
+ *    that the ContextObj itself be allocated using the
+ *    ContextMemoryManager.  If other memory is allocated not using the
+ *    ContextMemoryManager, it should be freed when restore() is called.  In
+ *    fact, any clean-up work on a saved object must be done by restore().
+ *    This is because the destructor is never called explicitly on saved
+ *    objects.
+ * 3. Implement restore()
+ *    The role of restore() is, given the ContextObj returned by a previous
+ *    call to save(), to restore the current object to the state it was in
+ *    when save() was called.  Note that the implementation of restore does
+ *    *not* need to worry about restoring the base class data.  This is done
+ *    automatically.  Ideally, restore() should not have to free any memory
+ *    as any memory allocated by save() should have been done using the
+ *    ContextMemoryManager (see item 2 above).
+ * 4. In the subclass implementation, any time the state is about to be
+ *    changed, first call makeCurrent().
+ */
 class ContextObj {
   /**
    * Pointer to Scope in which this object was last modified.
@@ -325,6 +329,7 @@ class ContextObj {
   ContextObj* restoreAndContinue();
 
 protected:
+
   /**
    * This is a method that must be implemented by all classes inheriting from
    * ContextObj.  See the comment before the class declaration.
@@ -341,57 +346,70 @@ protected:
    * This method checks if the object has been modified in this Scope yet.  If
    * not, it calls update().
    */
-  void makeCurrent() { if (!(d_pScope->isCurrent())) update(); }
+  void makeCurrent() {
+    if(!(d_pScope->isCurrent())) {
+      update();
+    }
+  }
 
   /**
-   * operator new using ContextMemoryManager (common case used by subclasses
-   * during save() ).  No delete is required for memory allocated this way,
-   * since it is automatically released when the context is popped.  Also note
-   * that allocations using this operator never have their destructor called,
-   * so any clean-up has to be done using the restore method.
+   * operator new using ContextMemoryManager (common case used by
+   * subclasses during save() ).  No delete is required for memory
+   * allocated this way, since it is automatically released when the
+   * context is popped.  Also note that allocations using this
+   * operator never have their destructor called, so any clean-up has
+   * to be done using the restore method.
    */
   static void* operator new(size_t size, ContextMemoryManager* pCMM) {
     return pCMM->newData(size);
   }
 
   /**
-   * Corresponding placement delete.  Note that this is provided just to
-   * satisfy the requirement that a placement delete should be provided for
-   * every placement new.  It would only be called if a ContextObj Constructor
-   * throws an exception after a successful call to the above new operator.
+   * Corresponding placement delete.  Note that this is provided just
+   * to satisfy the requirement that a placement delete should be
+   * provided for every placement new.  It would only be called if a
+   * ContextObj constructor throws an exception after a successful
+   * call to the above new operator.
    */
-  static void operator delete(void* pMem, ContextMemoryManager* pCMM) { }
+  static void operator delete(void* pMem, ContextMemoryManager* pCMM) {}
 
 public:
+
   /**
    * Create a new ContextObj.  The initial scope is set to the bottom
-   * scope of the Context.  Note that in the common case, the copy constructor
-   * is called to create new ContextObj objects.  The default copy constructor
-   * does the right thing, so we do not explicitly define it.
+   * scope of the Context.  Note that in the common case, the copy
+   * constructor is called to create new ContextObj objects.  The
+   * default copy constructor does the right thing, so we do not
+   * explicitly define it.
    */
   ContextObj(Context* context);
 
   /**
-   * Destructor: Calls restore until restored to initial version.  Also removes
-   * object from all Scope lists.  Note that this doesn't actually free the
-   * memory allocated by the ContextMemoryManager for this object.  This isn't
-   * done until the corresponding Scope is popped.
+   * Destructor: Calls restore until restored to initial version.
+   * Also removes object from all Scope lists.  Note that this doesn't
+   * actually free the memory allocated by the ContextMemoryManager
+   * for this object.  This isn't done until the corresponding Scope
+   * is popped.
    */
-  virtual ~ContextObj();
+  virtual ~ContextObj() throw(AssertionException);
 
   /**
-   * If you want to allocate a ContextObj object on the heap, use this special
-   * new operator.  To free this memory, instead of "delete p", use
-   * "p->deleteSelf()".
+   * If you want to allocate a ContextObj object on the heap, use this
+   * special new operator.  To free this memory, instead of
+   * "delete p", use "p->deleteSelf()".
    */
-  static void* operator new(size_t size, bool) { return ::operator new(size); }
+  static void* operator new(size_t size, bool) {
+    return ::operator new(size);
+  }
 
   /**
-   * Corresponding placement delete.  Note that this is provided for the
-   * compiler in case the ContextObj constructor throws an exception.  The
-   * client can't call it.
+   * Corresponding placement delete.  Note that this is provided for
+   * the compiler in case the ContextObj constructor throws an
+   * exception.  The client can't call it.
    */
-  static void operator delete(void* pMem, bool) { ::operator delete(pMem); }
+  static void operator delete(void* pMem, bool) {
+    ::operator delete(pMem);
+  }
 
   /**
    * Use this instead of delete to delete memory allocated using the special
@@ -399,7 +417,9 @@ public:
    * function on memory allocated using the new that takes a
    * ContextMemoryManager as an argument.
    */
-  void deleteSelf() { ::operator delete(this); }
+  void deleteSelf() {
+    ::operator delete(this);
+  }
 
   /**
    * Disable delete: objects allocated with new(ContextMemorymanager) should
@@ -407,23 +427,23 @@ public:
    * calling deleteSelf().
    */
   static void operator delete(void* pMem) {
-    AlwaysAssert(false, "Not Allowed!");
+    AlwaysAssert(false, "It is not allowed to delete a ContextObj this way!");
   }
 
-}; /* class ContextObj */
+};/* class ContextObj */
 
   /**
-   * For more flexible context-dependent behavior than that provided by
-   * ContextObj, objects may implement the ContextNotifyObj interface and
-   * simply get a notification when a pop has occurred.  See Context class for
-   * how to register a ContextNotifyObj with the Context (you can choose to
-   * have notification come before or after the ContextObj objects have been
-   * restored).
+   * For more flexible context-dependent behavior than that provided
+   * by ContextObj, objects may implement the ContextNotifyObj
+   * interface and simply get a notification when a pop has occurred.
+   * See Context class for how to register a ContextNotifyObj with the
+   * Context (you can choose to have notification come before or after
+   * the ContextObj objects have been restored).
    */
 class ContextNotifyObj {
   /**
-   * Context is our friend so that when the Context is deleted, any remaining
-   * ContextNotifyObj can be removed from the Context list.
+   * Context is our friend so that when the Context is deleted, any
+   * remaining ContextNotifyObj can be removed from the Context list.
    */
   friend class Context;
 
@@ -451,18 +471,19 @@ class ContextNotifyObj {
 
 public:
   /**
-   * Constructor for ContextNotifyObj.  Parameters are the context to which
-   * this notify object will be added, and a flag which, if true, tells the
-   * context to notify this object *before* the ContextObj objects are
-   * restored.  Otherwise, the context notifies the object after the ContextObj
-   * objects are restored.  The default is for notification after.
+   * Constructor for ContextNotifyObj.  Parameters are the context to
+   * which this notify object will be added, and a flag which, if
+   * true, tells the context to notify this object *before* the
+   * ContextObj objects are restored.  Otherwise, the context notifies
+   * the object after the ContextObj objects are restored.  The
+   * default is for notification after.
    */
   ContextNotifyObj(Context* pContext, bool preNotify = false);
 
   /**
    * Destructor: removes object from list
    */
-  virtual ~ContextNotifyObj();
+  virtual ~ContextNotifyObj() throw(AssertionException);
 
   /**
    * This is the method called to notify the object of a pop.  It must be
@@ -473,11 +494,11 @@ public:
 
 // Inline functions whose definitions had to be delayed:
 
-inline Scope::~Scope() {
+inline Scope::~Scope() throw() {
   // Call restore() method on each ContextObj object in the list.
-  // Note that it is the responsibility of restore() to return the next item in
-  // the list.
-  while (d_pContextObjList != NULL) {
+  // Note that it is the responsibility of restore() to return the
+  // next item in the list.
+  while(d_pContextObjList != NULL) {
     d_pContextObjList = d_pContextObjList->restoreAndContinue();
   }
 }
@@ -490,290 +511,7 @@ inline void Scope::addToChain(ContextObj* pContextObj) {
   d_pContextObjList = pContextObj;
 }
 
-  /**
-   * Most basic template for context-dependent objects.  Simply makes a copy
-   * (using the copy constructor) of class T when saving, and copies it back
-   * (using operator=) during restore.
-   */
-template <class T>
-class CDO :public ContextObj {
-
-  /**
-   * The data of type T being stored in this context-dependent object.
-   */
-  T d_data;
-
-  /**
-   * Implementation of mandatory ContextObj method save: simply copies the
-   * current data to a copy using the copy constructor.  Memory is allocated
-   * using the ContextMemoryManager.
-   */
-  virtual ContextObj* save(ContextMemoryManager* pCMM) {
-    return new(pCMM) CDO<T>(*this);
-  }
-
-  /**
-   * Implementation of mandatory ContextObj method restore: simply copies the
-   * saved data back from the saved copy using operator= for T.
-   */
-  virtual void restore(ContextObj* pContextObj) {
-    d_data = ((CDO<T>*)pContextObj)->d_data;
-  }
-
-  /**
-   * Copy constructor - it's private to ensure it is only used by save().
-   * Basic CDO objects, cannot be copied-they have to be unique.
-   */
-  CDO(const CDO<T>& cdo): ContextObj(cdo), d_data(cdo.d_data) { }
-
-  /**
-   * operator= for CDO is private to ensure CDO object is not copied.
-   */
-  CDO<T>& operator=(const CDO<T>& cdo) {}
-
-public:
-  /**
-   * Main constructor - uses default constructor for T to create the initial
-   * value of d_data.
-   */
-  CDO(Context* context) : ContextObj(context) {}
-
-  /**
-   * Constructor from object of type T.  Creates a ContextObj and sets the data
-   * to the given data value.  Note that this value is only valid in the
-   * current Scope.  If the Scope is popped, the value will revert to whatever
-   * is assigned by the default constructor for T
-   */
-  CDO(Context* context, const T& data) : ContextObj(context) {
-    makeCurrent(); d_data = data;
-  }
-
-  /**
-   * Destructor - no need to do anything.
-   */
-  ~CDO() {}
-
-  /**
-   * Set the data in the CDO.  First call makeCurrent.
-   */
-  void set(const T& data) { makeCurrent(); d_data = data; }
-
-  /**
-   * Get the current data from the CDO.  Read-only.
-   */
-  const T& get() const { return d_data; }
-
-  /**
-   * For convenience, define operator T to be the same as get().
-   */
-  operator T() { return get(); }
-
-  /**
-   * For convenience, define operator= that takes an object of type T.
-   */
-  CDO<T>& operator=(const T& data) { set(data); return *this; }
-
-}; /* class CDO */
-
-  /**
-   * Generic context-dependent dynamic array.  Note that for efficiency, this
-   * implementation makes the following assumptions:
-   * 1. Over time, objects are only added to the list.  Objects are only
-   *    removed when a pop restores the list to a previous state.
-   * 2. T objects can safely be copied using their copy constructor,
-   *    operator=, and memcpy.
-   */
-template <class T>
-class CDList :public ContextObj {
-  /**
-   * d_list is a dynamic array of objects of type T.
-   */
-  T* d_list;
-
-  /**
-   * Whether to call the destructor when items are popped from the
-   * list.  True by default, but can be set to false by setting the
-   * second argument in the constructor to false.
-   */
-  bool d_callDestructor;
-
-  /**
-   * Number of objects in d_list
-   */
-  unsigned d_size;
-
-  /**
-   * Allocated size of d_list.
-   */
-  unsigned d_sizeAlloc;
-
-  /**
-   * Implementation of mandatory ContextObj method save: simply copies the
-   * current size to a copy using the copy constructor (the pointer and the
-   * allocated size are *not* copied as they are not restored on a pop).
-   * The saved information is allocated using the ContextMemoryManager.
-   */
-  ContextObj* save(ContextMemoryManager* pCMM) {
-    return new(pCMM) CDList<T>(*this);
-  }
-
-  /**
-   * Implementation of mandatory ContextObj method restore: simply restores the
-   * previous size.  Note that the list pointer and the allocated size are not
-   * changed.
-   */
-  void restore(ContextObj* data) {
-    if (d_callDestructor) {
-      unsigned size = ((CDList<T>*)data)->d_size;
-      while (d_size != size) {
-        --d_size;
-        d_list[d_size].~T();
-      }
-    }
-    else {
-      d_size = ((CDList<T>*)data)->d_size;
-    }
-  }
-
-  /**
-   * Privae copy constructor used only by save above.  d_list and d_sizeAlloc
-   * are not copied: only the base class information and d_size are needed in
-   * restore.
-   */
-  CDList(const CDList<T>& l): ContextObj(l), d_list(NULL),
-                              d_size(l.d_size), d_sizeAlloc(0) { }
-
-  /**
-   * Reallocate the array with more space.
-   * Throws bad_alloc if memory allocation fails.
-   */
-  void grow() {
-    if (d_list == NULL) {
-      // Allocate an initial list if one does not yet exist
-      d_sizeAlloc = 10;
-      d_list = (T*)malloc(sizeof(T)*d_sizeAlloc);
-      if(d_list == NULL){
-        throw std::bad_alloc();
-      }
-    }
-    else {
-      // Allocate a new array with double the size
-      d_sizeAlloc *= 2;
-      T* tmpList = (T*)realloc(d_list, sizeof(T)*d_sizeAlloc);
-      if(tmpList == NULL){
-        throw std::bad_alloc();
-      }
-      d_list = tmpList;
-    }
-  }
-
-public:
-  /**
-   * Main constructor: d_list starts as NULL, size is 0
-   */
- CDList(Context* context, bool callDestructor = true)
-   : ContextObj(context), d_list(NULL), d_callDestructor(callDestructor),
-    d_size(0), d_sizeAlloc(0) { }
-
-  /**
-   * Destructor: delete the list
-   */
-  ~CDList() {
-    if(d_list != NULL) {
-      if (d_callDestructor) {
-        while (d_size != 0) {
-          --d_size;
-          d_list[d_size].~T();
-        }
-      }
-      delete d_list;
-    }
-  }
-
-  /**
-   * Return the current size of (i.e. valid number of objects in) the list
-   */
-  unsigned size() const { return d_size; }
-
-
-  /**
-   * Return true iff there are no valid objects in the list.
-   */
-  bool empty() const { return d_size == 0; }
-
-  /**
-   * Add an item to the end of the list.
-   */
-  void push_back(const T& data) {
-    makeCurrent();
-    if (d_size == d_sizeAlloc) grow();
-    ::new((void*)(d_list + d_size)) T(data);
-    ++ d_size;
-  }
-
-  /**
-   * operator[]: return the ith item in the list
-   */
-  const T& operator[](unsigned i) const {
-    Assert(i < d_size, "index out of bounds in CDList::operator[]");
-    return d_list[i];
-  }
-
-  /**
-   * return the most recent item added to the list
-   */
-  const T& back() const {
-    Assert(d_size > 0, "CDList::back() called on empty list");
-    return d_list[d_size-1];
-  }
-
-  /**
-   * Iterator for CDList class.  It has to be const because we don't allow
-   * items in the list to be changed.  It's a straightforward wrapper around a
-   * pointer.  Note that for efficiency, we implement only prefix increment and
-   * decrement.  Also note that it's OK to create an iterator from an empty,
-   * uninitialized list, as begin() and end() will have the same value (NULL).
-   */
-  class const_iterator {
-    friend class CDList<T>;
-    T* d_it;
-    const_iterator(T* it) : d_it(it) {};
-  public:
-    const_iterator() : d_it(NULL) {}
-    bool operator==(const const_iterator& i) const { return d_it == i.d_it; }
-    bool operator!=(const const_iterator& i) const { return d_it != i.d_it; }
-    const T& operator*() const { return *d_it; }
-    /** Prefix increment */
-    const_iterator& operator++() { ++d_it; return *this; }
-    /** Prefix decrement */
-    const_iterator& operator--() { --d_it; return *this; }
-  }; /* class const_iterator */
-
-  /**
-   * Returns an iterator pointing to the first item in the list.
-   */
-  const_iterator begin() const {
-    return const_iterator(d_list);
-  }
-
-  /**
-   * Returns an iterator pointing one past the last item in the list.
-   */
-  const_iterator end() const {
-    return const_iterator(d_list + d_size);
-  }
-
-}; /* class CDList */
-
-template <class T>
-class CDMap;
-
-template <class T>
-class CDSet;
-
-} /* CVC4::context namespace */
-
-} /* CVC4 namespace */
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
 
 #endif /* __CVC4__CONTEXT__CONTEXT_H */
-
diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp
index df7d82987..ab81c7486 100644
--- a/src/context/context_mm.cpp
+++ b/src/context/context_mm.cpp
@@ -32,9 +32,9 @@ void ContextMemoryManager::newChunk() {
          "Index should be at the end of the list");
 
   // Create new chunk if no free chunk available
-  if (d_freeChunks.empty()) {
+  if(d_freeChunks.empty()) {
     d_chunkList.push_back((char*)malloc(chunkSizeBytes));
-    if (d_chunkList.back() == NULL) {
+    if(d_chunkList.back() == NULL) {
       throw std::bad_alloc();
     }
   }
@@ -53,31 +53,32 @@ ContextMemoryManager::ContextMemoryManager() : d_indexChunkList(0) {
   // Create initial chunk
   d_chunkList.push_back((char*)malloc(chunkSizeBytes));
   d_nextFree = d_chunkList.back();
-  if (d_nextFree == NULL) {
+  if(d_nextFree == NULL) {
     throw std::bad_alloc();
   }
   d_endChunk = d_nextFree + chunkSizeBytes;
 }
 
 
-ContextMemoryManager::~ContextMemoryManager() {
+ContextMemoryManager::~ContextMemoryManager() throw() {
   // Delete all chunks
-  while (!d_chunkList.empty()) {
+  while(!d_chunkList.empty()) {
     free(d_chunkList.back());
     d_chunkList.pop_back();
   }
-  while (!d_freeChunks.empty()) {
+  while(!d_freeChunks.empty()) {
     free(d_freeChunks.back());
     d_freeChunks.pop_back();
   }
 }
 
+
 void* ContextMemoryManager::newData(size_t size) {
   // Use next available free location in current chunk
   void* res = (void*)d_nextFree;
   d_nextFree += size;
   // Check if the request is too big for the chunk
-  if (d_nextFree > d_endChunk) {
+  if(d_nextFree > d_endChunk) {
     newChunk();
     res = (void*)d_nextFree;
     d_nextFree += size;
@@ -104,7 +105,7 @@ void ContextMemoryManager::pop() {
   d_endChunkStack.pop_back();
 
   // Free all the new chunks since the last push
-  while (d_indexChunkList > d_indexChunkListStack.back()) {
+  while(d_indexChunkList > d_indexChunkListStack.back()) {
     d_freeChunks.push_back(d_chunkList.back());
     d_chunkList.pop_back();
     --d_indexChunkList;
@@ -112,7 +113,7 @@ void ContextMemoryManager::pop() {
   d_indexChunkListStack.pop_back();
 
   // Delete excess free chunks
-  while (d_freeChunks.size() > maxFreeChunks) {
+  while(d_freeChunks.size() > maxFreeChunks) {
     free(d_freeChunks.front());
     d_freeChunks.pop_front();
   }
@@ -120,6 +121,4 @@ void ContextMemoryManager::pop() {
 
 
 } /* CVC4::context namespace */
-
-
 } /* CVC4 namespace */
diff --git a/src/context/context_mm.h b/src/context/context_mm.h
index c4e5aba4f..04b0c8167 100644
--- a/src/context/context_mm.h
+++ b/src/context/context_mm.h
@@ -25,17 +25,16 @@
 namespace CVC4 {
 namespace context {
 
-
-  /**
-   * Region-based memory manager for contexts.  Calls to newData provide memory
-   * from the current region.  This memory will persist until the entire
-   * region is deallocated (by calling pop).
-   *
-   * If push is called, the current region is deactivated and pushed on a
-   * stack, and a new current region is created.  A subsequent call to pop
-   * releases the new region and restores the top region from the stack.
-   *
-   */
+/**
+ * Region-based memory manager for contexts.  Calls to newData provide memory
+ * from the current region.  This memory will persist until the entire
+ * region is deallocated (by calling pop).
+ *
+ * If push is called, the current region is deactivated and pushed on a
+ * stack, and a new current region is created.  A subsequent call to pop
+ * releases the new region and restores the top region from the stack.
+ *
+ */
 class ContextMemoryManager {
 
   /**
@@ -102,6 +101,7 @@ class ContextMemoryManager {
   void newChunk();
 
  public:
+
   /**
    * Constructor - creates an initial region and an empty stack
    */
@@ -110,7 +110,7 @@ class ContextMemoryManager {
   /**
    * Destructor - deletes all memory in all regions
    */
-  ~ContextMemoryManager();
+  ~ContextMemoryManager() throw();
 
   /**
    * Allocate size bytes from the current region
@@ -128,7 +128,7 @@ class ContextMemoryManager {
    */
   void pop();
 
-}; /* class ContextMemoryManager */
+};/* class ContextMemoryManager */
 
 }/* CVC4::context namespace */
 }/* CVC4 namespace */
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 */
 
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index baad6fe31..b319b7293 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -46,12 +46,6 @@ Languages currently supported as arguments to the -L / --lang option:\n\
   smt | smtlib  SMT-LIB format\n\
 ";
 
-static const char cnf_help[] = "\
-CNF conversions currently supported as arguments to the --cnf option:\n\
-  direct  put in equiv. CNF directly (exp. blow up in # clauses, no new vars)\n\
-  var     variable-introduction method (new vars, no exp. blow up in # clauses)\n\
-";
-
 /**
  * For the main getopt() routine, we need ways to switch on long
  * options without clashing with short option characters.  This is an
@@ -61,8 +55,7 @@ CNF conversions currently supported as arguments to the --cnf option:\n\
  * any collision.
  */
 enum OptionValue {
-  CNF = 256, /* no clash with char options */
-  SMTCOMP,
+  SMTCOMP = 256, /* no clash with char options */
   STATS,
   SEGV_NOSPIN,
   PARSE_ONLY,
@@ -98,7 +91,6 @@ static struct option cmdlineOptions[] = {
   { "quiet"      , no_argument      , NULL, 'q'         },
   { "lang"       , required_argument, NULL, 'L'         },
   { "debug"      , required_argument, NULL, 'd'         },
-  { "cnf"        , required_argument, NULL, CNF         },
   { "smtcomp"    , no_argument      , NULL, SMTCOMP     },
   { "stats"      , no_argument      , NULL, STATS       },
   { "segv-nospin", no_argument      , NULL, SEGV_NOSPIN },
@@ -179,21 +171,6 @@ throw(OptionException) {
       fputs(lang_help, stdout);
       exit(1);
 
-    case CNF:
-      if(!strcmp(optarg, "direct")) {
-        opts->d_cnfConversion = CNF_DIRECT_EXPONENTIAL;
-        break;
-      } else if(!strcmp(optarg, "var")) {
-        opts->d_cnfConversion = CNF_VAR_INTRODUCTION;
-        break;
-      } else if(strcmp(optarg, "help")) {
-        throw OptionException(string("unknown CNF conversion for --cnf: `") +
-                              optarg + "'.  Try --cnf help.");
-      }
-
-      fputs(cnf_help, stdout);
-      exit(1);
-
     case 'd':
       Debug.on(optarg);
       /* fall-through */
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 2eea56947..1da56b9f9 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -151,7 +151,7 @@ int runCvc4(int argc, char *argv[]) {
   } else {
     string filename = argv[firstArgIndex];
     input = new ifstream(filename.c_str());
-    if(input == NULL) {
+    if(!*input) {
       throw Exception("file does not exist or is unreadable: " + filename);
     }
     parser = Parser::getNewParser(&exprMgr, options.lang, *input, filename);
diff --git a/src/main/util.cpp b/src/main/util.cpp
index adb117b9d..a2b46513d 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -16,6 +16,7 @@
 #include <cstdio>
 #include <cstdlib>
 #include <cerrno>
+#include <exception>
 #include <string.h>
 #include <signal.h>
 
@@ -63,6 +64,45 @@ void segv_handler(int sig, siginfo_t* info, void*) {
 #endif /* CVC4_DEBUG */
 }
 
+static terminate_handler default_terminator;
+
+void cvc4unexpected() {
+#ifdef CVC4_DEBUG
+  fprintf(stderr,
+          "\n"
+          "CVC4 threw an \"unexpected\" exception (one that wasn't properly specified\n"
+          "in the throws() specifier for the throwing function).\n\n");
+  if(segvNoSpin) {
+    fprintf(stderr, "No-spin requested.\n");
+    set_terminate(default_terminator);
+  } else {
+    fprintf(stderr, "Spinning so that a debugger can be connected.\n");
+    fprintf(stderr, "Try:  gdb %s %u\n", progName, getpid());
+    for(;;) {
+      sleep(60);
+    }
+  }
+#else /* CVC4_DEBUG */
+  fprintf(stderr, "CVC4 threw an \"unexpected\" exception.\n");
+  set_terminate(default_terminator);
+#endif /* CVC4_DEBUG */
+}
+
+void cvc4terminate() {
+#ifdef CVC4_DEBUG
+  fprintf(stderr,
+          "\n"
+          "CVC4 was terminated by the C++ runtime.\n"
+          "Perhaps an exception was thrown during stack unwinding.  (Don't do that.)\n");
+  default_terminator();
+#else /* CVC4_DEBUG */
+  fprintf(stderr,
+          "CVC4 was terminated by the C++ runtime.\n"
+          "Perhaps an exception was thrown during stack unwinding.\n");
+  default_terminator();
+#endif /* CVC4_DEBUG */
+}
+
 /** Initialize the driver.  Sets signal handlers for SIGINT and SIGSEGV. */
 void cvc4_init() throw() {
   struct sigaction act1;
@@ -78,6 +118,9 @@ void cvc4_init() throw() {
   sigemptyset(&act2.sa_mask);
   if(sigaction(SIGSEGV, &act2, NULL))
     throw Exception(string("sigaction(SIGSEGV) failure: ") + strerror(errno));
+
+  set_unexpected(cvc4unexpected);
+  default_terminator = set_terminate(cvc4terminate);
 }
 
 }/* CVC4::main namespace */
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index 6eb269bca..e2949286a 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -171,10 +171,10 @@ const Type* AntlrParser::predicateType(const std::vector<const Type*>& sorts) {
 Expr 
 AntlrParser::mkVar(const std::string& name, const Type* type) {
   Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl;
-  Assert( !isDeclared(name) ) ;
+  Assert( !isDeclared(name) );
   Expr expr = d_exprManager->mkVar(type, name);
   d_varSymbolTable.bindName(name, expr);
-  Assert( isDeclared(name) ) ;
+  Assert( isDeclared(name) );
   return expr;
 }
 
@@ -192,10 +192,10 @@ AntlrParser::mkVars(const std::vector<std::string> names,
 const Type* 
 AntlrParser::newSort(const std::string& name) {
   Debug("parser") << "newSort(" << name << ")" << std::endl;
-  Assert( !isDeclared(name, SYM_SORT) ) ;
+  Assert( !isDeclared(name, SYM_SORT) );
   const Type* type = d_exprManager->mkSort(name);
   d_sortTable.bindName(name, type);
-  Assert( isDeclared(name, SYM_SORT) ) ;
+  Assert( isDeclared(name, SYM_SORT) );
   return type;
 }
 
diff --git a/src/parser/memory_mapped_input_buffer.h b/src/parser/memory_mapped_input_buffer.h
index c92e62524..e1639a072 100644
--- a/src/parser/memory_mapped_input_buffer.h
+++ b/src/parser/memory_mapped_input_buffer.h
@@ -11,16 +11,19 @@
  ** ANTLR input buffer from a memory-mapped file.
  **/
 
-#ifndef MEMORY_MAPPED_INPUT_BUFFER_H_
-#define MEMORY_MAPPED_INPUT_BUFFER_H_
+#ifndef __CVC4__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H
+#define __CVC4__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H
+
+#include <cstdio>
+#include <cerrno>
 
 #include <fcntl.h>
-#include <stdio.h>
 #include <stdint.h>
+#include <string.h>
 
-#include <sys/errno.h>
 #include <sys/mman.h>
 #include <sys/stat.h>
+
 #include <antlr/InputBuffer.hpp>
 
 #include "util/Assert.h"
@@ -33,32 +36,34 @@ class MemoryMappedInputBuffer : public antlr::InputBuffer {
 
 public:
   MemoryMappedInputBuffer(const std::string& filename) {
-    errno = 0;
     struct stat st;
     if( stat(filename.c_str(), &st) == -1 ) {
-      throw Exception("unable to stat() file");
-//      throw Exception( "unable to stat() file " << filename << " errno " << errno );
+      char buf[80];
+      const char* errMsg = strerror_r(errno, buf, sizeof(buf));
+      throw Exception("unable to stat() file `" + filename + "': " + errMsg);
     }
     d_size = st.st_size;
 
     int fd = open(filename.c_str(), O_RDONLY);
     if( fd == -1 ) {
-      throw Exception("unable to fopen() file");
+      char buf[80];
+      const char* errMsg = strerror_r(errno, buf, sizeof(buf));
+      throw Exception("unable to fopen() file `" + filename + "': " + errMsg);
     }
 
     d_start = static_cast< const char * >(
         mmap( 0, d_size, PROT_READ, MAP_FILE | MAP_PRIVATE, fd, 0 ) );
-    errno = 0;
     if( intptr_t( d_start ) == -1 ) {
-      throw Exception("unable to mmap() file");
-//         throw Exception( "unable to mmap() file " << filename << " errno " << errno );
+      char buf[80];
+      const char* errMsg = strerror_r(errno, buf, sizeof(buf));
+      throw Exception("unable to mmap() file `" + filename + "': " + errMsg);
     }
     d_cur = d_start;
     d_end = d_start + d_size;
   }
 
   ~MemoryMappedInputBuffer() {
-    munmap((void*)d_start,d_size);
+    munmap((void*) d_start, d_size);
   }
 
   inline int getChar() {
@@ -71,8 +76,7 @@ private:
   const char *d_start, *d_end, *d_cur;
 };
 
-}
-}
-
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
 
-#endif /* MEMORY_MAPPED_INPUT_BUFFER_H_ */
+#endif /* __CVC4__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H */
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 852eda595..a129d97ee 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -18,12 +18,12 @@
 #include <antlr/CharScanner.hpp>
 #include <antlr/CharBuffer.hpp>
 
-#include "parser.h"
-#include "memory_mapped_input_buffer.h"
+#include "parser/parser.h"
+#include "parser/memory_mapped_input_buffer.h"
 #include "expr/command.h"
 #include "util/output.h"
 #include "util/Assert.h"
-#include "parser_exception.h"
+#include "parser/parser_exception.h"
 #include "parser/antlr_parser.h"
 #include "parser/smt/generated/AntlrSmtParser.hpp"
 #include "parser/smt/generated/AntlrSmtLexer.hpp"
@@ -125,7 +125,7 @@ Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang,
 
 Parser* Parser::getMemoryMappedParser(ExprManager* em, InputLanguage lang, string filename) {
   MemoryMappedInputBuffer* inputBuffer = new MemoryMappedInputBuffer(filename);
-  return getNewParser(em,lang,inputBuffer,filename);
+  return getNewParser(em, lang, inputBuffer, filename);
 }
 
 Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang,
diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h
index e30398824..f0ddc6a7f 100644
--- a/src/parser/parser_exception.h
+++ b/src/parser/parser_exception.h
@@ -24,14 +24,14 @@
 namespace CVC4 {
 namespace parser {
 
-class CVC4_PUBLIC ParserException: public Exception {
+class CVC4_PUBLIC ParserException : public Exception {
 public:
   // Constructors
   ParserException() { }
   ParserException(const std::string& msg): Exception(msg) { }
   ParserException(const char* msg): Exception(msg) { }
   // Destructor
-  virtual ~ParserException() { }
+  virtual ~ParserException() throw() {}
   virtual std::string toString() const {
     return "Parse Error: " + d_msg;
   }
diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h
index 5838790a8..4ab2fb521 100644
--- a/src/parser/symbol_table.h
+++ b/src/parser/symbol_table.h
@@ -35,7 +35,7 @@ struct StringHashFcn {
 /**
  * Generic symbol table for looking up variables by name.
  */
-template<typename ObjectType>
+template <class ObjectType>
 class SymbolTable {
 
 private:
@@ -85,7 +85,7 @@ public:
   ObjectType getObject(const std::string& name) throw () {
     table_iterator find = d_nameBindings.find(name);
     Assert(find != d_nameBindings.end());
-    return find->second /*.top()*/ ;
+    return find->second; /*.top()*/
   }
 
   /**
diff --git a/src/prop/cnf_conversion.h b/src/prop/cnf_conversion.h
deleted file mode 100644
index d66e721db..000000000
--- a/src/prop/cnf_conversion.h
+++ /dev/null
@@ -1,51 +0,0 @@
-/*********************                                                        */
-/** cnf_conversion.h
- ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): dejan, mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.
- **
- ** A type for describing possible CNF conversions.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__CNF_CONVERSION_H
-#define __CVC4__CNF_CONVERSION_H
-
-namespace CVC4 {
-
-enum CnfConversion {
-  /** TODO: explanation of DIRECT_EXPONENTIAL (is this implemented?) */
-  CNF_DIRECT_EXPONENTIAL = 0,
-  /** Explanation of CNF_VAR_INTRODUCTION */
-  CNF_VAR_INTRODUCTION = 1
-};
-
-inline std::ostream& operator<<(std::ostream&, CVC4::CnfConversion) CVC4_PUBLIC;
-
-inline std::ostream& operator<<(std::ostream& out, CVC4::CnfConversion c) {
-  using namespace CVC4;
-
-  switch(c) {
-  case CNF_DIRECT_EXPONENTIAL:
-    out << "CNF_DIRECT_EXPONENTIAL";
-    break;
-  case CNF_VAR_INTRODUCTION:
-    out << "CNF_VAR_INTRODUCTION";
-    break;
-  default:
-    out << "UNKNOWN-CONVERTER!" << int(c);
-  }
-
-  return out;
-}
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__CNF_CONVERSION_H */
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 6e3b6ae2f..612b00bcf 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -320,21 +320,21 @@ SatLiteral TseitinCnfStream::toCNF(const TNode& node) {
 void TseitinCnfStream::convertAndAssert(const TNode& node) {
   Debug("cnf") << "convertAndAssert(" << node << ")" << endl;
   // If the node is a conjuntion, we handle each conjunct separatelu
-  if (node.getKind() == AND) {
+  if(node.getKind() == AND) {
     TNode::const_iterator conjunct = node.begin();
     TNode::const_iterator node_end = node.end();
-    while (conjunct != node_end) {
+    while(conjunct != node_end) {
       convertAndAssert(*conjunct);
       ++ conjunct;
     }
     return;
   }
   // If the node is a disjunction, we construct a clause and assert it
-  if (node.getKind() == OR) {
+  if(node.getKind() == OR) {
     int nChildren = node.getNumChildren();
     SatClause clause(nChildren);
     TNode::const_iterator disjunct = node.begin();
-    for (int i = 0; i < nChildren; ++ disjunct, ++ i) {
+    for(int i = 0; i < nChildren; ++ disjunct, ++ i) {
       clause[i] = toCNF(*disjunct);
     }
     assertClause(clause);
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c45314a55..8def3e279 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -25,8 +25,45 @@ using CVC4::context::Context;
 
 namespace CVC4 {
 
+namespace smt {
+
+/**
+ * This is an inelegant solution, but for the present, it will work.
+ * The point of this is to separate the public and private portions of
+ * the SmtEngine class, so that smt_engine.h doesn't
+ * #include "expr/node.h", which is a private CVC4 header (and can lead
+ * to linking errors due to the improper inlining of non-visible symbols
+ * into user code!).
+ *
+ * The "real" solution (that which is usually implemented) is to move
+ * ALL the implementation to SmtEnginePrivate and maintain a
+ * heap-allocated instance of it in SmtEngine.  SmtEngine (the public
+ * one) becomes an "interface shell" which simply acts as a forwarder
+ * of method calls.
+ */
+class SmtEnginePrivate {
+public:
+
+  /**
+   * Pre-process an Node.  This is expected to be highly-variable,
+   * with a lot of "source-level configurability" to add multiple
+   * passes over the Node.  TODO: may need to specify a LEVEL of
+   * preprocessing (certain contexts need more/less ?).
+   */
+  static Node preprocess(SmtEngine& smt, TNode node);
+
+  /**
+   * Adds a formula to the current context.
+   */
+  static void addFormula(SmtEngine& smt, TNode node);
+};/* class SmtEnginePrivate */
+
+}/* namespace CVC4::smt */
+
+using ::CVC4::smt::SmtEnginePrivate;
+
 SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () :
-  d_ctxt(new Context),
+  d_ctxt(em->getContext()),
   d_exprManager(em),
   d_nodeManager(em->getNodeManager()),
   d_options(opts) {
@@ -37,10 +74,10 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () :
 }
 
 SmtEngine::~SmtEngine() {
+  NodeManagerScope nms(d_nodeManager);
   delete d_propEngine;
   delete d_theoryEngine;
   delete d_decisionEngine;
-  delete d_ctxt;
 }
 
 void SmtEngine::doCommand(Command* c) {
@@ -48,7 +85,7 @@ void SmtEngine::doCommand(Command* c) {
   c->invoke(this);
 }
 
-Node SmtEngine::preprocess(TNode e) {
+Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode e) {
   return e;
 }
 
@@ -62,15 +99,15 @@ Result SmtEngine::quickCheck() {
   return Result(Result::VALIDITY_UNKNOWN);
 }
 
-void SmtEngine::addFormula(TNode e) {
+void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode e) {
   Debug("smt") << "push_back assertion " << e << std::endl;
-  d_propEngine->assertFormula(preprocess(e));
+  smt.d_propEngine->assertFormula(SmtEnginePrivate::preprocess(smt, e));
 }
 
 Result SmtEngine::checkSat(const BoolExpr& e) {
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT checkSat(" << e << ")" << std::endl;
-  addFormula(e.getNode());
+  SmtEnginePrivate::addFormula(*this, e.getNode());
   Result r = check().asSatisfiabilityResult();
   Debug("smt") << "SMT checkSat(" << e << ") ==> " << r << std::endl;
   return r;
@@ -79,7 +116,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
 Result SmtEngine::query(const BoolExpr& e) {
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT query(" << e << ")" << std::endl;
-  addFormula(e.getNode().notNode());
+  SmtEnginePrivate::addFormula(*this, e.getNode().notNode());
   Result r = check().asValidityResult();
   Debug("smt") << "SMT query(" << e << ") ==> " << r << std::endl;
   return r;
@@ -88,7 +125,7 @@ Result SmtEngine::query(const BoolExpr& e) {
 Result SmtEngine::assertFormula(const BoolExpr& e) {
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT assertFormula(" << e << ")" << std::endl;
-  addFormula(e.getNode());
+  SmtEnginePrivate::addFormula(*this, e.getNode());
   return quickCheck().asValidityResult();
 }
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 7495e4100..36cb8746c 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -24,9 +24,6 @@
 #include "util/result.h"
 #include "util/model.h"
 
-// FIXME private header in public code
-#include "expr/node.h"
-
 // In terms of abstraction, this is below (and provides services to)
 // ValidityChecker and above (and requires the services of)
 // PropEngine.
@@ -35,7 +32,7 @@ namespace CVC4 {
 
 namespace context {
   class Context;
-}
+}/* CVC4::context namespace */
 
 class Command;
 class Options;
@@ -44,7 +41,11 @@ class DecisionEngine;
 
 namespace prop {
   class PropEngine;
-}
+}/* CVC4::prop namespace */
+
+namespace smt {
+  class SmtEnginePrivate;
+}/* CVC4::smt namespace */
 
 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
 // hood): use a type parameter and have check() delegate, or subclass
@@ -140,18 +141,9 @@ private:
   /** The propositional engine */
   prop::PropEngine* d_propEngine;
 
-  /**
-   * Pre-process an Node.  This is expected to be highly-variable,
-   * with a lot of "source-level configurability" to add multiple
-   * passes over the Node.  TODO: may need to specify a LEVEL of
-   * preprocessing (certain contexts need more/less ?).
-   */
-  Node preprocess(TNode node);
-
-  /**
-   * Adds a formula to the current context.
-   */
-  void addFormula(TNode node);
+  // preprocess() and addFormula() used to be housed here; they are
+  // now in an SmtEnginePrivate class.  See the comment in
+  // smt_engine.cpp.
 
   /**
    * Full check of consistency in current context.  Returns true iff
@@ -166,6 +158,8 @@ private:
    */
   Result quickCheck();
 
+  friend class ::CVC4::smt::SmtEnginePrivate;
+
 };/* class SmtEngine */
 
 }/* CVC4 namespace */
diff --git a/src/theory/uf/ecdata.h b/src/theory/uf/ecdata.h
index 735712cdc..199b09164 100644
--- a/src/theory/uf/ecdata.h
+++ b/src/theory/uf/ecdata.h
@@ -21,6 +21,7 @@
 
 #include "expr/node.h"
 #include "context/context.h"
+#include "context/cdo.h"
 #include "context/context_mm.h"
 
 namespace CVC4 {
@@ -105,7 +106,6 @@ private:
    */
   ECData* d_find;
 
-
   /**
    * This is pointer back to the node that represents this equivalence class.
    *
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index d432d733f..3753bd78a 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -30,6 +30,7 @@
 #include "theory/theory.h"
 
 #include "context/context.h"
+#include "context/cdlist.h"
 #include "theory/uf/ecdata.h"
 
 namespace CVC4 {
diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp
index 8e2dd9220..f992032ee 100644
--- a/src/util/Assert.cpp
+++ b/src/util/Assert.cpp
@@ -25,6 +25,10 @@ using namespace std;
 
 namespace CVC4 {
 
+#ifdef CVC4_DEBUG
+__thread CVC4_PUBLIC const char* s_debugAssertionFailure = NULL;
+#endif /* CVC4_DEBUG */
+
 void AssertionException::construct(const char* header, const char* extra,
                                    const char* function, const char* file,
                                    unsigned line, const char* fmt,
@@ -65,7 +69,13 @@ void AssertionException::construct(const char* header, const char* extra,
   }
 
   setMessage(string(buf));
+
+#ifdef CVC4_DEBUG
+  // we leak buf[] but only in debug mode with assertions failing
+  s_debugAssertionFailure = buf;
+#else /* CVC4_DEBUG */
   delete [] buf;
+#endif /* CVC4_DEBUG */
 }
 
 void AssertionException::construct(const char* header, const char* extra,
@@ -98,7 +108,13 @@ void AssertionException::construct(const char* header, const char* extra,
   }
 
   setMessage(string(buf));
+
+#ifdef CVC4_DEBUG
+  // we leak buf[] but only in debug mode with assertions failing
+  s_debugAssertionFailure = buf;
+#else /* CVC4_DEBUG */
   delete [] buf;
+#endif /* CVC4_DEBUG */
 }
 
 }/* CVC4 namespace */
diff --git a/src/util/Assert.h b/src/util/Assert.h
index 3b42f2887..8c230218c 100644
--- a/src/util/Assert.h
+++ b/src/util/Assert.h
@@ -19,12 +19,13 @@
 #include <string>
 #include <sstream>
 #include <cstdio>
+#include <cstdlib>
 #include <cstdarg>
-#include "util/exception.h"
-#include "cvc4_config.h"
-#include "config.h"
 
-#include <cassert>
+#include "config.h"
+#include "cvc4_config.h"
+#include "util/exception.h"
+#include "util/output.h"
 
 namespace CVC4 {
 
@@ -192,14 +193,42 @@ public:
   }
 };/* class IllegalArgumentException */
 
-#define AlwaysAssert(cond, msg...) \
-  do { \
-    if(EXPECT_FALSE( ! (cond) )) { \
-      throw AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
-    } \
+#ifdef CVC4_DEBUG
+
+extern __thread CVC4_PUBLIC const char* s_debugAssertionFailure;
+
+// If we're currently handling an exception, print a warning instead;
+// otherwise std::terminate() is called by the runtime and we lose
+// details of the exception
+#define AlwaysAssert(cond, msg...)                                      \
+  do {                                                                  \
+    if(EXPECT_FALSE( ! (cond) )) {                                      \
+      if(EXPECT_FALSE( std::uncaught_exception() )) {                   \
+        Warning() << "===========================================" << std::endl \
+                  << "An assertion failed during stack unwinding:" << std::endl \
+                  << AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) << std::endl \
+                  << "===========================================" << std::endl; \
+        if(s_debugAssertionFailure != NULL) {                                \
+          Warning() << "The propagating exception is:" << std::endl     \
+                    << s_debugAssertionFailure << std::endl                  \
+                    << "===========================================" << std::endl; \
+        }                                                               \
+      } else {                                                          \
+        throw AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
+      }                                                                 \
+    }                                                                   \
   } while(0)
-#define DtorAlwaysAssert(cond, msg...) \
-  assert(EXPECT_TRUE( cond ))
+#else /* CVC4_DEBUG */
+// These simpler (but less useful) versions for non-debug builds fails
+// with terminate() if thrown during stack unwinding.
+#  define AlwaysAssert(cond, msg...)                                    \
+     do {                                                               \
+       if(EXPECT_FALSE( ! (cond) )) {                                   \
+         throw AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
+       }                                                                \
+     } while(0)
+#endif /* CVC4_DEBUG */
+
 #define Unreachable(msg...) \
   throw UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 #define Unhandled(msg...) \
@@ -219,11 +248,9 @@ public:
 
 #ifdef CVC4_ASSERTIONS
 #  define Assert(cond, msg...) AlwaysAssert(cond, ## msg)
-#  define DtorAssert(cond, msg...) assert(EXPECT_TRUE( cond ))
 #  define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ## msg)
 #else /* ! CVC4_ASSERTIONS */
 #  define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/
-#  define DtorAssert(cond, msg...) /*EXPECT_TRUE( cond )*/
 #  define AssertArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/
 #endif /* CVC4_ASSERTIONS */
 
diff --git a/src/util/exception.h b/src/util/exception.h
index b77e7c860..5449d67f7 100644
--- a/src/util/exception.h
+++ b/src/util/exception.h
@@ -31,7 +31,7 @@ public:
   Exception(const std::string& msg) : d_msg(msg) {}
   Exception(const char* msg) : d_msg(msg) {}
   // Destructor
-  virtual ~Exception() {}
+  virtual ~Exception() throw() {}
   // NON-VIRTUAL METHOD for setting and printing the error message
   void setMessage(const std::string& msg) { d_msg = msg; }
   // Printing: feel free to redefine toString().  When inherited,
diff --git a/src/util/options.h b/src/util/options.h
index 676dc0059..b71acd982 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -18,7 +18,6 @@
 
 #include <iostream>
 #include "parser/parser.h"
-#include "prop/cnf_conversion.h"
 
 namespace CVC4 {
 
@@ -42,9 +41,6 @@ struct CVC4_PUBLIC Options {
   /** The input language */
   parser::Parser::InputLanguage lang;
 
-  /** The CNF conversion */
-  CVC4::CnfConversion d_cnfConversion;
-
   /** Should we exit after parsing? */
   bool parseOnly;
 
@@ -61,7 +57,6 @@ struct CVC4_PUBLIC Options {
               err(0),
               verbosity(0),
               lang(parser::Parser::LANG_AUTO),
-              d_cnfConversion(CVC4::CNF_VAR_INTRODUCTION),
               parseOnly(false),
               semanticChecks(true),
               memoryMap(false)
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 8caec4f40..967d6a8c8 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -7,6 +7,7 @@ UNIT_TESTS = \
 	parser/parser_black \
 	context/context_black \
 	context/context_mm_black \
+	context/cdlist_black \
 	theory/theory_black \
 	theory/theory_uf_white \
 	util/assert_white \
diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h
new file mode 100644
index 000000000..560c70722
--- /dev/null
+++ b/test/unit/context/cdlist_black.h
@@ -0,0 +1,72 @@
+/*********************                                                        */
+/** cdlist_black.h
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Black box testing of CVC4::context::CDList<>.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include <vector>
+#include <iostream>
+#include "context/context.h"
+#include "context/cdlist.h"
+
+using namespace std;
+using namespace CVC4::context;
+
+class CDListBlack : public CxxTest::TestSuite {
+private:
+
+  Context* d_context;
+
+public:
+
+  void setUp() {
+    d_context = new Context();
+  }
+
+  // test at different sizes.  this triggers grow() behavior differently.
+  // grow() is completely broken in revision 256; fix forthcoming by Tim
+  void testCDList10() { listTest(10); }
+  void testCDList15() { listTest(15); }
+  void testCDList20() { listTest(20); }
+  void testCDList35() { listTest(35); }
+  void testCDList50() { listTest(50); }
+  void testCDList99() { listTest(99); }
+
+  void listTest(int N) {
+    CDList<int> list(d_context);
+
+    TS_ASSERT(list.empty());
+    for(int i = 0; i < N; ++i) {
+      TS_ASSERT(list.size() == i);
+      list.push_back(i);
+      TS_ASSERT(!list.empty());
+      TS_ASSERT(list.back() == i);
+      int i2 = 0;
+      for(CDList<int>::const_iterator j = list.begin();
+          j != list.end();
+          ++j) {
+        TS_ASSERT(*j == i2++);
+      }
+    }
+    TS_ASSERT(list.size() == N);
+
+    for(int i = 0; i < N; ++i) {
+      TS_ASSERT(list[i] == i);
+    }
+  }
+
+  void tearDown() {
+    delete d_context;
+  }
+};
diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h
index 64ad2d7f7..f06ed9f42 100644
--- a/test/unit/context/context_black.h
+++ b/test/unit/context/context_black.h
@@ -10,17 +10,20 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** Black box testing of CVC4::Node.
+ ** Black box testing of CVC4::context::Context.
  **/
 
 #include <cxxtest/TestSuite.h>
 
-//Used in some of the tests
 #include <vector>
 #include <iostream>
 #include "context/context.h"
+#include "context/cdlist.h"
+#include "context/cdo.h"
+#include "util/Assert.h"
 
 using namespace std;
+using namespace CVC4;
 using namespace CVC4::context;
 
 class ContextBlack : public CxxTest::TestSuite {
@@ -31,7 +34,7 @@ private:
 public:
 
   void setUp() {
-    d_context = new Context();
+    d_context = new Context;
   }
 
   void testIntCDO() {
@@ -53,40 +56,8 @@ public:
     // the interface doesn't declare any exceptions
     d_context->push();
     d_context->pop();
-//    d_context->pop();
-//    d_context->pop();
-  }
-
-  // test at different sizes.  this triggers grow() behavior differently.
-  // grow() is completely broken in revision 256; fix forthcoming by Tim
-  void testCDList10() { listTest(10); }
-  void testCDList15() { listTest(15); }
-  void testCDList20() { listTest(20); }
-  void testCDList35() { listTest(35); }
-  void testCDList50() { listTest(50); }
-  void testCDList99() { listTest(99); }
-
-  void listTest(int N) {
-    CDList<int> list(d_context);
-
-    TS_ASSERT(list.empty());
-    for(int i = 0; i < N; ++i) {
-      TS_ASSERT(list.size() == i);
-      list.push_back(i);
-      TS_ASSERT(!list.empty());
-      TS_ASSERT(list.back() == i);
-      int i2 = 0;
-      for(CDList<int>::const_iterator j = list.begin();
-          j != list.end();
-          ++j) {
-        TS_ASSERT(*j == i2++);
-      }
-    }
-    TS_ASSERT(list.size() == N);
-
-    for(int i = 0; i < N; ++i) {
-      TS_ASSERT(list[i] == i);
-    }
+    TS_ASSERT_THROWS( d_context->pop(), AssertionException );
+    TS_ASSERT_THROWS( d_context->pop(), AssertionException );
   }
 
   void tearDown() {
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index c11d5cf86..96f02c489 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -27,24 +27,28 @@
 
 using namespace CVC4;
 using namespace CVC4::kind;
+using namespace CVC4::context;
 using namespace std;
 
 class NodeBlack : public CxxTest::TestSuite {
 private:
 
-  NodeManager *d_nodeManager;
-  NodeManagerScope *d_scope;
+  Context* d_ctxt;
+  NodeManager* d_nodeManager;
+  NodeManagerScope* d_scope;
 
 public:
 
   void setUp() {
-    d_nodeManager = new NodeManager();
+    d_ctxt = new Context;
+    d_nodeManager = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nodeManager);
   }
 
   void tearDown() {
     delete d_scope;
     delete d_nodeManager;
+    delete d_ctxt;
   }
 
   bool imp(bool a, bool b) const {
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index 871e93dca..ab3c1c842 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -23,29 +23,34 @@
 #include "expr/node_manager.h"
 #include "expr/node.h"
 #include "expr/kind.h"
+#include "context/context.h"
 #include "util/Assert.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
+using namespace CVC4::context;
 using namespace std;
 
 class NodeBuilderBlack : public CxxTest::TestSuite {
 private:
 
-  NodeManagerScope *d_scope;
-  NodeManager *d_nm;
+  Context* d_ctxt;
+  NodeManager* d_nm;
+  NodeManagerScope* d_scope;
 
 public:
 
   void setUp() {
-    d_nm = new NodeManager();
+    d_ctxt = new Context;
+    d_nm = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nm);
     specKind = PLUS;
   }
 
   void tearDown() {
-    delete d_nm;
     delete d_scope;
+    delete d_nm;
+    delete d_ctxt;
   }
 
 
@@ -609,20 +614,37 @@ public:
                                      f,
                                      d_nm->mkNode(AND, q, a)));
 
-    Node assoc1 = (a && b) && c;
-    Node assoc2 = a && (b && c);
-
-    TS_ASSERT_EQUALS(assoc1, d_nm->mkNode(AND, a, b, c));
-    TS_ASSERT_EQUALS(assoc2, d_nm->mkNode(AND, a, d_nm->mkNode(AND, b, c)));
-
-    Node prec1 = (a && b) || c;
-    Node prec2 = a || (b && c);
-    Node prec3 = a && (b || c);
-    Node prec4 = (a || b) && c;
-
-    TS_ASSERT_EQUALS(prec1, d_nm->mkNode(OR, d_nm->mkNode(AND, a, b), c));
-    TS_ASSERT_EQUALS(prec2, d_nm->mkNode(OR, a, d_nm->mkNode(AND, b, c)));
-    TS_ASSERT_EQUALS(prec3, d_nm->mkNode(AND, a, d_nm->mkNode(OR, b, c)));
-    TS_ASSERT_EQUALS(prec4, d_nm->mkNode(AND, d_nm->mkNode(OR, a, b), c));
+    TS_ASSERT_EQUALS(Node((a && b) && c), d_nm->mkNode(AND, a, b, c));
+    TS_ASSERT_EQUALS(Node(a && (b && c)), d_nm->mkNode(AND, a, d_nm->mkNode(AND, b, c)));
+    TS_ASSERT_EQUALS(Node((a || b) || c), d_nm->mkNode(OR, a, b, c));
+    TS_ASSERT_EQUALS(Node(a || (b || c)), d_nm->mkNode(OR, a, d_nm->mkNode(OR, b, c)));
+    TS_ASSERT_EQUALS(Node((a && b) || c), d_nm->mkNode(OR, d_nm->mkNode(AND, a, b), c));
+    TS_ASSERT_EQUALS(Node(a && (b || c)), d_nm->mkNode(AND, a, d_nm->mkNode(OR, b, c)));
+    TS_ASSERT_EQUALS(Node((a || b) && c), d_nm->mkNode(AND, d_nm->mkNode(OR, a, b), c));
+    TS_ASSERT_EQUALS(Node(a || (b && c)), d_nm->mkNode(OR, a, d_nm->mkNode(AND, b, c)));
+
+    TS_ASSERT_EQUALS(Node((a + b) + c), d_nm->mkNode(PLUS, a, b, c));
+    TS_ASSERT_EQUALS(Node(a + (b + c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(PLUS, b, c)));
+    TS_ASSERT_EQUALS(Node((a - b) - c), d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, b), d_nm->mkNode(UMINUS, c)));
+    TS_ASSERT_EQUALS(Node(a - (b - c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, d_nm->mkNode(PLUS, b, d_nm->mkNode(UMINUS, c)))));
+    TS_ASSERT_EQUALS(Node((a * b) * c), d_nm->mkNode(MULT, a, b, c));
+    TS_ASSERT_EQUALS(Node(a * (b * c)), d_nm->mkNode(MULT, a, d_nm->mkNode(MULT, b, c)));
+    TS_ASSERT_EQUALS(Node((a + b) - c), d_nm->mkNode(PLUS, a, b, d_nm->mkNode(UMINUS, c)));
+    TS_ASSERT_EQUALS(Node(a + (b - c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(PLUS, b, d_nm->mkNode(UMINUS, c))));
+    TS_ASSERT_EQUALS(Node((a - b) + c), d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, b), c));
+    TS_ASSERT_EQUALS(Node(a - (b + c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, d_nm->mkNode(PLUS, b, c))));
+    TS_ASSERT_EQUALS(Node((a + b) * c), d_nm->mkNode(MULT, d_nm->mkNode(PLUS, a, b), c));
+    TS_ASSERT_EQUALS(Node(a + (b * c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(MULT, b, c)));
+    TS_ASSERT_EQUALS(Node((a - b) * c), d_nm->mkNode(MULT, d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, b)), c));
+    TS_ASSERT_EQUALS(Node(a - (b * c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, d_nm->mkNode(MULT, b, c))));
+    TS_ASSERT_EQUALS(Node((a * b) + c), d_nm->mkNode(PLUS, d_nm->mkNode(MULT, a, b), c));
+    TS_ASSERT_EQUALS(Node(a * (b + c)), d_nm->mkNode(MULT, a, d_nm->mkNode(PLUS, b, c)));
+    TS_ASSERT_EQUALS(Node((a * b) - c), d_nm->mkNode(PLUS, d_nm->mkNode(MULT, a, b), d_nm->mkNode(UMINUS, c)));
+    TS_ASSERT_EQUALS(Node(a * (b - c)), d_nm->mkNode(MULT, a, d_nm->mkNode(PLUS, b, d_nm->mkNode(UMINUS, c))));
+
+    TS_ASSERT_EQUALS(Node(-a), d_nm->mkNode(UMINUS, a));
+    TS_ASSERT_EQUALS(Node(- a - b), d_nm->mkNode(PLUS, d_nm->mkNode(UMINUS, a), d_nm->mkNode(UMINUS, b)));
+    TS_ASSERT_EQUALS(Node(- a + b), d_nm->mkNode(PLUS, d_nm->mkNode(UMINUS, a), b));
+    TS_ASSERT_EQUALS(Node(- a * b), d_nm->mkNode(MULT, d_nm->mkNode(UMINUS, a), b));
   }
 };
diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h
index 871abe232..88ae5253f 100644
--- a/test/unit/expr/node_white.h
+++ b/test/unit/expr/node_white.h
@@ -22,9 +22,12 @@
 #include "expr/node_manager.h"
 #include "expr/node.h"
 #include "expr/attribute.h"
+#include "context/context.h"
+#include "util/Assert.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
+using namespace CVC4::context;
 using namespace CVC4::expr;
 using namespace CVC4::expr::attr;
 using namespace std;
@@ -41,39 +44,33 @@ typedef Attribute<Test2, std::string> TestStringAttr2;
 // it would be nice to have CDAttribute<> for context-dependence
 typedef CDAttribute<Test1, bool> TestCDFlag;
 
-struct ecdata;
-struct cleanupfcn {
-  static void cleanup(ecdata* ec) { /* clean up */ }
-};
-
-// ManagedAttribute<> has a cleanup function deleting the value
-typedef ManagedAttribute<Test1, ecdata*, cleanupfcn> TestECDataAttr;
-
 typedef Attribute<Test1, bool> TestFlag1;
 typedef Attribute<Test2, bool> TestFlag2;
 typedef Attribute<Test3, bool> TestFlag3;
 typedef Attribute<Test4, bool> TestFlag4;
 typedef Attribute<Test5, bool> TestFlag5;
 
-struct FooBar {};
-struct Test6;
-typedef Attribute<Test6, FooBar> TestFlag6;
+typedef CDAttribute<Test1, bool> TestFlag1cd;
+typedef CDAttribute<Test2, bool> TestFlag2cd;
 
 class NodeWhite : public CxxTest::TestSuite {
 
-  NodeManagerScope *d_scope;
-  NodeManager *d_nm;
+  Context* d_ctxt;
+  NodeManager* d_nm;
+  NodeManagerScope* d_scope;
 
 public:
 
   void setUp() {
-    d_nm = new NodeManager();
+    d_ctxt = new Context;
+    d_nm = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nm);
   }
 
   void tearDown() {
     delete d_scope;
     delete d_nm;
+    delete d_ctxt;
   }
 
   void testNull() {
@@ -96,16 +93,149 @@ public:
     TS_ASSERT(VarNameAttr::s_id == 0);
     TS_ASSERT(TestStringAttr1::s_id == 1);
     TS_ASSERT(TestStringAttr2::s_id == 2);
-    TS_ASSERT(attr::LastAttributeId<string>::s_id == 3);
+    TS_ASSERT((attr::LastAttributeId<string, false>::s_id == 3));
 
     TS_ASSERT(TypeAttr::s_id == 0);
-    TS_ASSERT(attr::LastAttributeId<void*>::s_id == 1);
+    TS_ASSERT((attr::LastAttributeId<void*, false>::s_id == 1));
 
     TS_ASSERT(TestFlag1::s_id == 0);
     TS_ASSERT(TestFlag2::s_id == 1);
     TS_ASSERT(TestFlag3::s_id == 2);
     TS_ASSERT(TestFlag4::s_id == 3);
     TS_ASSERT(TestFlag5::s_id == 4);
+    TS_ASSERT((attr::LastAttributeId<bool, false>::s_id == 5));
+  
+    TS_ASSERT(TestFlag1cd::s_id == 0);
+    TS_ASSERT(TestFlag2cd::s_id == 1);
+    TS_ASSERT((attr::LastAttributeId<bool, true>::s_id == 2));
+  }
+
+  void testCDAttributes() {
+    AttributeManager& am = d_nm->d_attrManager;
+
+    //Debug.on("boolattr");
+
+    Node a = d_nm->mkVar();
+    Node b = d_nm->mkVar();
+    Node c = d_nm->mkVar();
+
+    Debug("boolattr", "get flag 1 on a (should be F)\n");
+    TS_ASSERT(! a.getAttribute(TestFlag1cd()));
+    Debug("boolattr", "get flag 1 on b (should be F)\n");
+    TS_ASSERT(! b.getAttribute(TestFlag1cd()));
+    Debug("boolattr", "get flag 1 on c (should be F)\n");
+    TS_ASSERT(! c.getAttribute(TestFlag1cd()));
+
+    d_ctxt->push(); // level 1
+
+    // test that all boolean flags are FALSE to start
+    Debug("boolattr", "get flag 1 on a (should be F)\n");
+    TS_ASSERT(! a.getAttribute(TestFlag1cd()));
+    Debug("boolattr", "get flag 1 on b (should be F)\n");
+    TS_ASSERT(! b.getAttribute(TestFlag1cd()));
+    Debug("boolattr", "get flag 1 on c (should be F)\n");
+    TS_ASSERT(! c.getAttribute(TestFlag1cd()));
+
+    // test that they all HAVE the boolean attributes
+    TS_ASSERT(a.hasAttribute(TestFlag1cd()));
+    TS_ASSERT(b.hasAttribute(TestFlag1cd()));
+    TS_ASSERT(c.hasAttribute(TestFlag1cd()));
+
+    // test two-arg version of hasAttribute()
+    bool bb;
+    Debug("boolattr", "get flag 1 on a (should be F)\n");
+    TS_ASSERT(a.hasAttribute(TestFlag1cd(), bb));
+    TS_ASSERT(! bb);
+    Debug("boolattr", "get flag 1 on b (should be F)\n");
+    TS_ASSERT(b.hasAttribute(TestFlag1cd(), bb));
+    TS_ASSERT(! bb);
+    Debug("boolattr", "get flag 1 on c (should be F)\n");
+    TS_ASSERT(c.hasAttribute(TestFlag1cd(), bb));
+    TS_ASSERT(! bb);
+
+    // setting boolean flags
+    Debug("boolattr", "set flag 1 on a to T\n");
+    a.setAttribute(TestFlag1cd(), true);
+    Debug("boolattr", "set flag 1 on b to F\n");
+    b.setAttribute(TestFlag1cd(), false);
+    Debug("boolattr", "set flag 1 on c to F\n");
+    c.setAttribute(TestFlag1cd(), false);
+
+    Debug("boolattr", "get flag 1 on a (should be T)\n");
+    TS_ASSERT(a.getAttribute(TestFlag1cd()));
+    Debug("boolattr", "get flag 1 on b (should be F)\n");
+    TS_ASSERT(! b.getAttribute(TestFlag1cd()));
+    Debug("boolattr", "get flag 1 on c (should be F)\n");
+    TS_ASSERT(! c.getAttribute(TestFlag1cd()));
+
+    d_ctxt->push(); // level 2
+
+    Debug("boolattr", "get flag 1 on a (should be T)\n");
+    TS_ASSERT(a.getAttribute(TestFlag1cd()));
+    Debug("boolattr", "get flag 1 on b (should be F)\n");
+    TS_ASSERT(! b.getAttribute(TestFlag1cd()));
+    Debug("boolattr", "get flag 1 on c (should be F)\n");
+    TS_ASSERT(! c.getAttribute(TestFlag1cd()));
+
+    Debug("boolattr", "set flag 1 on a to F\n");
+    a.setAttribute(TestFlag1cd(), false);
+    Debug("boolattr", "set flag 1 on b to T\n");
+    b.setAttribute(TestFlag1cd(), true);
+
+    Debug("boolattr", "get flag 1 on a (should be F)\n");
+    TS_ASSERT(! a.getAttribute(TestFlag1cd()));
+    Debug("boolattr", "get flag 1 on b (should be T)\n");
+    TS_ASSERT(b.getAttribute(TestFlag1cd()));
+    Debug("boolattr", "get flag 1 on c (should be F)\n");
+    TS_ASSERT(! c.getAttribute(TestFlag1cd()));
+
+    d_ctxt->push(); // level 3
+
+    Debug("boolattr", "get flag 1 on a (should be F)\n");
+    TS_ASSERT(! a.getAttribute(TestFlag1cd()));
+    Debug("boolattr", "get flag 1 on b (should be T)\n");
+    TS_ASSERT(b.getAttribute(TestFlag1cd()));
+    Debug("boolattr", "get flag 1 on c (should be F)\n");
+    TS_ASSERT(! c.getAttribute(TestFlag1cd()));
+
+    Debug("boolattr", "set flag 1 on c to T\n");
+    c.setAttribute(TestFlag1cd(), true);
+
+    Debug("boolattr", "get flag 1 on a (should be F)\n");
+    TS_ASSERT(! a.getAttribute(TestFlag1cd()));
+    Debug("boolattr", "get flag 1 on b (should be T)\n");
+    TS_ASSERT(b.getAttribute(TestFlag1cd()));
+    Debug("boolattr", "get flag 1 on c (should be T)\n");
+    TS_ASSERT(c.getAttribute(TestFlag1cd()));
+
+    d_ctxt->pop(); // level 2
+
+    Debug("boolattr", "get flag 1 on a (should be F)\n");
+    TS_ASSERT(! a.getAttribute(TestFlag1cd()));
+    Debug("boolattr", "get flag 1 on b (should be T)\n");
+    TS_ASSERT(b.getAttribute(TestFlag1cd()));
+    Debug("boolattr", "get flag 1 on c (should be F)\n");
+    TS_ASSERT(! c.getAttribute(TestFlag1cd()));
+
+    d_ctxt->pop(); // level 1
+
+    Debug("boolattr", "get flag 1 on a (should be T)\n");
+    TS_ASSERT(a.getAttribute(TestFlag1cd()));
+    Debug("boolattr", "get flag 1 on b (should be F)\n");
+    TS_ASSERT(! b.getAttribute(TestFlag1cd()));
+    Debug("boolattr", "get flag 1 on c (should be F)\n");
+    TS_ASSERT(! c.getAttribute(TestFlag1cd()));
+
+    d_ctxt->pop(); // level 0
+
+    Debug("boolattr", "get flag 1 on a (should be F)\n");
+    TS_ASSERT(! a.getAttribute(TestFlag1cd()));
+    Debug("boolattr", "get flag 1 on b (should be F)\n");
+    TS_ASSERT(! b.getAttribute(TestFlag1cd()));
+    Debug("boolattr", "get flag 1 on c (should be F)\n");
+    TS_ASSERT(! c.getAttribute(TestFlag1cd()));
+
+    TS_ASSERT_THROWS( d_ctxt->pop(), AssertionException );
   }
 
   void testAttributes() {
@@ -169,49 +299,29 @@ public:
     TS_ASSERT(! unnamed.getAttribute(TestFlag5()));
 
     // test that they all HAVE the boolean attributes
-    Debug("boolattr", "get flag 1 on a (should be F)\n");
     TS_ASSERT(a.hasAttribute(TestFlag1()));
-    Debug("boolattr", "get flag 1 on b (should be F)\n");
     TS_ASSERT(b.hasAttribute(TestFlag1()));
-    Debug("boolattr", "get flag 1 on c (should be F)\n");
     TS_ASSERT(c.hasAttribute(TestFlag1()));
-    Debug("boolattr", "get flag 1 on unnamed (should be F)\n");
     TS_ASSERT(unnamed.hasAttribute(TestFlag1()));
 
-    Debug("boolattr", "get flag 2 on a (should be F)\n");
     TS_ASSERT(a.hasAttribute(TestFlag2()));
-    Debug("boolattr", "get flag 2 on b (should be F)\n");
     TS_ASSERT(b.hasAttribute(TestFlag2()));
-    Debug("boolattr", "get flag 2 on c (should be F)\n");
     TS_ASSERT(c.hasAttribute(TestFlag2()));
-    Debug("boolattr", "get flag 2 on unnamed (should be F)\n");
     TS_ASSERT(unnamed.hasAttribute(TestFlag2()));
 
-    Debug("boolattr", "get flag 3 on a (should be F)\n");
     TS_ASSERT(a.hasAttribute(TestFlag3()));
-    Debug("boolattr", "get flag 3 on b (should be F)\n");
     TS_ASSERT(b.hasAttribute(TestFlag3()));
-    Debug("boolattr", "get flag 3 on c (should be F)\n");
     TS_ASSERT(c.hasAttribute(TestFlag3()));
-    Debug("boolattr", "get flag 3 on unnamed (should be F)\n");
     TS_ASSERT(unnamed.hasAttribute(TestFlag3()));
 
-    Debug("boolattr", "get flag 4 on a (should be F)\n");
     TS_ASSERT(a.hasAttribute(TestFlag4()));
-    Debug("boolattr", "get flag 4 on b (should be F)\n");
     TS_ASSERT(b.hasAttribute(TestFlag4()));
-    Debug("boolattr", "get flag 4 on c (should be F)\n");
     TS_ASSERT(c.hasAttribute(TestFlag4()));
-    Debug("boolattr", "get flag 4 on unnamed (should be F)\n");
     TS_ASSERT(unnamed.hasAttribute(TestFlag4()));
 
-    Debug("boolattr", "get flag 5 on a (should be F)\n");
     TS_ASSERT(a.hasAttribute(TestFlag5()));
-    Debug("boolattr", "get flag 5 on b (should be F)\n");
     TS_ASSERT(b.hasAttribute(TestFlag5()));
-    Debug("boolattr", "get flag 5 on c (should be F)\n");
     TS_ASSERT(c.hasAttribute(TestFlag5()));
-    Debug("boolattr", "get flag 5 on unnamed (should be F)\n");
     TS_ASSERT(unnamed.hasAttribute(TestFlag5()));
 
     // test two-arg version of hasAttribute()
@@ -465,6 +575,5 @@ public:
     TS_ASSERT(unnamed.getAttribute(VarNameAttr()) == "");
 
     TS_ASSERT(! unnamed.hasAttribute(VarNameAttr()));
-
   }
 };
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 17fefd07b..908ab81fc 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -87,8 +87,9 @@ public:
   set<Node> d_registered;
   vector<Node> d_getSequence;
 
-  DummyTheory(context::Context* ctxt, OutputChannel& out) :
-    TheoryImpl<DummyTheory>(ctxt, out) {}
+  DummyTheory(Context* ctxt, OutputChannel& out) :
+    TheoryImpl<DummyTheory>(ctxt, out) {
+  }
 
   void registerTerm(TNode n) {
     // check that we registerTerm() a term only once
@@ -125,13 +126,12 @@ public:
 
 class TheoryBlack : public CxxTest::TestSuite {
 
-  NodeManagerScope *d_scope;
-  NodeManager *d_nm;
+  Context* d_ctxt;
+  NodeManager* d_nm;
+  NodeManagerScope* d_scope;
 
   TestOutputChannel d_outputChannel;
 
-  Context* d_context;
-
   DummyTheory* d_dummy;
 
   Node atom0;
@@ -139,28 +139,23 @@ class TheoryBlack : public CxxTest::TestSuite {
 
 public:
 
-  TheoryBlack() {}
-
   void setUp() {
-    d_nm = new NodeManager();
-
+    d_ctxt = new Context;
+    d_nm = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nm);
-
-    d_context = new Context();
-
-    d_dummy = new DummyTheory(d_context, d_outputChannel);
-
+    d_dummy = new DummyTheory(d_ctxt, d_outputChannel);
     d_outputChannel.clear();
-
     atom0 = d_nm->mkNode(kind::TRUE);
     atom1 = d_nm->mkNode(kind::FALSE);
   }
 
   void tearDown() {
+    atom1 = Node::null();
+    atom0 = Node::null();
     delete d_dummy;
-    delete d_context;
     delete d_scope;
     delete d_nm;
+    delete d_ctxt;
   }
 
   void testEffort(){
diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h
index fe2c8d821..86266e923 100644
--- a/test/unit/theory/theory_uf_white.h
+++ b/test/unit/theory/theory_uf_white.h
@@ -36,10 +36,10 @@ using namespace std;
  * Very basic OutputChannel for testing simple Theory Behaviour.
  * Stores a call sequence for the output channel
  */
-enum OutputChannelCallType{CONFLICT, PROPOGATE, LEMMA, EXPLANATION};
+enum OutputChannelCallType { CONFLICT, PROPOGATE, LEMMA, EXPLANATION };
 class TestOutputChannel : public OutputChannel {
 private:
-  void push(OutputChannelCallType call, TNode n){
+  void push(OutputChannelCallType call, TNode n) {
     d_callHistory.push_back(make_pair(call,n));
   }
 public:
@@ -51,71 +51,71 @@ public:
 
   void safePoint() throw(Interrupted) {}
 
-  void conflict(TNode n, bool safe = false) throw(Interrupted){
+  void conflict(TNode n, bool safe = false) throw(Interrupted) {
     push(CONFLICT, n);
   }
 
-  void propagate(TNode n, bool safe = false) throw(Interrupted){
+  void propagate(TNode n, bool safe = false) throw(Interrupted) {
     push(PROPOGATE, n);
   }
 
-  void lemma(TNode n, bool safe = false) throw(Interrupted){
+  void lemma(TNode n, bool safe = false) throw(Interrupted) {
     push(LEMMA, n);
   }
-  void explanation(TNode n, bool safe = false) throw(Interrupted){
+  void explanation(TNode n, bool safe = false) throw(Interrupted) {
     push(EXPLANATION, n);
   }
 
-  void clear(){
+  void clear() {
     d_callHistory.clear();
   }
-  Node getIthNode(int i){
+
+  Node getIthNode(int i) {
     Node tmp = (d_callHistory[i]).second;
     return tmp;
   }
 
-  OutputChannelCallType getIthCallType(int i){
+  OutputChannelCallType getIthCallType(int i) {
     return (d_callHistory[i]).first;
   }
 
-  unsigned getNumCalls(){
+  unsigned getNumCalls() {
     return d_callHistory.size();
   }
 };
 
 class TheoryUFWhite : public CxxTest::TestSuite {
 
-  NodeManagerScope *d_scope;
-  NodeManager *d_nm;
+  Context* d_ctxt;
+  NodeManager* d_nm;
+  NodeManagerScope* d_scope;
 
   TestOutputChannel d_outputChannel;
-  Theory::Effort level;
+  Theory::Effort d_level;
 
-  Context* d_context;
   TheoryUF* d_euf;
 
 public:
 
-  TheoryUFWhite(): level(Theory::FULL_EFFORT) { }
+  TheoryUFWhite() : d_level(Theory::FULL_EFFORT) {}
 
   void setUp() {
-    d_nm = new NodeManager();
+    d_ctxt = new Context;
+    d_nm = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nm);
-
-    d_context = new Context();
-
     d_outputChannel.clear();
-    d_euf = new TheoryUF(d_context, d_outputChannel);
+    d_euf = new TheoryUF(d_ctxt, d_outputChannel);
   }
 
   void tearDown() {
     delete d_euf;
-    delete d_context;
+    d_outputChannel.clear();
     delete d_scope;
     delete d_nm;
+    delete d_ctxt;
   }
 
-  void testPushPopChain(){
+  void testPushPopChain() {
     Node x = d_nm->mkVar();
     Node f = d_nm->mkVar();
     Node f_x = d_nm->mkNode(kind::APPLY, f, x);
@@ -140,26 +140,26 @@ public:
 
     d_euf->assertFact( f3_x_eq_x );
     d_euf->assertFact( f1_x_neq_x );
-    d_euf->check(level);
-    d_context->push();
+    d_euf->check(d_level);
+    d_ctxt->push();
 
     d_euf->assertFact( f5_x_eq_x );
-    d_euf->check(level);
+    d_euf->check(d_level);
 
     TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls());
     TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0));
     Node realConflict = d_outputChannel.getIthNode(0);
     TS_ASSERT_EQUALS(expectedConflict, realConflict);
 
-    d_context->pop();
-    d_euf->check(level);
+    d_ctxt->pop();
+    d_euf->check(d_level);
 
     //Test that no additional calls to the output channel occurred.
     TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls());
 
     d_euf->assertFact( f5_x_eq_x );
 
-    d_euf->check(level);
+    d_euf->check(d_level);
 
     TS_ASSERT_EQUALS(2, d_outputChannel.getNumCalls());
     TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0));
@@ -174,7 +174,7 @@ public:
 
 
   /* test that {f(f(x)) == x, f(f(f(x))) != f(x)} is inconsistent */
-  void testSimpleChain(){
+  void testSimpleChain() {
     Node x = d_nm->mkVar();
     Node f = d_nm->mkVar();
     Node f_x = d_nm->mkNode(kind::APPLY, f, x);
@@ -188,7 +188,7 @@ public:
 
     d_euf->assertFact(f_f_x_eq_x);
     d_euf->assertFact(f_f_f_x_neq_f_x);
-    d_euf->check(level);
+    d_euf->check(d_level);
 
     TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls());
     TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0));
@@ -199,13 +199,13 @@ public:
   }
 
   /* test that !(x == x) is inconsistent */
-  void testSelfInconsistent(){
+  void testSelfInconsistent() {
     Node x = d_nm->mkVar();
     Node x_neq_x = (x.eqNode(x)).notNode();
     Node and_x_neq_x = d_nm->mkNode(kind::AND, x_neq_x);
 
     d_euf->assertFact(x_neq_x);
-    d_euf->check(level);
+    d_euf->check(d_level);
 
     TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls());
     TS_ASSERT_EQUALS(and_x_neq_x, d_outputChannel.getIthNode(0));
@@ -213,12 +213,12 @@ public:
   }
 
   /* test that (x == x) is consistent */
-  void testSelfConsistent(){
+  void testSelfConsistent() {
     Node x = d_nm->mkVar();
     Node x_eq_x = x.eqNode(x);
 
     d_euf->assertFact(x_eq_x);
-    d_euf->check(level);
+    d_euf->check(d_level);
 
     TS_ASSERT_EQUALS(0, d_outputChannel.getNumCalls());
   }
@@ -229,7 +229,7 @@ public:
       f(f(f(f(f(x))))) = x,
       f(x) != x
      } is inconsistent */
-  void testChain(){
+  void testChain() {
     Node x = d_nm->mkVar();
     Node f = d_nm->mkVar();
     Node f_x = d_nm->mkNode(kind::APPLY, f, x);
@@ -251,7 +251,7 @@ public:
     d_euf->assertFact( f3_x_eq_x );
     d_euf->assertFact( f5_x_eq_x );
     d_euf->assertFact( f1_x_neq_x );
-    d_euf->check(level);
+    d_euf->check(d_level);
 
     TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls());
     TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0));
@@ -260,28 +260,28 @@ public:
   }
 
 
-  void testPushPopA(){
+  void testPushPopA() {
     Node x = d_nm->mkVar();
     Node x_eq_x = x.eqNode(x);
 
-    d_context->push();
+    d_ctxt->push();
     d_euf->assertFact( x_eq_x );
-    d_euf->check(level);
-    d_context->pop();
-    d_euf->check(level);
+    d_euf->check(d_level);
+    d_ctxt->pop();
+    d_euf->check(d_level);
   }
 
-  void testPushPopB(){
+  void testPushPopB() {
     Node x = d_nm->mkVar();
     Node f = d_nm->mkVar();
     Node f_x = d_nm->mkNode(kind::APPLY, f, x);
     Node f_x_eq_x = f_x.eqNode(x);
 
     d_euf->assertFact( f_x_eq_x );
-    d_context->push();
-    d_euf->check(level);
-    d_context->pop();
-    d_euf->check(level);
+    d_ctxt->push();
+    d_euf->check(d_level);
+    d_ctxt->pop();
+    d_euf->check(d_level);
   }