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

76 files changed, 412 insertions, 60 deletions

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) {