18 files changed, 659 insertions, 150 deletions

diff --git a/Makefile.am b/Makefile.am
index 5aec4e904..c10bc1263 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -11,3 +11,48 @@ SUBDIRS = src test contrib
 regress0 regress1 regress2 regress3: all
 	(cd test && $(MAKE) $(AM_MAKEFLAGS) $@) || exit 1
 
+LCOV = lcov
+GENHTML = genhtml
+
+LCOV_EXCLUDES = \
+	"$(CXXTEST)/*" \
+	"/usr/include/*" \
+	"$(abs_top_builddir)/test/*"
+
+# lcov 1.7 has some bugs that we have to work around (can't do
+# baseline measurement, merge between different test-names doesn't
+# work...)
+.PHONY: lcov
+lcov: all
+	$(LCOV) -z -d .
+	$(MAKE) check -C test/unit
+	$(LCOV) -c -d . -t cvc4_units -o cvc4-coverage-full.info
+	$(LCOV) -o cvc4-coverage.info -r cvc4-coverage-full.info $(LCOV_EXCLUDES)
+	mkdir -p "@top_srcdir@/html"
+	$(GENHTML) -o "@top_srcdir@/html" cvc4-coverage.info
+	@echo "De-mangling C++ symbols..."
+	@find "@top_srcdir@/html" -name '*.func.html' | \
+		xargs perl -pi -e 's#(<td class="coverFn"><a href=".*">)(.*)(</a></td>)#$$_=`c++filt "$$2"`;chomp;print "$$1<xmp>$$_</xmp>$$3\n";#e'
+
+# when we get a working lcov, we can do better stats for
+# modules/test-types; unfortunately lcov 1.8 directory paths
+# are broken(?) or at least different than 1.7
+.PHONY: lcov18
+lcov18: all
+	@for testtype in public black white; do \
+		echo; echo "=== Collecting coverage data from $$testtype unit tests ==="; \
+		echo $(LCOV) -z -d .; \
+		$(LCOV) -z -d . || exit 1; \
+		echo $(MAKE) check -C test/unit TEST_SUFFIX=_$$testtype || exit 1; \
+		$(MAKE) check -C test/unit TEST_SUFFIX=_$$testtype || exit 1; \
+		echo $(LCOV) -c -d . -t $$testtype -o cvc4-coverage-$$testtype-full.info || exit 1; \
+		$(LCOV) -c -d . -t $$testtype -o cvc4-coverage-$$testtype-full.info || exit 1; \
+		echo $(LCOV) -o cvc4-coverage-$$testtype.info -r cvc4-coverage-$$testtype-full.info $(LCOV_EXCLUDES); \
+		$(LCOV) -o cvc4-coverage-$$testtype.info -r cvc4-coverage-$$testtype-full.info $(LCOV_EXCLUDES) || exit 1; \
+		echo; \
+	done
+	mkdir -p "@top_srcdir@/html"
+	$(GENHTML) -o "@top_srcdir@/html" cvc4-coverage-public.info cvc4-coverage-black.info cvc4-coverage-white.info
+	@echo "De-mangling C++ symbols..."
+	@find "@top_srcdir@/html" -name '*.func.html' | \
+		xargs perl -pi -e 's,(<td class="coverFn"><a href=".*">)(.*)(</a></td>),$$_=`c++filt "$$2"`;chomp;print "$$1<xmp>$$_</xmp>$$3";,e'
diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index b0161c562..a2abc08d8 100644
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -95,6 +95,7 @@ private:
   CDList(const CDList<T>& l) :
     ContextObj(l),
     d_list(NULL),
+    d_callDestructor(l.d_callDestructor),
     d_size(l.d_size),
     d_sizeAlloc(0) {
   }
diff --git a/src/context/cdmap.h b/src/context/cdmap.h
index 75f6eb2ae..4621d7fc5 100644
--- a/src/context/cdmap.h
+++ b/src/context/cdmap.h
@@ -140,24 +140,6 @@ public:
   }
 };/* class CDOmap<> */
 
-// Dummy subclass of ContextObj to serve as our data class
-class CDMapData : public ContextObj {
-  // befriend CDMap<> so that it can allocate us
-  template <class Key, class Data, class HashFcn>
-  friend class CDMap;
-
-  ContextObj* save(ContextMemoryManager* pCMM) {
-    return new(pCMM) CDMapData(*this);
-  }
-
-  void restore(ContextObj* data) {}
-
-public:
-
-  CDMapData(Context* context) : ContextObj(context) {}
-  CDMapData(const ContextObj& co) : ContextObj(co) {}
-  ~CDMapData() throw(AssertionException) { destroy(); }
-};
 
 /**
  * Generic templated class for a map which must be saved and restored
@@ -181,11 +163,13 @@ class CDMap : public ContextObj {
 
   // Nothing to save; the elements take care of themselves
   virtual ContextObj* save(ContextMemoryManager* pCMM) {
-    return new(pCMM) CDMapData(*this);
+    Unreachable();
   }
 
   // Similarly, nothing to restore
-  virtual void restore(ContextObj* data) {}
+  virtual void restore(ContextObj* data) {
+    Unreachable();
+  }
 
   void emptyTrash() {
     //FIXME multithreading
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 96152d075..fda2801be 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -199,7 +199,6 @@ inline bool NodeValueConstCompare<k, pool>::compare(const ::CVC4::expr::NodeValu
     if(x->d_nchildren == 1) {
       Assert(y->d_nchildren == 0);
       return compare(y, x);
-      return *reinterpret_cast<T*>(x->d_children[0]) == y->getConst<T>();
     } else if(y->d_nchildren == 1) {
       Assert(x->d_nchildren == 0);
       return x->getConst<T>() == *reinterpret_cast<T*>(y->d_children[0]);
diff --git a/src/util/output.h b/src/util/output.h
index 6315389e8..79bdd788e 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -172,8 +172,8 @@ class CVC4_PUBLIC NoticeC {
 public:
   NoticeC(std::ostream* os) : d_os(os) {}
 
-  void operator()(const char*);
-  void operator()(std::string);
+  void operator()(const char* s) { *d_os << s; }
+  void operator()(std::string s) { *d_os << s; }
 
   void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
 
@@ -193,8 +193,8 @@ class CVC4_PUBLIC ChatC {
 public:
   ChatC(std::ostream* os) : d_os(os) {}
 
-  void operator()(const char*);
-  void operator()(std::string);
+  void operator()(const char* s) { *d_os << s; }
+  void operator()(std::string s) { *d_os << s; }
 
   void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
 
@@ -215,10 +215,29 @@ class CVC4_PUBLIC TraceC {
 public:
   TraceC(std::ostream* os) : d_os(os) {}
 
-  void operator()(const char* tag, const char*);
-  void operator()(const char* tag, std::string);
-  void operator()(std::string tag, const char*);
-  void operator()(std::string tag, std::string);
+  void operator()(const char* tag, const char* s) {
+    if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) {
+      *d_os << s;
+    }
+  }
+
+  void operator()(const char* tag, const std::string& s) {
+    if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) {
+      *d_os << s;
+    }
+  }
+
+  void operator()(const std::string& tag, const char* s) {
+    if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
+      *d_os << s;
+    }
+  }
+
+  void operator()(const std::string& tag, const std::string& s) {
+    if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
+      *d_os << s;
+    }
+  }
 
   void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
   void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index c52ac5d1c..3f0816560 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -1,6 +1,6 @@
 # All unit tests
 UNIT_TESTS = \
-	expr/expr_black \
+	expr/expr_public \
 	expr/node_white \
 	expr/node_black \
 	expr/kind_black \
@@ -16,11 +16,13 @@ UNIT_TESTS = \
 	context/cdo_black \
 	context/cdlist_black \
 	context/cdmap_black \
+	context/cdmap_white \
 	theory/theory_black \
 	theory/theory_uf_white \
 	util/assert_white \
-	util/configuration_white \
-	util/output_white \
+	util/configuration_black \
+	util/output_black \
+	util/exception_black \
 	util/integer_black \
 	util/integer_white \
 	util/rational_white
diff --git a/test/unit/Makefile.tests b/test/unit/Makefile.tests
index 4f2f3dd5f..e3ec536ce 100644
--- a/test/unit/Makefile.tests
+++ b/test/unit/Makefile.tests
@@ -8,7 +8,7 @@
 # It's a pain to make automake happy.
 
 # Add "filtered" tests to the set of TESTS
-TESTS = $(filter $(TEST_PREFIX)%,$(UNIT_TESTS))
+TESTS = $(filter $(TEST_PREFIX)%,$(filter %$(TEST_SUFFIX),$(UNIT_TESTS)))
 
 # subsets of the tests, based on name
 WHITE_TESTS = $(filter %_white,$(UNIT_TESTS))
diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h
index f31d5f273..418357630 100644
--- a/test/unit/context/cdlist_black.h
+++ b/test/unit/context/cdlist_black.h
@@ -23,6 +23,14 @@
 using namespace std;
 using namespace CVC4::context;
 
+
+struct DtorSensitiveObject {
+  bool& d_dtorCalled;
+  DtorSensitiveObject(bool& dtorCalled) : d_dtorCalled(dtorCalled) {}
+  ~DtorSensitiveObject() { d_dtorCalled = true; }
+};
+
+
 class CDListBlack : public CxxTest::TestSuite {
 private:
 
@@ -34,6 +42,10 @@ public:
     d_context = new Context();
   }
 
+  void tearDown() {
+    delete d_context;
+  }
+
   // test at different sizes.  this triggers grow() behavior differently.
   // grow() was completely broken in revision 256
   void testCDList10() { listTest(10); }
@@ -44,7 +56,12 @@ public:
   void testCDList99() { listTest(99); }
 
   void listTest(int N) {
-    CDList<int> list(d_context);
+    listTest(N, true);
+    listTest(N, false);
+  }
+
+  void listTest(int N, bool callDestructor) {
+    CDList<int> list(d_context, callDestructor);
 
     TS_ASSERT(list.empty());
     for(int i = 0; i < N; ++i) {
@@ -66,7 +83,46 @@ public:
     }
   }
 
-  void tearDown() {
-    delete d_context;
+  void testDtorCalled() {
+    bool shouldRemainFalse = false;
+    bool shouldFlipToTrue = false;
+    bool alsoFlipToTrue = false;
+    bool shouldAlsoRemainFalse = false;
+    bool aThirdFalse = false;
+
+    CDList<DtorSensitiveObject> listT(d_context, true);
+    CDList<DtorSensitiveObject> listF(d_context, false);
+
+    DtorSensitiveObject shouldRemainFalseDSO(shouldRemainFalse);
+    DtorSensitiveObject shouldFlipToTrueDSO(shouldFlipToTrue);
+    DtorSensitiveObject alsoFlipToTrueDSO(alsoFlipToTrue);
+    DtorSensitiveObject shouldAlsoRemainFalseDSO(shouldAlsoRemainFalse);
+    DtorSensitiveObject aThirdFalseDSO(aThirdFalse);
+
+    listT.push_back(shouldAlsoRemainFalseDSO);
+    listF.push_back(shouldAlsoRemainFalseDSO);
+
+    d_context->push();
+
+    listT.push_back(shouldFlipToTrueDSO);
+    listT.push_back(alsoFlipToTrueDSO);
+
+    listF.push_back(shouldRemainFalseDSO);
+    listF.push_back(shouldAlsoRemainFalseDSO);
+    listF.push_back(aThirdFalseDSO);
+
+    TS_ASSERT_EQUALS(shouldRemainFalse, false);
+    TS_ASSERT_EQUALS(shouldFlipToTrue, false);
+    TS_ASSERT_EQUALS(alsoFlipToTrue, false);
+    TS_ASSERT_EQUALS(shouldAlsoRemainFalse, false);
+    TS_ASSERT_EQUALS(aThirdFalse, false);
+
+    d_context->pop();
+
+    TS_ASSERT_EQUALS(shouldRemainFalse, false);
+    TS_ASSERT_EQUALS(shouldFlipToTrue, true);
+    TS_ASSERT_EQUALS(alsoFlipToTrue, true);
+    TS_ASSERT_EQUALS(shouldAlsoRemainFalse, false);
+    TS_ASSERT_EQUALS(aThirdFalse, false);
   }
 };
diff --git a/test/unit/context/cdmap_white.h b/test/unit/context/cdmap_white.h
new file mode 100644
index 000000000..9a920ede8
--- /dev/null
+++ b/test/unit/context/cdmap_white.h
@@ -0,0 +1,52 @@
+/*********************                                                        */
+/** cdmap_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::CDMap<>.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "context/cdmap.h"
+#include "util/Assert.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::context;
+
+class CDMapWhite : public CxxTest::TestSuite {
+
+  Context* d_context;
+
+public:
+
+  void setUp() {
+    d_context = new Context;
+  }
+
+  void tearDown() {
+    delete d_context;
+  }
+
+  void testUnreachableSaveAndRestore() {
+    CDMap<int, int> map(d_context);
+
+    TS_ASSERT_THROWS_NOTHING(map.makeCurrent());
+
+    TS_ASSERT_THROWS(map.update(), UnreachableCodeException);
+
+    TS_ASSERT_THROWS(map.save(d_context->getCMM()), UnreachableCodeException);
+    TS_ASSERT_THROWS(map.restore(&map), UnreachableCodeException);
+
+    d_context->push();
+    TS_ASSERT_THROWS(map.makeCurrent(), UnreachableCodeException);
+  }
+};
diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h
index 549d99369..37c94aaad 100644
--- a/test/unit/context/context_black.h
+++ b/test/unit/context/context_black.h
@@ -60,4 +60,55 @@ public:
     d_context->push();
     i = 5;
   }
+
+  void testPreNotify() {
+    struct MyContextNotifyObj : ContextNotifyObj {
+      int nCalls;
+
+      MyContextNotifyObj(Context* context, bool pre) :
+        ContextNotifyObj(context, pre),
+        nCalls(0) {
+      }
+
+      void notify() {
+        ++nCalls;
+      }
+    } a(d_context, true), b(d_context, false);
+
+    {
+      MyContextNotifyObj c(d_context, true), d(d_context, false);
+
+      TS_ASSERT_EQUALS(a.nCalls, 0);
+      TS_ASSERT_EQUALS(b.nCalls, 0);
+      TS_ASSERT_EQUALS(c.nCalls, 0);
+      TS_ASSERT_EQUALS(d.nCalls, 0);
+
+      d_context->push();
+      d_context->push();
+
+      TS_ASSERT_EQUALS(a.nCalls, 0);
+      TS_ASSERT_EQUALS(b.nCalls, 0);
+      TS_ASSERT_EQUALS(c.nCalls, 0);
+      TS_ASSERT_EQUALS(d.nCalls, 0);
+
+      d_context->pop();
+
+      TS_ASSERT_EQUALS(a.nCalls, 1);
+      TS_ASSERT_EQUALS(b.nCalls, 1);
+      TS_ASSERT_EQUALS(c.nCalls, 1);
+      TS_ASSERT_EQUALS(d.nCalls, 1);
+
+      d_context->pop();
+
+      TS_ASSERT_EQUALS(a.nCalls, 2);
+      TS_ASSERT_EQUALS(b.nCalls, 2);
+      TS_ASSERT_EQUALS(c.nCalls, 2);
+      TS_ASSERT_EQUALS(d.nCalls, 2);
+    }
+
+    // we do this to get full code coverage of destruction paths
+    delete d_context;
+
+    d_context = NULL;
+  }
 };
diff --git a/test/unit/expr/expr_black.h b/test/unit/expr/expr_public.h
index 936381cd6..fd36a7cfa 100644
--- a/test/unit/expr/expr_black.h
+++ b/test/unit/expr/expr_public.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/** expr_black.h
+/** expr_public.h
  ** Original author: mdeters
  ** Major contributors: none
  ** Minor contributors (to current version): none
@@ -10,7 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** Black box testing of CVC4::Expr.
+ ** Public black-box testing of CVC4::Expr.
  **/
 
 #include <cxxtest/TestSuite.h>
@@ -27,7 +27,7 @@ using namespace CVC4;
 using namespace CVC4::kind;
 using namespace std;
 
-class ExprBlack : public CxxTest::TestSuite {
+class ExprPublic : public CxxTest::TestSuite {
 private:
 
   ExprManager* d_em;
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 24c8e407c..097724d48 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -243,7 +243,7 @@ public:
 
     TS_ASSERT_EQUALS(got, x_eq_f_f_x);
 
-    TS_ASSERT_EQUALS(7, d_dummy->d_registered.size());
+    TS_ASSERT_EQUALS(7u, d_dummy->d_registered.size());
     TS_ASSERT(d_dummy->d_registered.find(f_f_x) != d_dummy->d_registered.end());
     TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) != d_dummy->d_registered.end());
 
diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h
index c02214a25..f5da06a0b 100644
--- a/test/unit/theory/theory_uf_white.h
+++ b/test/unit/theory/theory_uf_white.h
@@ -154,13 +154,13 @@ public:
     d_euf->check(d_level);
 
     //Test that no additional calls to the output channel occurred.
-    TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls());
+    TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls());
 
     d_euf->assertFact( f5_x_eq_x );
 
     d_euf->check(d_level);
 
-    TS_ASSERT_EQUALS(2, d_outputChannel.getNumCalls());
+    TS_ASSERT_EQUALS(2u, d_outputChannel.getNumCalls());
     TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0));
     TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(1));
     Node  firstConflict = d_outputChannel.getIthNode(0);
@@ -189,7 +189,7 @@ public:
     d_euf->assertFact(f_f_f_x_neq_f_x);
     d_euf->check(d_level);
 
-    TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls());
+    TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls());
     TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0));
 
     Node realConflict = d_outputChannel.getIthNode(0);
@@ -205,7 +205,7 @@ public:
     d_euf->assertFact(x_neq_x);
     d_euf->check(d_level);
 
-    TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls());
+    TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls());
     TS_ASSERT_EQUALS(x_neq_x, d_outputChannel.getIthNode(0));
     TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0));
   }
@@ -218,7 +218,7 @@ public:
     d_euf->assertFact(x_eq_x);
     d_euf->check(d_level);
 
-    TS_ASSERT_EQUALS(0, d_outputChannel.getNumCalls());
+    TS_ASSERT_EQUALS(0u, d_outputChannel.getNumCalls());
   }
 
 
@@ -251,7 +251,7 @@ public:
     d_euf->assertFact( f1_x_neq_x );
     d_euf->check(d_level);
 
-    TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls());
+    TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls());
     TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0));
     Node realConflict = d_outputChannel.getIthNode(0);
     TS_ASSERT_EQUALS(expectedConflict, realConflict);
@@ -282,7 +282,4 @@ public:
     d_euf->check(d_level);
   }
 
-
-
-
 };
diff --git a/test/unit/util/assert_white.h b/test/unit/util/assert_white.h
index 9425daa44..d001c5a84 100644
--- a/test/unit/util/assert_white.h
+++ b/test/unit/util/assert_white.h
@@ -15,6 +15,9 @@
 
 #include <cxxtest/TestSuite.h>
 
+#include <string>
+#include <cstring>
+
 #include "util/Assert.h"
 
 using namespace CVC4;
@@ -39,9 +42,44 @@ public:
     TS_ASSERT_THROWS( Unimplemented(), UnimplementedOperationException );
     TS_ASSERT_THROWS( IllegalArgument("x"), IllegalArgumentException );
     TS_ASSERT_THROWS( CheckArgument(false, "x"), IllegalArgumentException );
-    TS_ASSERT_THROWS( AlwaysAssertArgument(false, "x"), IllegalArgumentException );
+    TS_ASSERT_THROWS( AlwaysAssertArgument(false, "x"),
+                      IllegalArgumentException );
     TS_ASSERT_THROWS_NOTHING( AssertArgument(true, "x") );
     TS_ASSERT_THROWS_NOTHING( AssertArgument(true, "x") );
   }
 
+  void testReallyLongAssert() {
+    string msg(1034, 'x');
+    try {
+      AlwaysAssert(false, msg.c_str());
+      TS_FAIL("Should have thrown an exception !");
+    } catch(AssertionException& e) {
+      // we don't want to match on the entire string, because it may
+      // have an absolute path to the unit test binary, line number
+      // info, etc.
+      const char* theString = e.toString().c_str();
+      const char* firstPart =
+        "Assertion failure\nvoid AssertWhite::testReallyLongAssert()\n";
+      string lastPartStr = "\n\n  false\n" + msg;
+      const char* lastPart = lastPartStr.c_str();
+      TS_ASSERT(strncmp(theString, firstPart, strlen(firstPart)) == 0);
+      TS_ASSERT(strncmp(theString + strlen(theString) - strlen(lastPart),
+                        lastPart, strlen(lastPart)) == 0);
+    } catch(...) {
+      TS_FAIL("Threw the wrong kind of exception !");
+    }
+  }
+
+  void testUnreachable() {
+    TS_ASSERT_THROWS( Unreachable(), UnreachableCodeException );
+    TS_ASSERT_THROWS( Unreachable("hello"), UnreachableCodeException );
+    TS_ASSERT_THROWS( Unreachable("hello %s", "world"), UnreachableCodeException );
+
+    int x = 5;
+    TS_ASSERT_THROWS( Unhandled(), UnhandledCaseException );
+    TS_ASSERT_THROWS( Unhandled(x), UnhandledCaseException );
+    TS_ASSERT_THROWS( Unhandled("foo"), UnhandledCaseException );
+    TS_ASSERT_THROWS( Unhandled("foo %s baz", "bar"), UnhandledCaseException );
+  }
+
 };
diff --git a/test/unit/util/configuration_white.h b/test/unit/util/configuration_black.h
index 04cacc155..5ee4cf095 100644
--- a/test/unit/util/configuration_white.h
+++ b/test/unit/util/configuration_black.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/** configuration_white.h
+/** configuration_black.h
  ** Original author: mdeters
  ** Major contributors: none
  ** Minor contributors (to current version): none
@@ -10,7 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** White box testing of CVC4::Configuration.
+ ** Black box testing of CVC4::Configuration.
  **/
 
 #include <cxxtest/TestSuite.h>
@@ -20,7 +20,7 @@
 using namespace CVC4;
 using namespace std;
 
-class ConfigurationWhite : public CxxTest::TestSuite {
+class ConfigurationBlack : public CxxTest::TestSuite {
 
 public:
 
diff --git a/test/unit/util/exception_black.h b/test/unit/util/exception_black.h
new file mode 100644
index 000000000..758a12645
--- /dev/null
+++ b/test/unit/util/exception_black.h
@@ -0,0 +1,58 @@
+/*********************                                                        */
+/** exception_black.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.
+ **
+ ** Black box testing of CVC4::Exception.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include <iostream>
+#include <sstream>
+
+#include "util/exception.h"
+
+using namespace CVC4;
+using namespace std;
+
+class ExceptionBlack : public CxxTest::TestSuite {
+public:
+
+  void setUp() {
+  }
+
+  void tearDown() {
+  }
+
+  // CVC4::Exception is a simple class, just test it all at once.
+  void testExceptions() {
+    Exception e1;
+    Exception e2(string("foo!"));
+    Exception e3("bar!");
+
+    TS_ASSERT_EQUALS(e1.toString(), string("Unknown exception"));
+    TS_ASSERT_EQUALS(e2.toString(), string("foo!"));
+    TS_ASSERT_EQUALS(e3.toString(), string("bar!"));
+
+    e1.setMessage("blah");
+    e2.setMessage("another");
+    e3.setMessage("three of 'em!");
+
+    stringstream s1, s2, s3;
+    s1 << e1;
+    s2 << e2;
+    s3 << e3;
+
+    TS_ASSERT_EQUALS(s1.str(), string("blah"));
+    TS_ASSERT_EQUALS(s2.str(), string("another"));
+    TS_ASSERT_EQUALS(s3.str(), string("three of 'em!"));
+  }
+};
diff --git a/test/unit/util/output_black.h b/test/unit/util/output_black.h
new file mode 100644
index 000000000..6e613e9f4
--- /dev/null
+++ b/test/unit/util/output_black.h
@@ -0,0 +1,304 @@
+/*********************                                                        */
+/** output_black.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.
+ **
+ ** Black box testing of CVC4 output classes.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include <iostream>
+#include <sstream>
+
+#include "util/output.h"
+
+using namespace CVC4;
+using namespace std;
+
+class OutputBlack : public CxxTest::TestSuite {
+
+  stringstream d_debugStream;
+  stringstream d_traceStream;
+  stringstream d_noticeStream;
+  stringstream d_chatStream;
+  stringstream d_messageStream;
+  stringstream d_warningStream;
+
+public:
+
+  void setUp() {
+    Debug.setStream(d_debugStream);
+    Trace.setStream(d_traceStream);
+    Notice.setStream(d_noticeStream);
+    Chat.setStream(d_chatStream);
+    Message.setStream(d_messageStream);
+    Warning.setStream(d_warningStream);
+
+    d_debugStream.str("");
+    d_traceStream.str("");
+    d_noticeStream.str("");
+    d_chatStream.str("");
+    d_messageStream.str("");
+    d_warningStream.str("");
+  }
+
+  void tearDown() {
+  }
+
+  void testOutput() {
+    Debug.on("foo");
+    Debug("foo") << "testing1";
+    Debug.off("foo");
+    Debug("foo") << "testing2";
+    Debug.on("foo");
+    Debug("foo") << "testing3";
+
+    Message() << "a message";
+    Warning() << "bad warning!";
+    Chat() << "chatty";
+    Notice() << "note";
+
+    Trace.on("foo");
+    Trace("foo") << "tracing1";
+    Trace.off("foo");
+    Trace("foo") << "tracing2";
+    Trace.on("foo");
+    Trace("foo") << "tracing3";
+
+#ifdef CVC4_MUZZLE
+
+    TS_ASSERT( d_debugStream.str() == "" );
+    TS_ASSERT( d_messageStream.str() == "" );
+    TS_ASSERT( d_warningStream.str() == "" );
+    TS_ASSERT( d_chatStream.str() == "" );
+    TS_ASSERT( d_noticeStream.str() == "" );
+    TS_ASSERT( d_traceStream.str() == "" );
+
+#else /* CVC4_MUZZLE */
+
+#  ifdef CVC4_DEBUG
+    TS_ASSERT( d_debugStream.str() == "testing1testing3" );
+#  else /* CVC4_DEBUG */
+    TS_ASSERT( d_debugStream.str() == "" );
+#  endif /* CVC4_DEBUG */
+
+    TS_ASSERT( d_messageStream.str() == "a message" );
+    TS_ASSERT( d_warningStream.str() == "bad warning!" );
+    TS_ASSERT( d_chatStream.str() == "chatty" );
+    TS_ASSERT( d_noticeStream.str() == "note" );
+
+#  ifdef CVC4_TRACING
+    TS_ASSERT( d_traceStream.str() == "tracing1tracing3" );
+#  else /* CVC4_TRACING */
+    TS_ASSERT( d_traceStream.str() == "" );
+#  endif /* CVC4_TRACING */
+
+#endif /* CVC4_MUZZLE */
+  }
+
+  void testPrintf() {
+
+#ifdef CVC4_MUZZLE
+
+    Debug.off("yo");
+    Debug.printf("yo", "hello %s", "world");
+    TS_ASSERT_EQUALS(d_debugStream.str(), string());
+    d_debugStream.str("");
+    Debug.printf(string("yo"), "hello %s", "world");
+    TS_ASSERT_EQUALS(d_debugStream.str(), string());
+    d_debugStream.str("");
+
+    Debug.on("yo");
+    Debug.printf("yo", "hello %s", "world");
+    TS_ASSERT_EQUALS(d_debugStream.str(), string());
+    d_debugStream.str("");
+    Debug.printf(string("yo"), "hello %s", "world");
+    TS_ASSERT_EQUALS(d_debugStream.str(), string());
+    d_debugStream.str("");
+
+    Trace.off("yo");
+    Trace.printf("yo", "hello %s", "world");
+    TS_ASSERT_EQUALS(d_traceStream.str(), string());
+    d_traceStream.str("");
+    Trace.printf(string("yo"), "hello %s", "world");
+    TS_ASSERT_EQUALS(d_traceStream.str(), string());
+    d_traceStream.str("");
+
+    Trace.on("yo");
+    Trace.printf("yo", "hello %s", "world");
+    TS_ASSERT_EQUALS(d_traceStream.str(), string());
+    d_traceStream.str("");
+    Trace.printf(string("yo"), "hello %s", "world");
+    TS_ASSERT_EQUALS(d_traceStream.str(), string());
+
+    Warning.printf("hello %s", "world");
+    TS_ASSERT_EQUALS(d_warningStream.str(), string());
+
+    Chat.printf("hello %s", "world");
+    TS_ASSERT_EQUALS(d_chatStream.str(), string());
+
+    Message.printf("hello %s", "world");
+    TS_ASSERT_EQUALS(d_messageStream.str(), string());
+
+    Notice.printf("hello %s", "world");
+    TS_ASSERT_EQUALS(d_noticeStream.str(), string());
+
+#else /* CVC4_MUZZLE */
+
+    Debug.off("yo");
+    Debug.printf("yo", "hello %s", "world");
+    TS_ASSERT_EQUALS(d_debugStream.str(), string());
+    d_debugStream.str("");
+    Debug.printf(string("yo"), "hello %s", "world");
+    TS_ASSERT_EQUALS(d_debugStream.str(), string());
+    d_debugStream.str("");
+
+    Debug.on("yo");
+    Debug.printf("yo", "hello %s", "world");
+#ifdef CVC4_DEBUG
+    TS_ASSERT_EQUALS(d_debugStream.str(), string("hello world"));
+#else /* CVC4_DEBUG */
+    TS_ASSERT_EQUALS(d_debugStream.str(), string());
+#endif /* CVC4_DEBUG */
+    d_debugStream.str("");
+    Debug.printf(string("yo"), "hello %s", "world");
+#ifdef CVC4_DEBUG
+    TS_ASSERT_EQUALS(d_debugStream.str(), string("hello world"));
+#else /* CVC4_DEBUG */
+    TS_ASSERT_EQUALS(d_debugStream.str(), string());
+#endif /* CVC4_DEBUG */
+    d_debugStream.str("");
+
+    Trace.off("yo");
+    Trace.printf("yo", "hello %s", "world");
+    TS_ASSERT_EQUALS(d_traceStream.str(), string());
+    d_traceStream.str("");
+    Trace.printf(string("yo"), "hello %s", "world");
+    TS_ASSERT_EQUALS(d_traceStream.str(), string());
+    d_traceStream.str("");
+
+    Trace.on("yo");
+    Trace.printf("yo", "hello %s", "world");
+#ifdef CVC4_TRACING
+    TS_ASSERT_EQUALS(d_traceStream.str(), string("hello world"));
+#else /* CVC4_TRACING */
+    TS_ASSERT_EQUALS(d_traceStream.str(), string());
+#endif /* CVC4_TRACING */
+    d_traceStream.str("");
+    Trace.printf(string("yo"), "hello %s", "world");
+#ifdef CVC4_TRACING
+    TS_ASSERT_EQUALS(d_traceStream.str(), string("hello world"));
+#else /* CVC4_TRACING */
+    TS_ASSERT_EQUALS(d_traceStream.str(), string());
+#endif /* CVC4_TRACING */
+
+    Warning.printf("hello %s", "world");
+    TS_ASSERT_EQUALS(d_warningStream.str(), string("hello world"));
+
+    Chat.printf("hello %s", "world");
+    TS_ASSERT_EQUALS(d_chatStream.str(), string("hello world"));
+
+    Message.printf("hello %s", "world");
+    TS_ASSERT_EQUALS(d_messageStream.str(), string("hello world"));
+
+    Notice.printf("hello %s", "world");
+    TS_ASSERT_EQUALS(d_noticeStream.str(), string("hello world"));
+
+#endif /* CVC4_MUZZLE */
+
+  }
+
+  void testSimplePrint() {
+
+#ifdef CVC4_MUZZLE
+
+    Debug.off("yo");
+    Debug("yo", "foobar");
+    TS_ASSERT_EQUALS(d_debugStream.str(), string());
+    d_debugStream.str("");
+    Debug.on("yo");
+    Debug("yo", "baz foo");
+    TS_ASSERT_EQUALS(d_debugStream.str(), string());
+    d_debugStream.str("");
+
+    Trace.off("yo");
+    Trace("yo", "foobar");
+    TS_ASSERT_EQUALS(d_traceStream.str(), string());
+    d_traceStream.str("");
+    Trace.on("yo");
+    Trace("yo", "baz foo");
+    TS_ASSERT_EQUALS(d_traceStream.str(), string());
+    d_traceStream.str("");
+
+    Warning("baz foo");
+    TS_ASSERT_EQUALS(d_warningStream.str(), string());
+    d_warningStream.str("");
+
+    Chat("baz foo");
+    TS_ASSERT_EQUALS(d_chatStream.str(), string());
+    d_chatStream.str("");
+
+    Message("baz foo");
+    TS_ASSERT_EQUALS(d_messageStream.str(), string());
+    d_messageStream.str("");
+
+    Notice("baz foo");
+    TS_ASSERT_EQUALS(d_noticeStream.str(), string());
+    d_noticeStream.str("");
+
+#else /* CVC4_MUZZLE */
+
+    Debug.off("yo");
+    Debug("yo", "foobar");
+    TS_ASSERT_EQUALS(d_debugStream.str(), string());
+    d_debugStream.str("");
+    Debug.on("yo");
+    Debug("yo", "baz foo");
+#  ifdef CVC4_DEBUG
+    TS_ASSERT_EQUALS(d_debugStream.str(), string("baz foo"));
+#  else /* CVC4_DEBUG */
+    TS_ASSERT_EQUALS(d_debugStream.str(), string());
+#  endif /* CVC4_DEBUG */
+    d_debugStream.str("");
+
+    Trace.off("yo");
+    Trace("yo", "foobar");
+    TS_ASSERT_EQUALS(d_traceStream.str(), string());
+    d_traceStream.str("");
+    Trace.on("yo");
+    Trace("yo", "baz foo");
+#  ifdef CVC4_TRACING
+    TS_ASSERT_EQUALS(d_traceStream.str(), string("baz foo"));
+#  else /* CVC4_TRACING */
+    TS_ASSERT_EQUALS(d_traceStream.str(), string());
+#  endif /* CVC4_TRACING */
+    d_traceStream.str("");
+
+    Warning("baz foo");
+    TS_ASSERT_EQUALS(d_warningStream.str(), string("baz foo"));
+    d_warningStream.str("");
+
+    Chat("baz foo");
+    TS_ASSERT_EQUALS(d_chatStream.str(), string("baz foo"));
+    d_chatStream.str("");
+
+    Message("baz foo");
+    TS_ASSERT_EQUALS(d_messageStream.str(), string("baz foo"));
+    d_messageStream.str("");
+
+    Notice("baz foo");
+    TS_ASSERT_EQUALS(d_noticeStream.str(), string("baz foo"));
+    d_noticeStream.str("");
+
+#endif /* CVC4_MUZZLE */
+
+  }
+};
diff --git a/test/unit/util/output_white.h b/test/unit/util/output_white.h
deleted file mode 100644
index 7eda3db9d..000000000
--- a/test/unit/util/output_white.h
+++ /dev/null
@@ -1,97 +0,0 @@
-/*********************                                                        */
-/** output_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::Configuration.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include <iostream>
-#include <sstream>
-
-#include "util/output.h"
-
-using namespace CVC4;
-using namespace std;
-
-class OutputWhite : public CxxTest::TestSuite {
-
-  stringstream d_debugStream;
-  stringstream d_traceStream;
-  stringstream d_noticeStream;
-  stringstream d_chatStream;
-  stringstream d_messageStream;
-  stringstream d_warningStream;
-
-public:
-
-  void setUp() {
-    Debug.setStream(d_debugStream);
-    Trace.setStream(d_traceStream);
-    Notice.setStream(d_noticeStream);
-    Chat.setStream(d_chatStream);
-    Message.setStream(d_messageStream);
-    Warning.setStream(d_warningStream);
-  }
-
-  void testOutput() {
-    Debug.on("foo");
-    Debug("foo") << "testing1";
-    Debug.off("foo");
-    Debug("foo") << "testing2";
-    Debug.on("foo");
-    Debug("foo") << "testing3";
-
-    Message() << "a message";
-    Warning() << "bad warning!";
-    Chat() << "chatty";
-    Notice() << "note";
-
-    Trace.on("foo");
-    Trace("foo") << "tracing1";
-    Trace.off("foo");
-    Trace("foo") << "tracing2";
-    Trace.on("foo");
-    Trace("foo") << "tracing3";
-
-#ifdef CVC4_MUZZLE
-
-    TS_ASSERT( d_debugStream.str() == "" );
-    TS_ASSERT( d_messageStream.str() == "" );
-    TS_ASSERT( d_warningStream.str() == "" );
-    TS_ASSERT( d_chatStream.str() == "" );
-    TS_ASSERT( d_noticeStream.str() == "" );
-    TS_ASSERT( d_traceStream.str() == "" );
-
-#else /* CVC4_MUZZLE */
-
-#  ifdef CVC4_DEBUG
-    TS_ASSERT( d_debugStream.str() == "testing1testing3" );
-#  else /* CVC4_DEBUG */
-    TS_ASSERT( d_debugStream.str() == "" );
-#  endif /* CVC4_DEBUG */
-
-    TS_ASSERT( d_messageStream.str() == "a message" );
-    TS_ASSERT( d_warningStream.str() == "bad warning!" );
-    TS_ASSERT( d_chatStream.str() == "chatty" );
-    TS_ASSERT( d_noticeStream.str() == "note" );
-
-#  ifdef CVC4_TRACING
-    TS_ASSERT( d_traceStream.str() == "tracing1tracing3" );
-#  else /* CVC4_TRACING */
-    TS_ASSERT( d_traceStream.str() == "" );
-#  endif /* CVC4_TRACING */
-
-#endif /* CVC4_MUZZLE */
-  }
-
-};