* 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.

35 files changed, 348 insertions, 288 deletions

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,36 +38,22 @@ 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.
    */
   Theory();
@@ -110,13 +96,23 @@ 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");
 }