From: Morgan Deters <mdeters@gmail.com>
Date: Sun, 4 Apr 2010 19:55:47 +0000 (+0000)
Subject: * Node::isAtomic() now looks at an "atomic" attribute of arguments
X-Git-Tag: cvc5-1.0.0~9139
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=42c58baf0a2a96c1f3bd797d64834d02adfb9a59;p=cvc5.git

* Node::isAtomic() now looks at an "atomic" attribute of arguments
  instead of assuming it's atomic based on kind.  Atomicity is
  determined at node building time.  Fixes bug #81.  If this is
  determined to make node building too slow, we can allocate another
  attribute "AtomicHasBeenComputed" to lazily compute atomicity.

* TheoryImpl<> has gone away.  Theory implementations now derive from
  Theory directly and share a single RegisteredAttr attribute for term
  registration (which shouldn't overlap: every term is "owned" by
  exactly one Theory).  Fixes bug #79.

* Additional atomicity tests in ExprBlack unit test.

* More appropriate whitebox testing for attribute ID assignment
  (AttributeWhite unit test).

* Better (and more correct) assertion checking in NodeBuilderBlack.

* run-regression script now checks exit status against what's provided
  in "% EXIT: " gesture in .cvc input files, and stderr against
  "% EXPECT-ERROR: ".  These can be used to support intended failures.
  Fixes bug #84.  Also add "% EXIT: " gestures to all .cvc regressions
  in repository.

* Solved some "control reaches end of non-void function" warnings in
  src/parser/bounded_token_buffer.cpp by replacing
  "AlwaysAssert(false)" with "Unreachable()" (which is known
  statically to never return normally).

* Regression tests now use the cvc4 binary under
  builds/$(CURRENT_BUILD)/src/main instead of the one in bin/ which
  may not be properly installed yet at that point of the build.
  (Partially fixes bug #46.)

* -fvisibility=hidden is now included by configure.ac instead of each
   Makefile.am, which will make it easier to support platforms
   (e.g. cygwin) that do things a different way.

* TheoryUF code formatting.  (re: my code review bug #64)

* CDMap<> is leaking memory again, pending a fix for bug #85 in the
  context subsystem.  (To avoid serious errors, can't free context
  objects.)

* add ContextWhite unit test for bug #85 (though it's currently
  "defanged," awaiting the bugfix)

* Minor documentation, other cleanup.
---

diff --git a/config/antlr.m4 b/config/antlr.m4
index 64b554378..604d2f6bc 100644
--- a/config/antlr.m4
+++ b/config/antlr.m4
@@ -26,10 +26,11 @@ AC_DEFUN([AC_PROG_ANTLR], [
 
 ##
 # Check the existence of the ANTLR3 C runtime library and headers
-# Will set ANTLR_INCLUDES and ANTLR_LIBS to the location of the ANTLR headers
-# and library respectively
+# Will set ANTLR_INCLUDES and ANTLR_LIBS to the location of the ANTLR
+# headers and library respectively
 ##
 AC_DEFUN([AC_LIB_ANTLR],[
+  AC_ARG_VAR(ANTLR_HOME, [path to libantlr3c installation])
 
   # Get the location of the ANTLR3 C includes and libraries
   AC_ARG_WITH(
diff --git a/configure.ac b/configure.ac
index a80d1fee9..7007ba47f 100644
--- a/configure.ac
+++ b/configure.ac
@@ -480,6 +480,9 @@ CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
 CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated"
 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
 
+FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
+AC_SUBST(FLAG_VISIBILITY_HIDDEN)
+
 # mk_include
 #
 # When automake scans Makefiles, it complains about non-standard make
diff --git a/src/Makefile.am b/src/Makefile.am
index 17c867163..593499c9b 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -15,7 +15,7 @@ LIBCVC4_VERSION = @CVC4_LIBRARY_VERSION@
 AM_CPPFLAGS =
 	-D__BUILDING_CVC4LIB \
 	-I@srcdir@/include -I@srcdir@
-AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
 
 SUBDIRS = expr util context theory prop smt . parser main
 
diff --git a/src/context/Makefile.am b/src/context/Makefile.am
index 54accdd6e..85847e096 100644
--- a/src/context/Makefile.am
+++ b/src/context/Makefile.am
@@ -1,7 +1,7 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
 	-I@srcdir@/../include -I@srcdir@/..
-AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libcontext.la
 
diff --git a/src/context/cdmap.h b/src/context/cdmap.h
index e9ae8337e..d4de88daf 100644
--- a/src/context/cdmap.h
+++ b/src/context/cdmap.h
@@ -191,7 +191,8 @@ class CDMap : public ContextObj {
     for(typename std::vector<Element*>::iterator i = d_trash.begin();
         i != d_trash.end();
         ++i) {
-      (*i)->deleteSelf();
+      Debug("gc") << "emptyTrash(): " << *i << std::endl;
+      //(*i)->deleteSelf();
     }
     d_trash.clear();
   }
diff --git a/src/context/context.h b/src/context/context.h
index 455169a62..0e2a9107f 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -208,12 +208,12 @@ public:
   /**
    * Get the level of the current Scope
    */
-  int getLevel(void) const { return d_level; }
+  int getLevel() const { return d_level; }
 
   /**
    * Return true iff this Scope is the current top Scope
    */
-  bool isCurrent(void) const { return this == d_pContext->getTopScope(); }
+  bool isCurrent() const { return this == d_pContext->getTopScope(); }
 
   /**
    * When a ContextObj object is modified for the first time in this Scope, it
@@ -240,7 +240,7 @@ public:
   static void operator delete(void* pMem) {}
 
   //FIXME:  //! Check for memory leaks
-  //  void check(void);
+  //  void check();
 
 };/* class Scope */
 
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 76f6ef1a4..1f5e403cc 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -1,7 +1,7 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
 	-I@srcdir@/../include -I@srcdir@/..
-AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libexpr.la
 
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 052458cbe..96152d075 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -113,6 +113,9 @@ enum MetaKind_t {
 // individual MetaKind constants under kind::metakind::
 typedef ::CVC4::kind::metakind::MetaKind_t MetaKind;
 
+/**
+ * Get the metakind for a particular kind.
+ */
 static inline MetaKind metaKindOf(Kind k) {
   static const MetaKind metaKinds[] = {
     metakind::INVALID, /* NULL_EXPR */
@@ -123,15 +126,20 @@ ${metakind_kinds}
   return metaKinds[k];
 }/* metaKindOf(k) */
 
-static inline bool kindIsAtomic(Kind k) {
-  static const bool isAtomic[] = {
+/**
+ * Determine if a particular kind can be atomic or not.  Some kinds
+ * are never atomic (OR, NOT, ITE...), some can be atomic depending on
+ * their children (PLUS might have an ITE under it, for instance).
+ */
+static inline bool kindCanBeAtomic(Kind k) {
+  static const bool canBeAtomic[] = {
     false, /* NULL_EXPR */
-${metakind_isatomic}
+${metakind_canbeatomic}
     false /* LAST_KIND */
-  };/* isAtomic[] */
+  };/* canBeAtomic[] */
 
-  return isAtomic[k];
-}/* kindIsAtomic(k) */
+  return canBeAtomic[k];
+}/* kindCanBeAtomic(k) */
 
 }/* CVC4::kind namespace */
 
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 6508f8121..f59388def 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -32,6 +32,23 @@ cat <<EOF
  ** for the CVC4 project.
  **/
 
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+
+/* Edit the template file instead:                     */
+/* $1 */
+
 EOF
 
 me=$(basename "$0")
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 3884f636a..b8dbc2dd6 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -200,11 +200,11 @@ function register_metakind {
   nc=$3
 
   if [ $mk = NONATOMIC_OPERATOR ]; then
-    metakind_isatomic="${metakind_isatomic}    false, /* $k */
+    metakind_canbeatomic="${metakind_canbeatomic}    false, /* $k */
 ";
     mk=OPERATOR
   else
-    metakind_isatomic="${metakind_isatomic}    true, /* $k */
+    metakind_canbeatomic="${metakind_canbeatomic}    true, /* $k */
 ";
   fi
 
@@ -278,7 +278,7 @@ while [ $# -gt 0 ]; do
   metakind_kinds="${metakind_kinds}
     /* from $b */
 "
-  metakind_isatomic="${metakind_isatomic}
+  metakind_canbeatomic="${metakind_canbeatomic}
     /* from $b */
 "
   source "$kf"
@@ -293,7 +293,7 @@ text=$(cat "$template")
 for var in \
     metakind_includes \
     metakind_kinds \
-    metakind_isatomic \
+    metakind_canbeatomic \
     metakind_constantMaps \
     metakind_compares \
     metakind_constHashes \
diff --git a/src/expr/node.h b/src/expr/node.h
index 6f6fdfb4d..3a2aca571 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -587,8 +587,8 @@ template <bool ref_count>
 NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(&expr::NodeValue::s_null);
 
 template <bool ref_count>
-bool NodeTemplate<ref_count>::isAtomic() const {
-  return kind::kindIsAtomic(getKind());
+inline bool NodeTemplate<ref_count>::isAtomic() const {
+  return NodeManager::currentNM()->isAtomic(*this);
 }
 
 // FIXME: escape from type system convenient but is there a better
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 99b1471f9..71242f2e1 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -35,18 +35,15 @@
 
 namespace CVC4 {
 
-class Type;
-
 namespace expr {
-namespace attr {
-
-struct VarName {};
-struct Type {};
 
+// Definition of an attribute for the variable name.
+// TODO: hide this attribute behind a NodeManager interface.
+namespace attr {
+  struct VarNameTag {};
 }/* CVC4::expr::attr namespace */
 
-typedef Attribute<attr::VarName, std::string> VarNameAttr;
-typedef ManagedAttribute<attr::Type, CVC4::Type*, attr::TypeCleanupStrategy> TypeAttr;
+typedef expr::Attribute<attr::VarNameTag, std::string> VarNameAttr;
 
 }/* CVC4::expr namespace */
 
@@ -125,6 +122,44 @@ class NodeManager {
     expr::NodeValue* child[N];
   };/* struct NodeManager::NVStorage<N> */
 
+  // attribute tags
+  struct TypeTag {};
+  struct AtomicTag {};
+
+  // NodeManager's attributes.  These aren't exposed outside of this
+  // class; use the getters.
+  typedef expr::ManagedAttribute<TypeTag,
+                                 CVC4::Type*,
+                                 expr::attr::TypeCleanupStrategy> TypeAttr;
+  typedef expr::Attribute<AtomicTag, bool> AtomicAttr;
+
+  /**
+   * Returns true if this node is atomic (has no more Boolean
+   * structure).  This is the NodeValue version for NodeManager's
+   * internal use.  There's a public version of this function below
+   * that takes a TNode.
+   * @param nv the node to check for atomicity
+   * @return true if atomic
+   */
+  inline bool isAtomic(expr::NodeValue* nv) const {
+    // The kindCanBeAtomic() and metakind checking are just optimizations
+    // (to avoid the hashtable lookup).  We assume that all nodes have
+    // the atomic attribute pre-computed and set at their time of
+    // creation.  This is because:
+    // (1) it's super cheap to do it bottom-up.
+    // (2) if we computed it lazily, we'd need a second attribute to
+    //     tell us whether we had computed it yet or not.
+    // The pre-computation and registration occurs in poolInsert().
+    AssertArgument(nv->getMetaKind() != kind::metakind::INVALID, *nv,
+                   "NodeManager::isAtomic() called on INVALID node (%s)",
+                   kind::kindToString(nv->getKind()).c_str());
+    return
+      nv->getMetaKind() == kind::metakind::VARIABLE ||
+      nv->getMetaKind() == kind::metakind::CONSTANT ||
+      ( kind::kindCanBeAtomic(nv->getKind()) &&
+        getAttribute(nv, AtomicAttr()) );
+  }
+
 public:
 
   NodeManager(context::Context* ctxt);
@@ -324,6 +359,15 @@ public:
    * TODO: Does this call compute the type if it's not already available?
    */
   inline Type* getType(TNode n) const;
+
+  /**
+   * Returns true if this node is atomic (has no more Boolean structure)
+   * @param n the node to check for atomicity
+   * @return true if atomic
+   */
+  inline bool isAtomic(TNode n) const {
+    return isAtomic(n.d_nv);
+  }
 };
 
 /**
@@ -476,7 +520,7 @@ inline Type* NodeManager::mkSort(const std::string& name) const {
 }
 
 inline Type* NodeManager::getType(TNode n) const {
-  return getAttribute(n, CVC4::expr::TypeAttr());
+  return getAttribute(n, TypeAttr());
 }
 
 inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const {
@@ -492,6 +536,39 @@ inline void NodeManager::poolInsert(expr::NodeValue* nv) {
   Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end(),
          "NodeValue already in the pool!");
   d_nodeValuePool.insert(nv);// FIXME multithreading
+
+  switch(nv->getMetaKind()) {
+  case kind::metakind::INVALID:
+  case kind::metakind::VARIABLE:
+  case kind::metakind::CONSTANT:
+    // nothing to do (don't bother setting the attribute, isAtomic()
+    // on VARIABLEs and CONSTANTs is always true)
+    break;
+
+  case kind::metakind::OPERATOR:
+  case kind::metakind::PARAMETERIZED:
+    {
+      // register this NodeValue as atomic or not; use nv_begin/end
+      // because we need to consider the operator too in the case of
+      // PARAMETERIZED-metakinded nodes (i.e. APPLYs); they could have a
+      // buried ITE.
+
+      // assume it's atomic if its kind can be atomic, check children
+      // to see if that is actually true
+      bool atomic = kind::kindCanBeAtomic(nv->getKind());
+      if(atomic) {
+        for(expr::NodeValue::nv_iterator i = nv->nv_begin();
+            i != nv->nv_end();
+            ++i) {
+          if(!(atomic = isAtomic(*i))) {
+            break;
+          }
+        }
+      }
+
+      setAttribute(nv, AtomicAttr(), atomic);
+    }
+  }
 }
 
 inline void NodeManager::poolRemove(expr::NodeValue* nv) {
@@ -569,7 +646,7 @@ inline Node NodeManager::mkVar(Type* type, const std::string& name) {
 inline Node NodeManager::mkVar(Type* type) {
   Node n = mkVar();
   type->inc();// reference-count the type
-  n.setAttribute(expr::TypeAttr(), type);
+  n.setAttribute(TypeAttr(), type);
   return n;
 }
 
diff --git a/src/main/main.cpp b/src/main/main.cpp
index b10103635..819f7695e 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -58,25 +58,25 @@ int main(int argc, char* argv[]) {
     }
     cerr << "CVC4 Error:" << endl << e << endl;
     printf(usage, options.binary_name.c_str());
-    abort();
+    exit(1);
   } catch(Exception& e) {
     if(options.smtcomp_mode) {
       cout << "unknown" << endl;
     }
     cerr << "CVC4 Error:" << endl << e << endl;
-    abort();
+    exit(1);
   } catch(bad_alloc) {
     if(options.smtcomp_mode) {
       cout << "unknown" << endl;
     }
     cerr << "CVC4 ran out of memory." << endl;
-    abort();
+    exit(1);
   } catch(...) {
     if(options.smtcomp_mode) {
       cout << "unknown" << endl;
     }
     cerr << "CVC4 threw an exception of unknown type." << endl;
-    abort();
+    exit(1);
   }
 }
 
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index 1aaf7ab69..dad8059f5 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -15,7 +15,7 @@ LIBCVC4PARSER_VERSION = @CVC4_PARSER_LIBRARY_VERSION@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4PARSERLIB \
 	-I@srcdir@/../include -I@srcdir@/.. $(ANTLR_INCLUDES)
-AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
 
 SUBDIRS = smt cvc
 
diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp
index 1418e8f3c..29006b343 100644
--- a/src/parser/bounded_token_buffer.cpp
+++ b/src/parser/bounded_token_buffer.cpp
@@ -281,13 +281,13 @@ dbgTokLT  (pANTLR3_TOKEN_STREAM ts, ANTLR3_INT32 k)
 static pANTLR3_COMMON_TOKEN
 LB(pANTLR3_COMMON_TOKEN_STREAM cts, ANTLR3_INT32 k)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 
 static pANTLR3_COMMON_TOKEN 
 get (pANTLR3_TOKEN_STREAM ts, ANTLR3_UINT32 i)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 
 static pANTLR3_TOKEN_SOURCE 
@@ -306,19 +306,19 @@ setTokenSource	(   pANTLR3_TOKEN_STREAM ts,
 static pANTLR3_STRING	    
 toString    (pANTLR3_TOKEN_STREAM ts)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 
 static pANTLR3_STRING
 toStringSS(pANTLR3_TOKEN_STREAM ts, ANTLR3_UINT32 start, ANTLR3_UINT32 stop)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 
 static pANTLR3_STRING	    
 toStringTT  (pANTLR3_TOKEN_STREAM ts, pANTLR3_COMMON_TOKEN start, pANTLR3_COMMON_TOKEN stop)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 
 /** Move the input pointer to the next incoming token.  The stream
@@ -395,13 +395,13 @@ discardOffChannel   (pANTLR3_COMMON_TOKEN_STREAM tokenStream, ANTLR3_BOOLEAN dis
 static pANTLR3_VECTOR	    
 getTokens   (pANTLR3_COMMON_TOKEN_STREAM tokenStream)
 {
-    AlwaysAssert(false);
+    Unreachable();
 }
 
 static pANTLR3_LIST	    
 getTokenRange	(pANTLR3_COMMON_TOKEN_STREAM tokenStream, ANTLR3_UINT32 start, ANTLR3_UINT32 stop)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }                                                   
 /** Given a start and stop index, return a List of all tokens in
  *  the token type BitSet.  Return null if no tokens were found.  This
@@ -410,19 +410,19 @@ getTokenRange	(pANTLR3_COMMON_TOKEN_STREAM tokenStream, ANTLR3_UINT32 start, ANT
 static pANTLR3_LIST	    
 getTokensSet	(pANTLR3_COMMON_TOKEN_STREAM tokenStream, ANTLR3_UINT32 start, ANTLR3_UINT32 stop, pANTLR3_BITSET types)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 
 static pANTLR3_LIST	    
 getTokensList	(pANTLR3_COMMON_TOKEN_STREAM tokenStream, ANTLR3_UINT32 start, ANTLR3_UINT32 stop, pANTLR3_LIST list)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 
 static pANTLR3_LIST	    
 getTokensType	(pANTLR3_COMMON_TOKEN_STREAM tokenStream, ANTLR3_UINT32 start, ANTLR3_UINT32 stop, ANTLR3_UINT32 type)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 
 static ANTLR3_UINT32	    
@@ -450,13 +450,13 @@ _LA  (pANTLR3_INT_STREAM is, ANTLR3_INT32 i)
 static ANTLR3_UINT32	    
 dbgLA  (pANTLR3_INT_STREAM is, ANTLR3_INT32 i)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 
 static ANTLR3_MARKER
 mark	(pANTLR3_INT_STREAM is)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 
 /// As per mark() but with a call to tell the debugger we are doing this
@@ -464,7 +464,7 @@ mark	(pANTLR3_INT_STREAM is)
 static ANTLR3_MARKER
 dbgMark	(pANTLR3_INT_STREAM is)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 
 static void		    
@@ -476,7 +476,7 @@ release	(pANTLR3_INT_STREAM is, ANTLR3_MARKER mark)
 static ANTLR3_UINT32	    
 size	(pANTLR3_INT_STREAM is)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 
 static ANTLR3_MARKER   
@@ -496,33 +496,33 @@ tindex	(pANTLR3_INT_STREAM is)
 static void		    
 dbgRewindLast	(pANTLR3_INT_STREAM is)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 static void		    
 rewindLast	(pANTLR3_INT_STREAM is)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 static void		    
 rewindStream	(pANTLR3_INT_STREAM is, ANTLR3_MARKER marker)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 static void		    
 dbgRewindStream	(pANTLR3_INT_STREAM is, ANTLR3_MARKER marker)
 {
-   AlwaysAssert(false);
+   Unreachable();
 }
 
 static void		    
 seek	(pANTLR3_INT_STREAM is, ANTLR3_MARKER index)
 {
-    AlwaysAssert(false);
+    Unreachable();
 }
 static void		    
 dbgSeek	(pANTLR3_INT_STREAM is, ANTLR3_MARKER index)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 
 static pANTLR3_COMMON_TOKEN nextToken(pBOUNDED_TOKEN_BUFFER buffer) {
diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am
index ade8d83e7..08e6c4d52 100644
--- a/src/parser/cvc/Makefile.am
+++ b/src/parser/cvc/Makefile.am
@@ -1,7 +1,7 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4PARSERLIB \
 	-I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES)
-AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
 
 # Compile generated C files using C++ compiler
 CC=$(CXX)
diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am
index f081f493f..3ffe61b05 100644
--- a/src/parser/smt/Makefile.am
+++ b/src/parser/smt/Makefile.am
@@ -1,7 +1,7 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4PARSERLIB \
 	-I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES)
-AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
 
 # Compile generated C files using C++ compiler
 AM_CFLAGS = $(AM_CXXFLAGS)
diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am
index fc0697eda..357818b32 100644
--- a/src/prop/Makefile.am
+++ b/src/prop/Makefile.am
@@ -1,7 +1,7 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
 	-I@srcdir@/../include -I@srcdir@/..
-AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libprop.la
 
diff --git a/src/prop/minisat/Makefile.am b/src/prop/minisat/Makefile.am
index 366cc34c8..d68237d9b 100644
--- a/src/prop/minisat/Makefile.am
+++ b/src/prop/minisat/Makefile.am
@@ -1,7 +1,7 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
 	-I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../.. -I@srcdir@/../../include
-AM_CXXFLAGS = -Wall -fvisibility=hidden -DNDEBUG
+AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) -DNDEBUG
 
 noinst_LTLIBRARIES = libminisat.la
 libminisat_la_SOURCES = \
diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index a2da2c949..889385d77 100644
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -1,7 +1,7 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
 	-I@srcdir@/../include -I@srcdir@/..
-AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libsmt.la
 
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index 2891e64cf..6b1854bfc 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -1,7 +1,7 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
 	-I@srcdir@/../include -I@srcdir@/..
-AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libtheory.la
 
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index 226d5af12..cb838f497 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -1,12 +1,11 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
 	-I@srcdir@/../../include -I@srcdir@/../..
-AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libarith.la
 
 libarith_la_SOURCES = \
-	theory_def.h \
 	theory_arith.h
 
 EXTRA_DIST = kinds
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 973651f7a..d211cd37d 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -25,10 +25,10 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-class TheoryArith : public TheoryImpl<TheoryArith> {
+class TheoryArith : public Theory {
 public:
   TheoryArith(context::Context* c, OutputChannel& out) :
-    TheoryImpl<TheoryArith>(c, out) {
+    Theory(c, out) {
   }
 
   void preRegisterTerm(TNode n) { Unimplemented(); }
diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am
index af3a28b3b..5d3514dda 100644
--- a/src/theory/arrays/Makefile.am
+++ b/src/theory/arrays/Makefile.am
@@ -1,12 +1,11 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
 	-I@srcdir@/../../include -I@srcdir@/../..
-AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libarrays.la
 
 libarrays_la_SOURCES = \
-	theory_def.h \
 	theory_arrays.h
 
 EXTRA_DIST = kinds
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index ec3b88ccd..2f62aacd7 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -25,10 +25,10 @@ namespace CVC4 {
 namespace theory {
 namespace arrays {
 
-class TheoryArrays : public TheoryImpl<TheoryArrays> {
+class TheoryArrays : public Theory {
 public:
   TheoryArrays(context::Context* c, OutputChannel& out) :
-    TheoryImpl<TheoryArrays>(c, out) {
+    Theory(c, out) {
   }
 
   void preRegisterTerm(TNode n) { Unimplemented(); }
diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am
index cbdf13add..690299630 100644
--- a/src/theory/booleans/Makefile.am
+++ b/src/theory/booleans/Makefile.am
@@ -1,12 +1,11 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
 	-I@srcdir@/../../include -I@srcdir@/../..
-AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libbooleans.la
 
 libbooleans_la_SOURCES = \
-	theory_def.h \
 	theory_bool.h
 
 EXTRA_DIST = kinds
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index 5196bb018..eb6e84c39 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -25,10 +25,10 @@ namespace CVC4 {
 namespace theory {
 namespace booleans {
 
-class TheoryBool : public TheoryImpl<TheoryBool> {
+class TheoryBool : public Theory {
 public:
   TheoryBool(context::Context* c, OutputChannel& out) :
-    TheoryImpl<TheoryBool>(c, out) {
+    Theory(c, out) {
   }
 
   void preRegisterTerm(TNode n) { Unimplemented(); }
diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am
index 54622bf9a..d90472fd3 100644
--- a/src/theory/bv/Makefile.am
+++ b/src/theory/bv/Makefile.am
@@ -1,12 +1,11 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
 	-I@srcdir@/../../include -I@srcdir@/../..
-AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libbv.la
 
 libbv_la_SOURCES = \
-	theory_def.h \
 	theory_bv.h
 
 EXTRA_DIST = kinds
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index fbb62545d..a859291a7 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -25,10 +25,10 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-class TheoryBV : public TheoryImpl<TheoryBV> {
+class TheoryBV : public Theory {
 public:
   TheoryBV(context::Context* c, OutputChannel& out) :
-    TheoryImpl<TheoryBV>(c, out) {
+    Theory(c, out) {
   }
 
   void preRegisterTerm(TNode n) { Unimplemented(); }
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 17a35f2ed..d4bd717be 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -23,5 +23,82 @@ using namespace std;
 namespace CVC4 {
 namespace theory {
 
+Node Theory::get() {
+  Assert( !d_facts.empty(),
+          "Theory::get() called with assertion queue empty!" );
+
+  Node fact = d_facts.front();
+  d_facts.pop_front();
+
+  Debug("theory") << "Theory::get() => " << fact
+                  << "(" << d_facts.size() << " left)" << std::endl;
+
+  if(! fact.getAttribute(RegisteredAttr())) {
+    std::list<TNode> toReg;
+    toReg.push_back(fact);
+
+    Debug("theory") << "Theory::get(): registering new atom" << std::endl;
+
+    /* Essentially this is doing a breadth-first numbering of
+     * non-registered subterms with children.  Any non-registered
+     * leaves are immediately registered. */
+    for(std::list<TNode>::iterator workp = toReg.begin();
+        workp != toReg.end();
+        ++workp) {
+
+      TNode n = *workp;
+
+      if(n.hasOperator()) {
+        TNode c = n.getOperator();
+
+        if(! c.getAttribute(RegisteredAttr())) {
+          if(c.getNumChildren() == 0) {
+            c.setAttribute(RegisteredAttr(), true);
+            registerTerm(c);
+          } else {
+            toReg.push_back(c);
+          }
+        }
+      }
+
+      for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
+        TNode c = *i;
+
+        if(! c.getAttribute(RegisteredAttr())) {
+          if(c.getNumChildren() == 0) {
+            c.setAttribute(RegisteredAttr(), true);
+            registerTerm(c);
+          } else {
+            toReg.push_back(c);
+          }
+        }
+      }
+    }
+
+    /* Now register the list of terms in reverse order.  Between this
+     * and the above registration of leaves, this should ensure that
+     * all subterms in the entire tree were registered in
+     * reverse-topological order. */
+    for(std::list<TNode>::reverse_iterator i = toReg.rbegin();
+        i != toReg.rend();
+        ++i) {
+
+      TNode n = *i;
+
+      /* Note that a shared TNode in the DAG rooted at "fact" could
+       * appear twice on the list, so we have to avoid hitting it
+       * twice. */
+      // FIXME when ExprSets are online, use one of those to avoid
+      // duplicates in the above?
+      if(! n.getAttribute(RegisteredAttr())) {
+        n.setAttribute(RegisteredAttr(), true);
+        registerTerm(n);
+      }
+    }
+  }
+
+  return fact;
+}
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 4c3a43061..2fcac86b0 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -38,35 +38,21 @@ namespace theory {
 struct RewriteCacheTag {};
 typedef expr::Attribute<RewriteCacheTag, TNode> RewriteCache;
 
-template <class T>
-class TheoryImpl;
-
 /**
  * Base class for T-solvers.  Abstract DPLL(T).
  *
  * This is essentially an interface class.  The TheoryEngine has
- * pointers to Theory.  But each individual theory implementation T
- * should inherit from TheoryImpl<T>, which specializes a few things
- * for that theory.
+ * pointers to Theory.  Note that only one specific Theory type (e.g.,
+ * TheoryUF) can exist per NodeManager, because of how the
+ * RegisteredAttr works.  (If you need multiple instances of the same
+ * theory, you'll have to write a multiplexed theory that dispatches
+ * all calls to them.)
  */
 class Theory {
 private:
 
-  template <class T>
-  friend class ::CVC4::theory::TheoryImpl;
-
   friend class ::CVC4::TheoryEngine;
 
-  /**
-   * Construct a Theory.
-   */
-  Theory(context::Context* ctxt, OutputChannel& out) throw() :
-    d_context(ctxt),
-    d_facts(),
-    d_factsResetter(*this),
-    d_out(&out) {
-  }
-
   /**
    * Disallow default construction.
    */
@@ -109,14 +95,24 @@ private:
 
 protected:
 
+  /**
+   * Construct a Theory.
+   */
+  Theory(context::Context* ctxt, OutputChannel& out) throw() :
+    d_context(ctxt),
+    d_facts(),
+    d_factsResetter(*this),
+    d_out(&out) {
+  }
+
   /**
    * This is called at shutdown time by the TheoryEngine, just before
    * destruction.  It is important because there are destruction
    * ordering issues between PropEngine and Theory (based on what
    * hard-links to Nodes are outstanding).  As the fact queue might be
    * nonempty, we ensure here that it's clear.  If you overload this,
-   * you must make an explicit call here to the Theory implementation
-   * of this function too.
+   * you must make an explicit call here to this->Theory::shutdown()
+   * too.
    */
   virtual void shutdown() {
     d_facts.clear();
@@ -158,6 +154,24 @@ protected:
     return n.getAttribute(RewriteCache());
   }
 
+  /** Tag for the "registerTerm()-has-been-called" flag on Nodes */
+  struct Registered {};
+  /** The "registerTerm()-has-been-called" flag on Nodes */
+  typedef CVC4::expr::CDAttribute<Registered, bool> RegisteredAttr;
+
+  /** Tag for the "preRegisterTerm()-has-been-called" flag on Nodes */
+  struct PreRegistered {};
+  /** The "preRegisterTerm()-has-been-called" flag on Nodes */
+  typedef CVC4::expr::Attribute<PreRegistered, bool> PreRegisteredAttr;
+
+  /**
+   * Returns the next atom in the assertFact() queue.  Guarantees that
+   * registerTerm() has been called on the theory specific subterms.
+   *
+   * @return the next atom in the assertFact() queue.
+   */
+  Node get();
+
 public:
 
   /**
@@ -308,133 +322,6 @@ protected:
 
 };/* class Theory */
 
-
-/**
- * Base class for T-solver implementations.  Each individual
- * implementation T of the Theory interface should inherit from
- * TheoryImpl<T>.  This class specializes some things for a particular
- * theory implementation.
- *
- * The problem with this is that Theory implementations cannot be
- * further subclassed without designing all non-children in the type
- * DAG to play the same trick as here (be template-polymorphic in their
- * most-derived child), linearizing the inheritance hierarchy (viewing
- * each instantiation separately).
- */
-template <class T>
-class TheoryImpl : public Theory {
-
-protected:
-
-  /**
-   * Construct a Theory.
-   */
-  TheoryImpl(context::Context* ctxt, OutputChannel& out) :
-    Theory(ctxt, out) {
-    /* FIXME: assert here that a TheoryImpl<T> doesn't already exist
-     * for this NodeManager??  If it does, we're hosed because they'll
-     * share per-theory node attributes. */
-  }
-
-  /** Tag for the "registerTerm()-has-been-called" flag on Nodes */
-  struct Registered {};
-  /** The "registerTerm()-has-been-called" flag on Nodes */
-  typedef CVC4::expr::CDAttribute<Registered, bool> RegisteredAttr;
-
-  /** Tag for the "preRegisterTerm()-has-been-called" flag on Nodes */
-  struct PreRegistered {};
-  /** The "preRegisterTerm()-has-been-called" flag on Nodes */
-  typedef CVC4::expr::Attribute<PreRegistered, bool> PreRegisteredAttr;
-
-  /**
-   * Returns the next atom in the assertFact() queue.  Guarantees that
-   * registerTerm() has been called on the theory specific subterms.
-   *
-   * @return the next atom in the assertFact() queue.
-   */
-  Node get();
-};/* class TheoryImpl<T> */
-
-template <class T>
-Node TheoryImpl<T>::get() {
-  Assert(typeid(*this) == typeid(T),
-         "Improper Theory inheritance chain detected.");
-
-  Assert( !d_facts.empty(),
-          "Theory::get() called with assertion queue empty!" );
-
-  Node fact = d_facts.front();
-  d_facts.pop_front();
-
-  Debug("theory") << "Theory::get() => " << fact << "(" << d_facts.size() << " left)" << std::endl;
-
-  if(! fact.getAttribute(RegisteredAttr())) {
-    std::list<TNode> toReg;
-    toReg.push_back(fact);
-
-    Debug("theory") << "Theory::get(): registering new atom" << std::endl;
-
-    /* Essentially this is doing a breadth-first numbering of
-     * non-registered subterms with children.  Any non-registered
-     * leaves are immediately registered. */
-    for(std::list<TNode>::iterator workp = toReg.begin();
-        workp != toReg.end();
-        ++workp) {
-
-      TNode n = *workp;
-
-      if(n.hasOperator()) {
-        TNode c = n.getOperator();
-
-        if(! c.getAttribute(RegisteredAttr())) {
-          if(c.getNumChildren() == 0) {
-            c.setAttribute(RegisteredAttr(), true);
-            registerTerm(c);
-          } else {
-            toReg.push_back(c);
-          }
-        }
-      }
-
-      for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
-        TNode c = *i;
-
-        if(! c.getAttribute(RegisteredAttr())) {
-          if(c.getNumChildren() == 0) {
-            c.setAttribute(RegisteredAttr(), true);
-            registerTerm(c);
-          } else {
-            toReg.push_back(c);
-          }
-        }
-      }
-    }
-
-    /* Now register the list of terms in reverse order.  Between this
-     * and the above registration of leaves, this should ensure that
-     * all subterms in the entire tree were registered in
-     * reverse-topological order. */
-    for(std::list<TNode>::reverse_iterator i = toReg.rbegin();
-        i != toReg.rend();
-        ++i) {
-
-      TNode n = *i;
-
-      /* Note that a shared TNode in the DAG rooted at "fact" could
-       * appear twice on the list, so we have to avoid hitting it
-       * twice. */
-      // FIXME when ExprSets are online, use one of those to avoid
-      // duplicates in the above?
-      if(! n.getAttribute(RegisteredAttr())) {
-        n.setAttribute(RegisteredAttr(), true);
-        registerTerm(n);
-      }
-    }
-  }
-
-  return fact;
-}
-
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am
index 156733c5b..e0aa3a1df 100644
--- a/src/theory/uf/Makefile.am
+++ b/src/theory/uf/Makefile.am
@@ -1,12 +1,11 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
 	-I@srcdir@/../../include -I@srcdir@/../..
-AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libuf.la
 
 libuf_la_SOURCES = \
-	theory_def.h \
 	ecdata.h \
 	ecdata.cpp \
 	theory_uf.h \
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 3fe82b16c..f0d8b47e0 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -10,10 +10,9 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- **
+ ** Implementation of the theory of uninterpreted functions.
  **/
 
-
 #include "theory/uf/theory_uf.h"
 #include "theory/uf/ecdata.h"
 #include "expr/kind.h"
@@ -24,37 +23,32 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::uf;
 
-
-
 TheoryUF::TheoryUF(Context* c, OutputChannel& out) :
-  TheoryImpl<TheoryUF>(c, out),
+  Theory(c, out),
   d_assertions(c),
   d_pending(c),
   d_currentPendingIdx(c,0),
   d_disequality(c),
-  d_registered(c)
-{}
+  d_registered(c) {
+}
 
-TheoryUF::~TheoryUF(){}
+TheoryUF::~TheoryUF() {
+}
 
-void TheoryUF::preRegisterTerm(TNode n){
+void TheoryUF::preRegisterTerm(TNode n) {
   Debug("uf") << "uf: begin preRegisterTerm(" << n << ")" << std::endl;
   Debug("uf") << "uf: end preRegisterTerm(" << n << ")" << std::endl;
 }
 
-void TheoryUF::registerTerm(TNode n){
+void TheoryUF::registerTerm(TNode n) {
 
   Debug("uf") << "uf: begin registerTerm(" << n << ")" << std::endl;
 
-
   d_registered.push_back(n);
 
-
-
-
   ECData* ecN;
 
-  if(n.getAttribute(ECAttr(), ecN)){
+  if(n.getAttribute(ECAttr(), ecN)) {
     /* registerTerm(n) is only called when a node has not been seen in the
      * current context.  ECAttr() is not a context-dependent attribute.
      * When n.hasAttribute(ECAttr(),...) is true on a registerTerm(n) call,
@@ -101,7 +95,7 @@ void TheoryUF::registerTerm(TNode n){
            "Expected getWatchListSize() == 0.  "
            "This data is either already in use or was not properly maintained "
            "during backtracking");
-  }else{
+  } else {
     //The attribute does not exist, so it is created and set
     ecN = new (true) ECData(getContext(), n);
     n.setAttribute(ECAttr(), ecN);
@@ -110,10 +104,10 @@ void TheoryUF::registerTerm(TNode n){
   /* If the node is an APPLY_UF, we need to add it to the predecessor list
    * of its children.
    */
-  if(n.getKind() == APPLY_UF){
+  if(n.getKind() == APPLY_UF) {
     TNode::iterator cIter = n.begin();
 
-    for(; cIter != n.end(); ++cIter){
+    for(; cIter != n.end(); ++cIter) {
       TNode child = *cIter;
 
       /* Because this can be called after nodes have been merged, we need
@@ -124,8 +118,8 @@ void TheoryUF::registerTerm(TNode n){
       /* Because this can be called after nodes have been merged we may need
        * to be merged with other predecessors of the equivalence class.
        */
-      for(Link* Px = ecChild->getFirst(); Px != NULL; Px = Px->d_next ){
-        if(equiv(n, Px->d_data)){
+      for(Link* Px = ecChild->getFirst(); Px != NULL; Px = Px->d_next ) {
+        if(equiv(n, Px->d_data)) {
           Node pend = n.eqNode(Px->d_data);
           d_pending.push_back(pend);
         }
@@ -138,30 +132,32 @@ void TheoryUF::registerTerm(TNode n){
 
 }
 
-bool TheoryUF::sameCongruenceClass(TNode x, TNode y){
+bool TheoryUF::sameCongruenceClass(TNode x, TNode y) {
   return
     ccFind(x.getAttribute(ECAttr())) ==
     ccFind(y.getAttribute(ECAttr()));
 }
 
-bool TheoryUF::equiv(TNode x, TNode y){
+bool TheoryUF::equiv(TNode x, TNode y) {
   Assert(x.getKind() == kind::APPLY_UF);
   Assert(y.getKind() == kind::APPLY_UF);
 
-  if(x.getNumChildren() != y.getNumChildren())
+  if(x.getNumChildren() != y.getNumChildren()) {
     return false;
+  }
 
-  if(x.getOperator() != y.getOperator())
+  if(x.getOperator() != y.getOperator()) {
     return false;
+  }
 
   // intentionally don't look at operator
 
   TNode::iterator xIter = x.begin();
   TNode::iterator yIter = y.begin();
 
-  while(xIter != x.end()){
+  while(xIter != x.end()) {
 
-    if(!sameCongruenceClass(*xIter, *yIter)){
+    if(!sameCongruenceClass(*xIter, *yIter)) {
       return false;
     }
 
@@ -178,10 +174,10 @@ bool TheoryUF::equiv(TNode x, TNode y){
  *    many better algorithms use eager path compression.
  * 2) Elminate recursion.
  */
-ECData* TheoryUF::ccFind(ECData * x){
-  if( x->getFind() == x)
+ECData* TheoryUF::ccFind(ECData * x) {
+  if(x->getFind() == x) {
     return x;
-  else{
+  } else {
     return ccFind(x->getFind());
   }
   /* Slightly better Find w/ path compression and no recursion*/
@@ -189,7 +185,7 @@ ECData* TheoryUF::ccFind(ECData * x){
     ECData* start;
     ECData* next = x;
     while(x != x->getFind()) x=x->getRep();
-    while( (start = next) != x){
+    while( (start = next) != x) {
       next = start->getFind();
       start->setFind(x);
     }
@@ -197,23 +193,23 @@ ECData* TheoryUF::ccFind(ECData * x){
   */
 }
 
-void TheoryUF::ccUnion(ECData* ecX, ECData* ecY){
+void TheoryUF::ccUnion(ECData* ecX, ECData* ecY) {
   ECData* nslave;
   ECData* nmaster;
 
-  if(ecX->getWatchListSize() <= ecY->getWatchListSize()){
+  if(ecX->getWatchListSize() <= ecY->getWatchListSize()) {
     nslave = ecX;
     nmaster = ecY;
-  }else{
+  } else {
     nslave = ecY;
     nmaster = ecX;
   }
 
   nslave->setFind(nmaster);
 
-  for(Link* Px = nmaster->getFirst(); Px != NULL; Px = Px->d_next ){
-    for(Link* Py = nslave->getFirst(); Py != NULL; Py = Py->d_next ){
-      if(equiv(Px->d_data,Py->d_data)){
+  for(Link* Px = nmaster->getFirst(); Px != NULL; Px = Px->d_next ) {
+    for(Link* Py = nslave->getFirst(); Py != NULL; Py = Py->d_next ) {
+      if(equiv(Px->d_data,Py->d_data)) {
         Node pendingEq = (Px->d_data).eqNode(Py->d_data);
         d_pending.push_back(pendingEq);
       }
@@ -223,7 +219,7 @@ void TheoryUF::ccUnion(ECData* ecX, ECData* ecY){
   ECData::takeOverDescendantWatchList(nslave, nmaster);
 }
 
-void TheoryUF::merge(){
+void TheoryUF::merge() {
   while(d_currentPendingIdx < d_pending.size() ) {
     Node assertion = d_pending[d_currentPendingIdx];
     d_currentPendingIdx = d_currentPendingIdx + 1;
@@ -248,7 +244,7 @@ void TheoryUF::merge(){
   }
 }
 
-Node TheoryUF::constructConflict(TNode diseq){
+Node TheoryUF::constructConflict(TNode diseq) {
   Debug("uf") << "uf: begin constructConflict()" << std::endl;
 
   NodeBuilder<> nb(kind::AND);
@@ -267,15 +263,15 @@ Node TheoryUF::constructConflict(TNode diseq){
   return conflict;
 }
 
-void TheoryUF::check(Effort level){
+void TheoryUF::check(Effort level) {
 
   Debug("uf") << "uf: begin check(" << level << ")" << std::endl;
 
-  while(!done()){
+  while(!done()) {
     Node assertion = get();
     Debug("uf") << "TheoryUF::check(): " << assertion << std::endl;
 
-    switch(assertion.getKind()){
+    switch(assertion.getKind()) {
     case EQUAL:
       d_assertions.push_back(assertion);
       d_pending.push_back(assertion);
@@ -292,18 +288,18 @@ void TheoryUF::check(Effort level){
   }
 
   //Make sure all outstanding merges are completed.
-  if(d_currentPendingIdx < d_pending.size()){
+  if(d_currentPendingIdx < d_pending.size()) {
     merge();
   }
 
-  if(fullEffort(level)){
+  if(fullEffort(level)) {
     for(CDList<Node>::const_iterator diseqIter = d_disequality.begin();
         diseqIter != d_disequality.end();
-        ++diseqIter){
+        ++diseqIter) {
 
       TNode left  = (*diseqIter)[0];
       TNode right = (*diseqIter)[1];
-      if(sameCongruenceClass(left, right)){
+      if(sameCongruenceClass(left, right)) {
         Node remakeNeq = (*diseqIter).notNode();
         Node conflict = constructConflict(remakeNeq);
         d_out->conflict(conflict, false);
@@ -313,5 +309,4 @@ void TheoryUF::check(Effort level){
   }
 
   Debug("uf") << "uf: end check(" << level << ")" << std::endl;
-
 }
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 8495e6c9c..5863a31fc 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -38,7 +38,7 @@ namespace CVC4 {
 namespace theory {
 namespace uf {
 
-class TheoryUF : public TheoryImpl<TheoryUF> {
+class TheoryUF : public Theory {
 
 private:
 
@@ -176,31 +176,30 @@ private:
   /** Constructs a conflict from an inconsistent disequality. */
   Node constructConflict(TNode diseq);
 
-};
+};/* class TheoryUF */
 
 
 /**
  * Cleanup function for ECData. This will be used for called whenever
  * a ECAttr is being destructed.
  */
-struct ECCleanupStrategy{
-  static void cleanup(ECData* ec){
+struct ECCleanupStrategy {
+  static void cleanup(ECData* ec) {
     Debug("ufgc") << "cleaning up ECData " << ec << "\n";
     ec->deleteSelf();
   }
-};
+};/* struct ECCleanupStrategy */
 
 /** Unique name to use for constructing ECAttr. */
-struct EquivClass;
+struct ECAttrTag {};
 
 /**
  * ECAttr is the attribute that maps a node to an equivalence class.
  */
-typedef expr::Attribute<EquivClass, ECData*, ECCleanupStrategy > ECAttr;
-
-} /* CVC4::theory::uf namespace */
-} /* CVC4::theory namespace */
-} /* CVC4 namespace */
+typedef expr::Attribute<ECAttrTag, ECData*, ECCleanupStrategy> ECAttr;
 
+}/* CVC4::theory::uf namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
 #endif /* __CVC4__THEORY__UF__THEORY_UF_H */
diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp
index 06be4ab7c..1611f28d3 100644
--- a/src/util/Assert.cpp
+++ b/src/util/Assert.cpp
@@ -70,8 +70,10 @@ 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;
+  if(s_debugAssertionFailure == NULL) {
+    // we leak buf[] but only in debug mode with assertions failing
+    s_debugAssertionFailure = buf;
+  }
 #else /* CVC4_DEBUG */
   delete [] buf;
 #endif /* CVC4_DEBUG */
@@ -110,7 +112,9 @@ void AssertionException::construct(const char* header, const char* extra,
 
 #ifdef CVC4_DEBUG
   // we leak buf[] but only in debug mode with assertions failing
-  s_debugAssertionFailure = buf;
+  if(s_debugAssertionFailure == NULL) {
+    s_debugAssertionFailure = buf;
+  }
 #else /* CVC4_DEBUG */
   delete [] buf;
 #endif /* CVC4_DEBUG */
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 5e8dfd2a4..6597c8b48 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -1,7 +1,7 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
 	-I@srcdir@/../include -I@srcdir@/..
-AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libutil.la
 
diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index f4ce30968..5ed13a139 100644
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -94,7 +94,7 @@ string Configuration::about() {
 This is a pre-release of CVC4.\n\
 Copyright (C) 2009, 2010\n\
   The ACSys Group\n\
-  Courant Institute of Mathematical Sciences,\n\
+  Courant Institute of Mathematical Sciences\n\
   New York University\n\
   New York, NY  10012  USA\n");
 }
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index eb07b22fb..fe95ed7aa 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,7 +1,9 @@
 SUBDIRS = precedence uf
 
-TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
 TESTS =	\
+    error.cvc \
+    boolean-prec.cvc \
     distinct.smt \
     flet.smt \
     flet2.smt \
@@ -43,7 +45,7 @@ TESTS =	\
 	wiki.19.cvc \
 	wiki.20.cvc \
 	wiki.21.cvc
-	
+
 # synonyms for "check"
 .PHONY: regress regress0 test
 regress regress0 test: check
diff --git a/test/regress/regress0/boolean-prec.cvc b/test/regress/regress0/boolean-prec.cvc
index 4f84de94d..d0205116c 100644
--- a/test/regress/regress0/boolean-prec.cvc
+++ b/test/regress/regress0/boolean-prec.cvc
@@ -1,6 +1,7 @@
-% Expect: VALID
+% EXPECT: VALID
 % Simple test for right precedence of AND, <=>, NOT.
 
 A, B, C: BOOLEAN;
 
 QUERY (NOT A AND NOT B <=> C) <=> (((NOT A) AND (NOT B)) <=> C);
+% EXIT: 20
diff --git a/test/regress/regress0/boolean.cvc b/test/regress/regress0/boolean.cvc
index 89afbe325..eeac40c9f 100644
--- a/test/regress/regress0/boolean.cvc
+++ b/test/regress/regress0/boolean.cvc
@@ -804,3 +804,4 @@ a288 : BOOLEAN =
         ELSE FALSE
         ENDIF;
 QUERY a288;
+% EXIT: 20
diff --git a/test/regress/regress0/bug1.cvc b/test/regress/regress0/bug1.cvc
index d3d936381..2b59638d1 100644
--- a/test/regress/regress0/bug1.cvc
+++ b/test/regress/regress0/bug1.cvc
@@ -6,3 +6,4 @@ ASSERT ((x > y) => f(x) > f (y));
 ASSERT (x = 3);
 ASSERT (y = 2);
 QUERY(f(x) > f (y));
+% EXIT: 20
diff --git a/test/regress/regress0/bug32.cvc b/test/regress/regress0/bug32.cvc
index 8d113d785..c6d79a4ab 100644
--- a/test/regress/regress0/bug32.cvc
+++ b/test/regress/regress0/bug32.cvc
@@ -4,3 +4,4 @@ b:BOOLEAN;
 ASSERT(a);
 QUERY(a OR b);
 
+% EXIT: 20
diff --git a/test/regress/regress0/error.cvc b/test/regress/regress0/error.cvc
new file mode 100644
index 000000000..09a69e212
--- /dev/null
+++ b/test/regress/regress0/error.cvc
@@ -0,0 +1,4 @@
+% EXPECT-ERROR: CVC4 Error:
+% EXPECT-ERROR: Parse Error: Parser Error: error.cvc:3.9: Symbol BOOL not declared
+p : BOOL;
+% EXIT: 1
diff --git a/test/regress/regress0/hole6.cvc b/test/regress/regress0/hole6.cvc
index bdd45b6d0..07bfa392c 100644
--- a/test/regress/regress0/hole6.cvc
+++ b/test/regress/regress0/hole6.cvc
@@ -177,3 +177,4 @@ ASSERT x_42 OR x_41 OR x_40 OR x_39 OR x_38 OR x_37;
 
 
 QUERY FALSE;
+% EXIT: 20
diff --git a/test/regress/regress0/logops.01.cvc b/test/regress/regress0/logops.01.cvc
index d947d1a27..5348cf7e4 100644
--- a/test/regress/regress0/logops.01.cvc
+++ b/test/regress/regress0/logops.01.cvc
@@ -1,3 +1,4 @@
 a, b, c: BOOLEAN;
 % EXPECT: VALID
 QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a);
+% EXIT: 20
diff --git a/test/regress/regress0/logops.02.cvc b/test/regress/regress0/logops.02.cvc
index ba2d55b4f..4a8539fae 100644
--- a/test/regress/regress0/logops.02.cvc
+++ b/test/regress/regress0/logops.02.cvc
@@ -1,3 +1,4 @@
 a, b, c: BOOLEAN;
 % EXPECT: INVALID
 QUERY NOT c AND b;
+% EXIT: 10
diff --git a/test/regress/regress0/logops.03.cvc b/test/regress/regress0/logops.03.cvc
index 85b23d2b0..6b5f34613 100644
--- a/test/regress/regress0/logops.03.cvc
+++ b/test/regress/regress0/logops.03.cvc
@@ -1,3 +1,4 @@
 a, b, c: BOOLEAN;
 % EXPECT: VALID
 QUERY (IF c THEN a ELSE b ENDIF) <=> ((c AND a) OR (NOT c AND b));
+% EXIT: 20
diff --git a/test/regress/regress0/logops.04.cvc b/test/regress/regress0/logops.04.cvc
index a71096542..6e7aa1f5e 100644
--- a/test/regress/regress0/logops.04.cvc
+++ b/test/regress/regress0/logops.04.cvc
@@ -1,3 +1,4 @@
 a, b, c: BOOLEAN;
 % EXPECT: VALID
 QUERY (a => b) <=> (NOT a OR b);
+% EXIT: 20
diff --git a/test/regress/regress0/logops.05.cvc b/test/regress/regress0/logops.05.cvc
index 19bbae5b4..14e2c887a 100644
--- a/test/regress/regress0/logops.05.cvc
+++ b/test/regress/regress0/logops.05.cvc
@@ -2,3 +2,4 @@ a, b, c: BOOLEAN;
 % EXPECT: VALID
 QUERY TRUE XOR FALSE;
  
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/Makefile.am b/test/regress/regress0/precedence/Makefile.am
index 0b4fcd4a6..362ec70b6 100644
--- a/test/regress/regress0/precedence/Makefile.am
+++ b/test/regress/regress0/precedence/Makefile.am
@@ -1,4 +1,4 @@
-TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/../../bin/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
 TESTS = \
     iff-implies.cvc \
 	implies-iff.cvc \
diff --git a/test/regress/regress0/precedence/and-not.cvc b/test/regress/regress0/precedence/and-not.cvc
index d283ca881..0de37db83 100644
--- a/test/regress/regress0/precedence/and-not.cvc
+++ b/test/regress/regress0/precedence/and-not.cvc
@@ -4,3 +4,4 @@
 A, B: BOOLEAN;
 
 QUERY (A AND NOT B) <=> (A AND (NOT B));
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/and-xor.cvc b/test/regress/regress0/precedence/and-xor.cvc
index c7268727a..7b29bb95e 100644
--- a/test/regress/regress0/precedence/and-xor.cvc
+++ b/test/regress/regress0/precedence/and-xor.cvc
@@ -4,3 +4,4 @@
 A, B, C: BOOLEAN;
 
 QUERY (A AND B XOR C) <=> ((A AND B) XOR C);
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/eq-fun.cvc b/test/regress/regress0/precedence/eq-fun.cvc
index 43feeb1f8..e85b4a3e6 100644
--- a/test/regress/regress0/precedence/eq-fun.cvc
+++ b/test/regress/regress0/precedence/eq-fun.cvc
@@ -6,3 +6,4 @@ x , y: T;
 f : T -> T;
 
 QUERY (f(x) = f(y)) <=> ((f(x)) = (f(y)));
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/iff-assoc.cvc b/test/regress/regress0/precedence/iff-assoc.cvc
index 82e0cbc72..b92354753 100644
--- a/test/regress/regress0/precedence/iff-assoc.cvc
+++ b/test/regress/regress0/precedence/iff-assoc.cvc
@@ -4,3 +4,4 @@
 A, B, C: BOOLEAN;
 
 QUERY (A <=> B <=> C) <=> (A <=> (B <=> C));
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/iff-implies.cvc b/test/regress/regress0/precedence/iff-implies.cvc
index bebafce14..0115fc319 100644
--- a/test/regress/regress0/precedence/iff-implies.cvc
+++ b/test/regress/regress0/precedence/iff-implies.cvc
@@ -4,3 +4,4 @@
 A, B, C: BOOLEAN;
 
 QUERY (A <=> B => C) <=> ((A <=> (B => C)));
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/implies-assoc.cvc b/test/regress/regress0/precedence/implies-assoc.cvc
index c73616caf..d465df313 100644
--- a/test/regress/regress0/precedence/implies-assoc.cvc
+++ b/test/regress/regress0/precedence/implies-assoc.cvc
@@ -4,3 +4,4 @@
 A, B, C: BOOLEAN;
 
 QUERY (A => B => C) <=> (A => (B => C));
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/implies-iff.cvc b/test/regress/regress0/precedence/implies-iff.cvc
index f44c4bc75..f8c813ceb 100644
--- a/test/regress/regress0/precedence/implies-iff.cvc
+++ b/test/regress/regress0/precedence/implies-iff.cvc
@@ -4,3 +4,4 @@
 A, B, C: BOOLEAN;
 
 QUERY (A => B <=> C) <=> ((A => B) <=> C);
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/implies-or.cvc b/test/regress/regress0/precedence/implies-or.cvc
index 835da8570..24edb4ecd 100644
--- a/test/regress/regress0/precedence/implies-or.cvc
+++ b/test/regress/regress0/precedence/implies-or.cvc
@@ -4,3 +4,4 @@
 A, B, C: BOOLEAN;
 
 QUERY (A => B OR C) <=> (A => (B OR C));
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/not-and.cvc b/test/regress/regress0/precedence/not-and.cvc
index 44c27af53..8c849a0d9 100644
--- a/test/regress/regress0/precedence/not-and.cvc
+++ b/test/regress/regress0/precedence/not-and.cvc
@@ -4,3 +4,4 @@
 A, B, C: BOOLEAN;
 
 QUERY (NOT A AND B) <=> ((NOT A) AND B);
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/not-eq.cvc b/test/regress/regress0/precedence/not-eq.cvc
index 1126926b8..16c812086 100644
--- a/test/regress/regress0/precedence/not-eq.cvc
+++ b/test/regress/regress0/precedence/not-eq.cvc
@@ -4,3 +4,4 @@
 A, B: BOOLEAN;
 
 QUERY (NOT A = B) <=> (NOT (A = B));
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/or-implies.cvc b/test/regress/regress0/precedence/or-implies.cvc
index 3b336db5a..d91f79dc8 100644
--- a/test/regress/regress0/precedence/or-implies.cvc
+++ b/test/regress/regress0/precedence/or-implies.cvc
@@ -4,3 +4,4 @@
 A, B, C: BOOLEAN;
 
 QUERY (A OR B => C) <=> ((A OR B) => C);
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/or-xor.cvc b/test/regress/regress0/precedence/or-xor.cvc
index 2198962c8..47cc87c76 100644
--- a/test/regress/regress0/precedence/or-xor.cvc
+++ b/test/regress/regress0/precedence/or-xor.cvc
@@ -4,3 +4,4 @@
 A, B, C: BOOLEAN;
 
 QUERY (A OR B XOR C) <=> (A OR (B XOR C));
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/xor-and.cvc b/test/regress/regress0/precedence/xor-and.cvc
index ccdaeebad..ba3f48a7f 100644
--- a/test/regress/regress0/precedence/xor-and.cvc
+++ b/test/regress/regress0/precedence/xor-and.cvc
@@ -4,3 +4,4 @@
 A, B, C: BOOLEAN;
 
 QUERY (A XOR B AND C) <=> (A XOR (B AND C));
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/xor-assoc.cvc b/test/regress/regress0/precedence/xor-assoc.cvc
index ffdb2c8c9..27911332c 100644
--- a/test/regress/regress0/precedence/xor-assoc.cvc
+++ b/test/regress/regress0/precedence/xor-assoc.cvc
@@ -4,3 +4,4 @@
 A, B, C: BOOLEAN;
 
 QUERY (A XOR B XOR C) <=> ((A XOR B) XOR C);
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/xor-or.cvc b/test/regress/regress0/precedence/xor-or.cvc
index 959dec14e..2b4436937 100644
--- a/test/regress/regress0/precedence/xor-or.cvc
+++ b/test/regress/regress0/precedence/xor-or.cvc
@@ -4,3 +4,4 @@
 A, B, C: BOOLEAN;
 
 QUERY (A XOR B OR C) <=> ((A XOR B) OR C);
+% EXIT: 20
diff --git a/test/regress/regress0/queries0.cvc b/test/regress/regress0/queries0.cvc
index 36107e784..fe6235981 100644
--- a/test/regress/regress0/queries0.cvc
+++ b/test/regress/regress0/queries0.cvc
@@ -8,3 +8,4 @@ QUERY (a AND b) OR NOT (a AND b);
 % EXPECT: INVALID
 QUERY (a OR b);
 
+% EXIT: 10
diff --git a/test/regress/regress0/simple.cvc b/test/regress/regress0/simple.cvc
index 21145b6e0..a0bff6c5a 100644
--- a/test/regress/regress0/simple.cvc
+++ b/test/regress/regress0/simple.cvc
@@ -5,3 +5,4 @@ ASSERT x3 OR x2;
 ASSERT x1 AND NOT x1;
 % EXPECT: VALID
 QUERY x2;
+% EXIT: 20
diff --git a/test/regress/regress0/smallcnf.cvc b/test/regress/regress0/smallcnf.cvc
index 3a36b8c1e..fe17e0b53 100644
--- a/test/regress/regress0/smallcnf.cvc
+++ b/test/regress/regress0/smallcnf.cvc
@@ -7,3 +7,4 @@ ASSERT a OR NOT b OR c;
 % EXPECT: INVALID
 QUERY FALSE;
 
+% EXIT: 10
diff --git a/test/regress/regress0/test11.cvc b/test/regress/regress0/test11.cvc
index 6f0cac8fa..2fa1e23ba 100644
--- a/test/regress/regress0/test11.cvc
+++ b/test/regress/regress0/test11.cvc
@@ -5,3 +5,4 @@ ASSERT NOT (x OR y);
 
 % EXPECT: VALID
 QUERY FALSE;
+% EXIT: 20
diff --git a/test/regress/regress0/test12.cvc b/test/regress/regress0/test12.cvc
index 48966f53b..a3d63b497 100644
--- a/test/regress/regress0/test12.cvc
+++ b/test/regress/regress0/test12.cvc
@@ -175,3 +175,4 @@ QUERY NOT P_10;
 POP;
 PUSH;
 QUERY FALSE;
+% EXIT: 20
diff --git a/test/regress/regress0/test9.cvc b/test/regress/regress0/test9.cvc
index de6be2f54..64c2011a4 100644
--- a/test/regress/regress0/test9.cvc
+++ b/test/regress/regress0/test9.cvc
@@ -2,3 +2,4 @@
 P,Q:BOOLEAN;
 ASSERT (P OR Q);
 QUERY (P OR Q);
+% EXIT: 20
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index ec99fd45c..802189f2b 100644
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -1,4 +1,4 @@
-TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/../../bin/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
 TESTS =	\
 	euf_simp01.smt \
 	euf_simp02.smt \
diff --git a/test/regress/regress0/uf/simple.01.cvc b/test/regress/regress0/uf/simple.01.cvc
index f5d8c1033..84b8b8a8d 100644
--- a/test/regress/regress0/uf/simple.01.cvc
+++ b/test/regress/regress0/uf/simple.01.cvc
@@ -5,3 +5,4 @@ x, y: A;
 f: A -> B;
 QUERY (x = y => f(x) = f(y));
 
+% EXIT: 20
diff --git a/test/regress/regress0/uf/simple.02.cvc b/test/regress/regress0/uf/simple.02.cvc
index 0ebc319ba..21d3e3cee 100644
--- a/test/regress/regress0/uf/simple.02.cvc
+++ b/test/regress/regress0/uf/simple.02.cvc
@@ -5,3 +5,4 @@ x, y: A;
 f: A -> B;
 QUERY (f(x) = f(y));
 
+% EXIT: 10
diff --git a/test/regress/regress0/uf/simple.03.cvc b/test/regress/regress0/uf/simple.03.cvc
index 54948edb8..476c6cd4a 100644
--- a/test/regress/regress0/uf/simple.03.cvc
+++ b/test/regress/regress0/uf/simple.03.cvc
@@ -9,3 +9,4 @@ f: A -> B;
 ASSERT (x = a AND y = a) OR (x = b AND y = b);
 QUERY (f(x) = f(y));
 
+% EXIT: 20
diff --git a/test/regress/regress0/uf/simple.04.cvc b/test/regress/regress0/uf/simple.04.cvc
index 58bb6fef1..c9675588d 100644
--- a/test/regress/regress0/uf/simple.04.cvc
+++ b/test/regress/regress0/uf/simple.04.cvc
@@ -9,3 +9,4 @@ f: A -> B;
 ASSERT (x = a OR x = b) AND (y = b OR y = a);
 QUERY (f(x) = f(y));
 
+% EXIT: 10
diff --git a/test/regress/regress0/uf20-03.cvc b/test/regress/regress0/uf20-03.cvc
index 74fdb1116..a44b028a2 100644
--- a/test/regress/regress0/uf20-03.cvc
+++ b/test/regress/regress0/uf20-03.cvc
@@ -113,3 +113,4 @@ ASSERT x_10 OR NOT x_11 OR x_16;
 
 
 QUERY FALSE;
+% EXIT: 10
diff --git a/test/regress/regress0/wiki.01.cvc b/test/regress/regress0/wiki.01.cvc
index 57660b5a1..7b6835469 100644
--- a/test/regress/regress0/wiki.01.cvc
+++ b/test/regress/regress0/wiki.01.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a OR (b OR c) <=> (a OR b) OR c;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.02.cvc b/test/regress/regress0/wiki.02.cvc
index baba45927..9fd4f8fb7 100644
--- a/test/regress/regress0/wiki.02.cvc
+++ b/test/regress/regress0/wiki.02.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a AND (b AND c) <=> (a AND b) AND c;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.03.cvc b/test/regress/regress0/wiki.03.cvc
index 791cc45c8..63c1029b4 100644
--- a/test/regress/regress0/wiki.03.cvc
+++ b/test/regress/regress0/wiki.03.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a OR b <=> b OR a;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.04.cvc b/test/regress/regress0/wiki.04.cvc
index f0f73ce1f..77fa0059b 100644
--- a/test/regress/regress0/wiki.04.cvc
+++ b/test/regress/regress0/wiki.04.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a AND b <=> b AND a;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.05.cvc b/test/regress/regress0/wiki.05.cvc
index afb094dae..cb7140bcc 100644
--- a/test/regress/regress0/wiki.05.cvc
+++ b/test/regress/regress0/wiki.05.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a OR (a AND b) <=> a;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.06.cvc b/test/regress/regress0/wiki.06.cvc
index 421bfbdfd..6c69ca4bc 100644
--- a/test/regress/regress0/wiki.06.cvc
+++ b/test/regress/regress0/wiki.06.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a AND (a OR b) <=> a;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.07.cvc b/test/regress/regress0/wiki.07.cvc
index a28cbf553..a0281d04b 100644
--- a/test/regress/regress0/wiki.07.cvc
+++ b/test/regress/regress0/wiki.07.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a OR (b AND c) <=> (a OR b) AND (a OR c);
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.08.cvc b/test/regress/regress0/wiki.08.cvc
index 70fc5f430..ddf0f328c 100644
--- a/test/regress/regress0/wiki.08.cvc
+++ b/test/regress/regress0/wiki.08.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a AND (b OR c) <=> (a AND b) OR (a AND c);
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.09.cvc b/test/regress/regress0/wiki.09.cvc
index d3118536d..f97021910 100644
--- a/test/regress/regress0/wiki.09.cvc
+++ b/test/regress/regress0/wiki.09.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a OR NOT a;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.10.cvc b/test/regress/regress0/wiki.10.cvc
index 41a9bcd3f..da8a1a9c3 100644
--- a/test/regress/regress0/wiki.10.cvc
+++ b/test/regress/regress0/wiki.10.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a AND NOT a <=> FALSE;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.11.cvc b/test/regress/regress0/wiki.11.cvc
index e9c0b9cce..4d7c3c130 100644
--- a/test/regress/regress0/wiki.11.cvc
+++ b/test/regress/regress0/wiki.11.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a OR a <=> a;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.12.cvc b/test/regress/regress0/wiki.12.cvc
index d5e7bd776..c932892c8 100644
--- a/test/regress/regress0/wiki.12.cvc
+++ b/test/regress/regress0/wiki.12.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a AND a <=> a;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.13.cvc b/test/regress/regress0/wiki.13.cvc
index 2674ba47b..3ad4fd4ab 100644
--- a/test/regress/regress0/wiki.13.cvc
+++ b/test/regress/regress0/wiki.13.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a OR FALSE <=> a;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.14.cvc b/test/regress/regress0/wiki.14.cvc
index 378b84dcd..454cf442c 100644
--- a/test/regress/regress0/wiki.14.cvc
+++ b/test/regress/regress0/wiki.14.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a AND TRUE <=> a;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.15.cvc b/test/regress/regress0/wiki.15.cvc
index ca51c4632..81a13f798 100644
--- a/test/regress/regress0/wiki.15.cvc
+++ b/test/regress/regress0/wiki.15.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a OR TRUE <=> TRUE;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.16.cvc b/test/regress/regress0/wiki.16.cvc
index af47433f8..bd13faf11 100644
--- a/test/regress/regress0/wiki.16.cvc
+++ b/test/regress/regress0/wiki.16.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY a AND FALSE <=> FALSE;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.17.cvc b/test/regress/regress0/wiki.17.cvc
index dc7e7a1c3..48949f89f 100644
--- a/test/regress/regress0/wiki.17.cvc
+++ b/test/regress/regress0/wiki.17.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY NOT FALSE <=> TRUE;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.18.cvc b/test/regress/regress0/wiki.18.cvc
index 21a87f4b5..8959d34a6 100644
--- a/test/regress/regress0/wiki.18.cvc
+++ b/test/regress/regress0/wiki.18.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY NOT TRUE <=> FALSE;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.19.cvc b/test/regress/regress0/wiki.19.cvc
index c6081c200..11366526b 100644
--- a/test/regress/regress0/wiki.19.cvc
+++ b/test/regress/regress0/wiki.19.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY NOT (a OR b) <=> NOT a AND NOT b;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.20.cvc b/test/regress/regress0/wiki.20.cvc
index 3bec9348b..5ef534bb0 100644
--- a/test/regress/regress0/wiki.20.cvc
+++ b/test/regress/regress0/wiki.20.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY NOT (a AND b) <=> NOT a OR NOT b;
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.21.cvc b/test/regress/regress0/wiki.21.cvc
index e99ba2d68..bcd7146fb 100644
--- a/test/regress/regress0/wiki.21.cvc
+++ b/test/regress/regress0/wiki.21.cvc
@@ -2,3 +2,4 @@ a, b, c : BOOLEAN;
 
 % EXPECT: VALID
 QUERY NOT NOT a <=> a;
+% EXIT: 20
diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am
index 8a41e99a3..9307a33a2 100644
--- a/test/regress/regress1/Makefile.am
+++ b/test/regress/regress1/Makefile.am
@@ -1,4 +1,4 @@
-TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
 TESTS =	friedman_n4_i5.smt \
 	hole7.cvc \
 	hole8.cvc \
diff --git a/test/regress/regress1/hole7.cvc b/test/regress/regress1/hole7.cvc
index 1bebf8049..5ff290f62 100644
--- a/test/regress/regress1/hole7.cvc
+++ b/test/regress/regress1/hole7.cvc
@@ -262,3 +262,4 @@ ASSERT x_56 OR x_55 OR x_54 OR x_53 OR x_52 OR x_51 OR x_50;
 
 
 QUERY FALSE;
+% EXIT: 20
diff --git a/test/regress/regress1/hole8.cvc b/test/regress/regress1/hole8.cvc
index 65942a27f..d0f974619 100644
--- a/test/regress/regress1/hole8.cvc
+++ b/test/regress/regress1/hole8.cvc
@@ -371,3 +371,4 @@ ASSERT x_72 OR x_71 OR x_70 OR x_69 OR x_68 OR x_67 OR x_66 OR x_65;
 
 
 QUERY FALSE;
+% EXIT: 20
diff --git a/test/regress/regress2/Makefile.am b/test/regress/regress2/Makefile.am
index 2f72dd5e2..710ee6b8e 100644
--- a/test/regress/regress2/Makefile.am
+++ b/test/regress/regress2/Makefile.am
@@ -1,4 +1,4 @@
-TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
 TESTS =	bmc-galileo-8.smt \
 	bmc-galileo-9.smt \
 	bmc-ibm-10.smt \
diff --git a/test/regress/regress2/hole9.cvc b/test/regress/regress2/hole9.cvc
index 93377ca0b..e631444d3 100644
--- a/test/regress/regress2/hole9.cvc
+++ b/test/regress/regress2/hole9.cvc
@@ -507,3 +507,4 @@ ASSERT x_90 OR x_89 OR x_88 OR x_87 OR x_86 OR x_85 OR x_84 OR x_83 OR x_82;
 
 
 QUERY FALSE;
+% EXIT: 20
diff --git a/test/regress/regress3/Makefile.am b/test/regress/regress3/Makefile.am
index f0f46171c..156fffb54 100644
--- a/test/regress/regress3/Makefile.am
+++ b/test/regress/regress3/Makefile.am
@@ -1,4 +1,4 @@
-TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4
+TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
 TESTS =	C880mul.miter.shuffled-as.sat03-348.smt \
 	comb2.shuffled-as.sat03-420.smt \
 	hole10.cvc \
diff --git a/test/regress/regress3/hole10.cvc b/test/regress/regress3/hole10.cvc
index 39c978b18..661e3ef4b 100644
--- a/test/regress/regress3/hole10.cvc
+++ b/test/regress/regress3/hole10.cvc
@@ -673,3 +673,4 @@ ASSERT x_110 OR x_109 OR x_108 OR x_107 OR x_106 OR x_105 OR x_104 OR x_103 OR x
 
 
 QUERY FALSE;
+% EXIT: 20
diff --git a/test/regress/run_regression b/test/regress/run_regression
index 2be776b3f..65ab6c31a 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -44,35 +44,68 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
   fi
 elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then
   expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'`
-  if [ -z "$expected_output" ]; then
-    error "cannot determine status of \`$benchmark'"
+  expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'`
+  if [ -z "$expected_output" -a -z "$expected_error" ]; then
+    error "cannot determine expected output of \`$benchmark': " \
+          "please use \`% EXPECT:' and/or \`% EXPECT-ERROR:' gestures"
   fi
   expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | sed 's,^% EXIT: ,,'`
+  if [ -z "$expected_exit_status" ]; then
+    error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
+  fi
 else
   error "benchmark \`$benchmark' must be *.cvc or *.smt"
 fi
 
-expfile=`mktemp -t cvc4_expected.XXXXXXXXXX`
-outfile=`mktemp -t cvc4_output.XXXXXXXXXX`
-echo "$expected_output" >"$expfile"
+expoutfile=`mktemp -t cvc4_expect_stdout.XXXXXXXXXX`
+experrfile=`mktemp -t cvc4_expect_stderr.XXXXXXXXXX`
+outfile=`mktemp -t cvc4_stdout.XXXXXXXXXX`
+errfile=`mktemp -t cvc4_stderr.XXXXXXXXXX`
+exitstatusfile=`mktemp -t cvc4_exitstatus.XXXXXXXXXX`
+if [ -z "$expected_output" ]; then
+  # in case expected stdout output is empty, make sure we don't differ
+  # by a newline, which we would if we echo "" >"$expoutfile"
+  touch "$expoutfile"
+else
+  echo "$expected_output" >"$expoutfile"
+fi
+if [ -z "$expected_error" ]; then
+  # in case expected stderr output is empty, make sure we don't differ
+  # by a newline, which we would if we echo "" >"$experrfile"
+  touch "$experrfile"
+else
+  echo "$expected_error" >"$experrfile"
+fi
 
-# echo "$cvc4" --segv-nospin "$benchmark"
-"$cvc4" --segv-nospin "$benchmark" > "$outfile"
+("$cvc4" --segv-nospin "$benchmark"; echo $? >"$exitstatusfile") > "$outfile" 2> "$errfile"
 
-diffs=`diff -u "$expfile" "$outfile"`
+diffs=`diff -u "$expoutfile" "$outfile"`
 diffexit=$?
-rm -f "$expfile"
+diffserr=`diff -u "$experrfile" "$errfile"`
+diffexiterr=$?
+exit_status=`cat "$exitstatusfile"`
+
+rm -f "$expoutfile"
+rm -f "$experrfile"
 rm -f "$outfile"
+rm -f "$errfile"
+rm -f "$exitstatusfile"
+
+exitcode=0
 if [ $diffexit -ne 0 ]; then
-  echo "$prog: error: differences between expected and actual output"
+  echo "$prog: error: differences between expected and actual output on stdout"
   echo "$diffs"
-  exit 1
+  exitcode=1
+fi
+if [ $diffexiterr -ne 0 ]; then
+  echo "$prog: error: differences between expected and actual output on stderr"
+  echo "$diffserr"
+  exitcode=1
 fi
 
-if [ -n "$expected_exit_status" ]; then
-  :
-  #if [ $exit_status != "$expected_exit_status" ]; then
-  #  error "expected exit status \`$expected_exit_status' but got \`$exit_status'"
-  #fi
+if [ "$exit_status" != "$expected_exit_status" ]; then
+  echo  "$prog: error: expected exit status \`$expected_exit_status' but got \`$exit_status'"
+  exitcode=1
 fi
 
+exit $exitcode
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 768a56a9b..451100b59 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -10,6 +10,7 @@ UNIT_TESTS = \
 	expr/attribute_black \
 	parser/parser_white \
 	context/context_black \
+	context/context_white \
 	context/context_mm_black \
 	context/cdo_black \
 	context/cdlist_black \
diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h
index 7040e4cc1..262c66fe5 100644
--- a/test/unit/context/cdmap_black.h
+++ b/test/unit/context/cdmap_black.h
@@ -30,6 +30,8 @@ public:
   void setUp() {
     d_context = new Context;
     //Debug.on("cdmap");
+    //Debug.on("gc");
+    //Debug.on("pushpop");
   }
 
   void tearDown() {
diff --git a/test/unit/context/context_white.h b/test/unit/context/context_white.h
new file mode 100644
index 000000000..3e0928baf
--- /dev/null
+++ b/test/unit/context/context_white.h
@@ -0,0 +1,186 @@
+/*********************                                                        */
+/** context_white.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.
+ **
+ ** White box testing of CVC4::context::Context.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "context/context.h"
+#include "context/cdo.h"
+#include "util/Assert.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::context;
+
+class ContextWhite : public CxxTest::TestSuite {
+private:
+
+  Context* d_context;
+
+public:
+
+  void setUp() {
+    d_context = new Context;
+  }
+
+  void tearDown() {
+    delete d_context;
+  }
+
+  void testContextSimple() {
+    Scope *s = d_context->getTopScope();
+
+    TS_ASSERT(s == d_context->getBottomScope());
+    TS_ASSERT(d_context->getLevel() == 0);
+    TS_ASSERT(d_context->d_scopeList.size() == 1);
+
+    TS_ASSERT(s->d_pContext == d_context);
+    TS_ASSERT(s->d_pCMM == d_context->d_pCMM);
+    TS_ASSERT(s->d_level == 0);
+    TS_ASSERT(s->d_pContextObjList == NULL);
+
+    CDO<int> a(d_context);
+
+    TS_ASSERT(s->d_pContext == d_context);
+    TS_ASSERT(s->d_pCMM == d_context->d_pCMM);
+    TS_ASSERT(s->d_level == 0);
+    TS_ASSERT(s->d_pContextObjList == &a);
+
+    TS_ASSERT(a.d_pScope == s);
+    TS_ASSERT(a.d_pContextObjRestore == NULL);
+    TS_ASSERT(a.d_pContextObjNext == NULL);
+    TS_ASSERT(a.d_ppContextObjPrev == &s->d_pContextObjList);
+
+    CDO<int> b(d_context);
+
+    TS_ASSERT(s->d_pContext == d_context);
+    TS_ASSERT(s->d_pCMM == d_context->d_pCMM);
+    TS_ASSERT(s->d_level == 0);
+    TS_ASSERT(s->d_pContextObjList == &b);
+
+    TS_ASSERT(a.d_pScope == s);
+    TS_ASSERT(a.d_pContextObjRestore == NULL);
+    TS_ASSERT(a.d_pContextObjNext == NULL);
+    TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext);
+
+    TS_ASSERT(b.d_pScope == s);
+    TS_ASSERT(b.d_pContextObjRestore == NULL);
+    TS_ASSERT(b.d_pContextObjNext == &a);
+    TS_ASSERT(b.d_ppContextObjPrev == &s->d_pContextObjList);
+
+    d_context->push();
+    Scope* t = d_context->getTopScope();
+    TS_ASSERT(s != t);
+
+    TS_ASSERT(s == d_context->getBottomScope());
+    TS_ASSERT(d_context->getLevel() == 1);
+    TS_ASSERT(d_context->d_scopeList.size() == 2);
+
+    TS_ASSERT(s->d_pContext == d_context);
+    TS_ASSERT(s->d_pCMM == d_context->d_pCMM);
+    TS_ASSERT(s->d_level == 0);
+    TS_ASSERT(s->d_pContextObjList == &b);
+
+    TS_ASSERT(t->d_pContext == d_context);
+    TS_ASSERT(t->d_pCMM == d_context->d_pCMM);
+    TS_ASSERT(t->d_level == 1);
+    TS_ASSERT(t->d_pContextObjList == NULL);
+
+    TS_ASSERT(a.d_pScope == s);
+    TS_ASSERT(a.d_pContextObjRestore == NULL);
+    TS_ASSERT(a.d_pContextObjNext == NULL);
+    TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext);
+
+    TS_ASSERT(b.d_pScope == s);
+    TS_ASSERT(b.d_pContextObjRestore == NULL);
+    TS_ASSERT(b.d_pContextObjNext == &a);
+    TS_ASSERT(b.d_ppContextObjPrev == &s->d_pContextObjList);
+
+    a = 5;
+
+    TS_ASSERT(t->d_pContext == d_context);
+    TS_ASSERT(t->d_pCMM == d_context->d_pCMM);
+    TS_ASSERT(t->d_level == 1);
+    TS_ASSERT(t->d_pContextObjList == &a);
+
+    TS_ASSERT(a.d_pScope == t);
+    TS_ASSERT(a.d_pContextObjRestore != NULL);
+    TS_ASSERT(a.d_pContextObjNext == NULL);
+    TS_ASSERT(a.d_ppContextObjPrev == &t->d_pContextObjList);
+
+    b = 3;
+
+    TS_ASSERT(t->d_pContext == d_context);
+    TS_ASSERT(t->d_pCMM == d_context->d_pCMM);
+    TS_ASSERT(t->d_level == 1);
+    TS_ASSERT(t->d_pContextObjList == &b);
+
+    TS_ASSERT(a.d_pScope == t);
+    TS_ASSERT(a.d_pContextObjRestore != NULL);
+    TS_ASSERT(a.d_pContextObjNext == NULL);
+    TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext);
+
+    TS_ASSERT(b.d_pScope == t);
+    TS_ASSERT(b.d_pContextObjRestore != NULL);
+    TS_ASSERT(b.d_pContextObjNext == &a);
+    TS_ASSERT(b.d_ppContextObjPrev == &t->d_pContextObjList);
+
+    d_context->push();
+    Scope* u = d_context->getTopScope();
+    TS_ASSERT(u != t);
+    TS_ASSERT(u != s);
+
+    CDO<int> c(d_context);
+    c = 4;
+
+    TS_ASSERT(c.d_pScope == u);
+    TS_ASSERT(c.d_pContextObjRestore != NULL);
+    TS_ASSERT(c.d_pContextObjNext == NULL);
+    TS_ASSERT(c.d_ppContextObjPrev == &u->d_pContextObjList);
+
+    d_context->pop();
+
+    TS_ASSERT(t->d_pContext == d_context);
+    TS_ASSERT(t->d_pCMM == d_context->d_pCMM);
+    TS_ASSERT(t->d_level == 1);
+    TS_ASSERT(t->d_pContextObjList == &b);
+
+    TS_ASSERT(a.d_pScope == t);
+    TS_ASSERT(a.d_pContextObjRestore != NULL);
+    TS_ASSERT(a.d_pContextObjNext == NULL);
+    TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext);
+
+    TS_ASSERT(b.d_pScope == t);
+    TS_ASSERT(b.d_pContextObjRestore != NULL);
+    TS_ASSERT(b.d_pContextObjNext == &a);
+    //TS_ASSERT(b.d_ppContextObjPrev == &t->d_pContextObjList);// THIS ONE FAILS
+
+    d_context->pop();
+
+    TS_ASSERT(s->d_pContext == d_context);
+    TS_ASSERT(s->d_pCMM == d_context->d_pCMM);
+    TS_ASSERT(s->d_level == 0);
+    //TS_ASSERT(s->d_pContextObjList == &b);// THIS ONE FAILS
+
+    TS_ASSERT(a.d_pScope == s);
+    TS_ASSERT(a.d_pContextObjRestore == NULL);
+    TS_ASSERT(a.d_pContextObjNext == NULL);
+    TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext);
+
+    TS_ASSERT(b.d_pScope == s);
+    TS_ASSERT(b.d_pContextObjRestore == NULL);
+    TS_ASSERT(b.d_pContextObjNext == &a);
+    TS_ASSERT(b.d_ppContextObjPrev == &s->d_pContextObjList);
+  }
+};
diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index fb18601a3..64c768a13 100644
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -17,12 +17,14 @@
 
 #include <string>
 
+#include "context/context.h"
 #include "expr/node_value.h"
 #include "expr/node_builder.h"
 #include "expr/node_manager.h"
-#include "expr/node.h"
 #include "expr/attribute.h"
-#include "context/context.h"
+#include "expr/node.h"
+#include "theory/theory.h"
+#include "theory/uf/theory_uf.h"
 #include "util/Assert.h"
 
 using namespace CVC4;
@@ -74,24 +76,73 @@ public:
   }
 
   void testAttributeIds() {
-    TS_ASSERT(VarNameAttr::s_id == 0);
-    TS_ASSERT(TestStringAttr1::s_id == 1);
-    TS_ASSERT(TestStringAttr2::s_id == 2);
-    TS_ASSERT((attr::LastAttributeId<string, false>::s_id == 3));
-
-    TS_ASSERT(TypeAttr::s_id == 0);
-    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));
+    // Test that IDs for (a subset of) attributes in the system are
+    // unique and that the LastAttributeId (which would be the next ID
+    // to assign) is greater than all attribute IDs.
+
+    // We used to check ID assignments explicitly.  However, between
+    // compilation modules, you don't get a strong guarantee
+    // (initialization order is somewhat implementation-specific, and
+    // anyway you'd have to change the tests anytime you add an
+    // attribute).  So we back off, and just test that they're unique
+    // and that the next ID to be assigned is strictly greater than
+    // those that have already been assigned.
+
+    unsigned lastId = attr::LastAttributeId<string, false>::s_id;
+    TS_ASSERT_LESS_THAN(VarNameAttr::s_id, lastId);
+    TS_ASSERT_LESS_THAN(TestStringAttr1::s_id, lastId);
+    TS_ASSERT_LESS_THAN(TestStringAttr2::s_id, lastId);
+
+    TS_ASSERT_DIFFERS(VarNameAttr::s_id, TestStringAttr1::s_id);
+    TS_ASSERT_DIFFERS(VarNameAttr::s_id, TestStringAttr2::s_id);
+    TS_ASSERT_DIFFERS(TestStringAttr1::s_id, TestStringAttr2::s_id);
+
+    lastId = attr::LastAttributeId<void*, false>::s_id;
+    TS_ASSERT_LESS_THAN(NodeManager::TypeAttr::s_id, lastId);
+    TS_ASSERT_LESS_THAN(theory::uf::ECAttr::s_id, lastId);
+    TS_ASSERT_DIFFERS(NodeManager::TypeAttr::s_id, theory::uf::ECAttr::s_id);
+
+    lastId = attr::LastAttributeId<bool, false>::s_id;
+    TS_ASSERT_LESS_THAN(NodeManager::AtomicAttr::s_id, lastId);
+    TS_ASSERT_LESS_THAN(theory::Theory::PreRegisteredAttr::s_id, lastId);
+    TS_ASSERT_LESS_THAN(TestFlag1::s_id, lastId);
+    TS_ASSERT_LESS_THAN(TestFlag2::s_id, lastId);
+    TS_ASSERT_LESS_THAN(TestFlag3::s_id, lastId);
+    TS_ASSERT_LESS_THAN(TestFlag4::s_id, lastId);
+    TS_ASSERT_LESS_THAN(TestFlag5::s_id, lastId);
+    TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id,
+                      theory::Theory::PreRegisteredAttr::s_id);
+    TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, TestFlag1::s_id);
+    TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, TestFlag2::s_id);
+    TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, TestFlag3::s_id);
+    TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, TestFlag4::s_id);
+    TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, TestFlag5::s_id);
+    TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag1::s_id);
+    TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag2::s_id);
+    TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag3::s_id);
+    TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag4::s_id);
+    TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag5::s_id);
+    TS_ASSERT_DIFFERS(TestFlag1::s_id, TestFlag2::s_id);
+    TS_ASSERT_DIFFERS(TestFlag1::s_id, TestFlag3::s_id);
+    TS_ASSERT_DIFFERS(TestFlag1::s_id, TestFlag4::s_id);
+    TS_ASSERT_DIFFERS(TestFlag1::s_id, TestFlag5::s_id);
+    TS_ASSERT_DIFFERS(TestFlag2::s_id, TestFlag3::s_id);
+    TS_ASSERT_DIFFERS(TestFlag2::s_id, TestFlag4::s_id);
+    TS_ASSERT_DIFFERS(TestFlag2::s_id, TestFlag5::s_id);
+    TS_ASSERT_DIFFERS(TestFlag3::s_id, TestFlag4::s_id);
+    TS_ASSERT_DIFFERS(TestFlag3::s_id, TestFlag5::s_id);
+    TS_ASSERT_DIFFERS(TestFlag4::s_id, TestFlag5::s_id);
+
+    lastId = attr::LastAttributeId<bool, true>::s_id;
+    TS_ASSERT_LESS_THAN(theory::Theory::RegisteredAttr::s_id, lastId);
+    TS_ASSERT_LESS_THAN(TestFlag1cd::s_id, lastId);
+    TS_ASSERT_LESS_THAN(TestFlag2cd::s_id, lastId);
+    TS_ASSERT_DIFFERS(theory::Theory::RegisteredAttr::s_id, TestFlag1cd::s_id);
+    TS_ASSERT_DIFFERS(theory::Theory::RegisteredAttr::s_id, TestFlag2cd::s_id);
+    TS_ASSERT_DIFFERS(TestFlag1cd::s_id, TestFlag2cd::s_id);
+
+    lastId = attr::LastAttributeId<TNode, false>::s_id;
+    TS_ASSERT_LESS_THAN(theory::RewriteCache::s_id, lastId);
   }
 
   void testCDAttributes() {
diff --git a/test/unit/expr/expr_black.h b/test/unit/expr/expr_black.h
index e253b4a24..03d4ba31c 100644
--- a/test/unit/expr/expr_black.h
+++ b/test/unit/expr/expr_black.h
@@ -354,7 +354,9 @@ public:
     TS_ASSERT(mult->isAtomic());
     TS_ASSERT(plus->isAtomic());
     TS_ASSERT(d->isAtomic());
-    TS_ASSERT(!null->isAtomic());
+#ifdef CVC4_ASSERTIONS
+    TS_ASSERT_THROWS(null->isAtomic(), IllegalArgumentException);
+#endif /* CVC4_ASSERTIONS */
 
     TS_ASSERT(i1->isAtomic());
     TS_ASSERT(i2->isAtomic());
@@ -368,6 +370,12 @@ public:
     TS_ASSERT(!x.isAtomic());
     TS_ASSERT(!y.isAtomic());
     TS_ASSERT(!z.isAtomic());
+
+    Expr w1 = d_em->mkExpr(PLUS, d_em->mkExpr(ITE, z, *i1, *i2), *i2);
+    Expr w2 = d_em->mkExpr(PLUS, d_em->mkExpr(MULT, *i1, *i2), *i2);
+
+    TS_ASSERT(!w1.isAtomic());
+    TS_ASSERT(w2.isAtomic());
   }
 
   void testGetConst() {
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index 81aa424f8..2a7b3623e 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -244,9 +244,9 @@ public:
 
     Node n = noKind;
 
-#ifdef CVC4_DEBUG
-    TS_ASSERT_THROWS_ANYTHING(noKind.getKind(););
-#endif
+#ifdef CVC4_ASSERTIONS
+    TS_ASSERT_THROWS(noKind.getKind(), AssertionException);
+#endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<> spec(specKind);
     TS_ASSERT_EQUALS(spec.getKind(), specKind);
@@ -277,11 +277,11 @@ public:
     push_back(noKind, K);
     TS_ASSERT_EQUALS(noKind.getNumChildren(), K+K);
 
-#ifdef CVC4_DEBUG
+#ifdef CVC4_ASSERTIONS
     noKind << specKind;
     n = noKind;
-    TS_ASSERT_THROWS_ANYTHING( noKind.getNumChildren() );
-#endif
+    TS_ASSERT_THROWS( noKind.getNumChildren(), AssertionException );
+#endif /* CVC4_ASSERTIONS */
   }
 
   void testOperatorSquare() {
@@ -297,10 +297,10 @@ public:
     Node i_2 = d_nm->mkConst(true);
     Node i_K = d_nm->mkNode(NOT, i_0);
 
-#ifdef CVC4_DEBUG
-    TS_ASSERT_THROWS_ANYTHING(arr[-1];);
-    TS_ASSERT_THROWS_ANYTHING(arr[0];);
-#endif
+#ifdef CVC4_ASSERTIONS
+    TS_ASSERT_THROWS(arr[-1], AssertionException);
+    TS_ASSERT_THROWS(arr[0], AssertionException);
+#endif /* CVC4_ASSERTIONS */
 
     arr << i_0;
 
@@ -330,10 +330,10 @@ public:
     }
     TS_ASSERT_EQUALS(arr[K], i_K);
 
-#ifdef CVC4_DEBUG
+#ifdef CVC4_ASSERTIONS
     Node n = arr;
-    TS_ASSERT_THROWS_ANYTHING(arr[0]);
-#endif
+    TS_ASSERT_THROWS(arr[0], AssertionException);
+#endif /* CVC4_ASSERTIONS */
   }
 
   void testClear() {
@@ -469,6 +469,10 @@ public:
     Node p = d_nm->mkNode(PLUS, z, d_nm->mkNode(UMINUS, x), z);
     Node q = d_nm->mkNode(AND, x, z, d_nm->mkNode(NOT, y));
 
+#ifdef CVC4_ASSERTIONS
+    TS_ASSERT_THROWS(d_nm->mkNode(XOR, y, x, x), AssertionException);
+#endif /* CVC4_ASSERTIONS */
+
     NodeBuilder<> b;
 
     // test append(TNode)
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 427a22c9d..c6da48291 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -82,13 +82,13 @@ public:
   }
 };
 
-class DummyTheory : public TheoryImpl<DummyTheory> {
+class DummyTheory : public Theory {
 public:
   set<Node> d_registered;
   vector<Node> d_getSequence;
 
   DummyTheory(Context* ctxt, OutputChannel& out) :
-    TheoryImpl<DummyTheory>(ctxt, out) {
+    Theory(ctxt, out) {
   }
 
   void registerTerm(TNode n) {