Add Valuation::getSatValue() so that theories can access the current

(propositional) assignment for theory atoms.

Fixed Debug/Trace as discussed in bug ticket #252 and on the mailing list.
This implementation leads to some compiler warnings in production builds,
but these will be corrected in coming days.  There appears to be a small
speedup in the parser as a result of this fix:

  http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=1902&reference_id=1886&p=5

Cleaned up a few CD Boolean attribute things.

Various small fixes to coding guidelines / test coverage.

This commit:
* Resolves bug 252 (tracing not disabled in production builds)
* Resolves bug 254 (implement CDAttrHash<>::BitIterator::find())

4 files changed, 273 insertions, 130 deletions

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index c732ffbb2..83291eb5a 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -52,6 +52,7 @@ CVC_TESTS = \
 	test9.cvc \
 	test11.cvc \
 	uf20-03.cvc \
+	uf20-03.tim.cvc \
 	wiki.01.cvc \
 	wiki.02.cvc \
 	wiki.03.cvc \
diff --git a/test/regress/regress0/uf20-03.tim.cvc b/test/regress/regress0/uf20-03.tim.cvc
new file mode 100644
index 000000000..f13bdcce5
--- /dev/null
+++ b/test/regress/regress0/uf20-03.tim.cvc
@@ -0,0 +1,117 @@
+% COMMAND-LINE: --uf=tim
+% EXPECT: invalid
+x_1 : BOOLEAN;
+x_2 : BOOLEAN;
+x_3 : BOOLEAN;
+x_4 : BOOLEAN;
+x_5 : BOOLEAN;
+x_6 : BOOLEAN;
+x_7 : BOOLEAN;
+x_8 : BOOLEAN;
+x_9 : BOOLEAN;
+x_10 : BOOLEAN;
+x_11 : BOOLEAN;
+x_12 : BOOLEAN;
+x_13 : BOOLEAN;
+x_14 : BOOLEAN;
+x_15 : BOOLEAN;
+x_16 : BOOLEAN;
+x_17 : BOOLEAN;
+x_18 : BOOLEAN;
+x_19 : BOOLEAN;
+x_20 : BOOLEAN;
+ASSERT NOT x_9 OR x_3 OR NOT x_15;
+ASSERT NOT x_12 OR NOT x_4 OR NOT x_15;
+ASSERT x_6 OR x_14 OR NOT x_17;
+ASSERT x_10 OR x_16 OR x_11;
+ASSERT NOT x_15 OR x_20 OR NOT x_7;
+ASSERT NOT x_1 OR x_10 OR x_16;
+ASSERT x_13 OR x_17 OR NOT x_7;
+ASSERT NOT x_2 OR NOT x_14 OR NOT x_13;
+ASSERT x_13 OR NOT x_6 OR x_15;
+ASSERT NOT x_9 OR x_3 OR x_16;
+ASSERT NOT x_20 OR NOT x_13 OR x_4;
+ASSERT NOT x_7 OR x_15 OR NOT x_14;
+ASSERT NOT x_15 OR NOT x_16 OR x_6;
+ASSERT x_5 OR NOT x_18 OR x_20;
+ASSERT NOT x_16 OR NOT x_19 OR x_7;
+ASSERT x_20 OR NOT x_18 OR NOT x_2;
+ASSERT x_10 OR NOT x_19 OR NOT x_14;
+ASSERT x_16 OR NOT x_7 OR x_12;
+ASSERT x_6 OR NOT x_5 OR NOT x_1;
+ASSERT NOT x_9 OR x_11 OR x_15;
+ASSERT x_19 OR NOT x_6 OR x_7;
+ASSERT NOT x_11 OR x_17 OR NOT x_19;
+ASSERT x_9 OR NOT x_16 OR x_6;
+ASSERT x_15 OR NOT x_20 OR x_10;
+ASSERT x_9 OR NOT x_1 OR NOT x_11;
+ASSERT NOT x_8 OR NOT x_19 OR x_5;
+ASSERT NOT x_19 OR x_11 OR x_20;
+ASSERT NOT x_12 OR x_13 OR NOT x_3;
+ASSERT NOT x_7 OR NOT x_17 OR NOT x_19;
+ASSERT x_17 OR x_6 OR NOT x_11;
+ASSERT NOT x_7 OR NOT x_17 OR x_10;
+ASSERT NOT x_14 OR x_9 OR x_20;
+ASSERT x_1 OR NOT x_18 OR NOT x_16;
+ASSERT NOT x_2 OR NOT x_15 OR x_20;
+ASSERT x_14 OR x_18 OR NOT x_1;
+ASSERT NOT x_8 OR NOT x_4 OR x_1;
+ASSERT x_13 OR x_3 OR NOT x_9;
+ASSERT x_5 OR x_7 OR x_8;
+ASSERT x_9 OR x_4 OR NOT x_20;
+ASSERT NOT x_18 OR NOT x_15 OR NOT x_10;
+ASSERT x_10 OR x_3 OR NOT x_20;
+ASSERT x_20 OR NOT x_14 OR x_16;
+ASSERT x_20 OR NOT x_3 OR NOT x_11;
+ASSERT NOT x_12 OR x_19 OR NOT x_16;
+ASSERT NOT x_3 OR x_5 OR x_10;
+ASSERT x_8 OR x_13 OR NOT x_7;
+ASSERT NOT x_2 OR NOT x_15 OR x_10;
+ASSERT NOT x_3 OR x_9 OR x_16;
+ASSERT NOT x_12 OR NOT x_16 OR NOT x_18;
+ASSERT x_3 OR x_1 OR NOT x_12;
+ASSERT NOT x_18 OR x_13 OR x_5;
+ASSERT x_1 OR x_3 OR NOT x_19;
+ASSERT NOT x_19 OR NOT x_5 OR x_6;
+ASSERT NOT x_20 OR x_8 OR NOT x_2;
+ASSERT x_17 OR NOT x_8 OR NOT x_13;
+ASSERT x_7 OR NOT x_11 OR NOT x_12;
+ASSERT NOT x_10 OR NOT x_14 OR NOT x_20;
+ASSERT NOT x_1 OR x_16 OR NOT x_12;
+ASSERT x_5 OR NOT x_3 OR x_9;
+ASSERT NOT x_18 OR x_8 OR x_14;
+ASSERT x_1 OR x_16 OR x_12;
+ASSERT x_20 OR NOT x_1 OR NOT x_16;
+ASSERT x_5 OR x_10 OR NOT x_13;
+ASSERT x_9 OR NOT x_10 OR x_6;
+ASSERT NOT x_12 OR x_10 OR NOT x_14;
+ASSERT NOT x_13 OR x_1 OR x_4;
+ASSERT NOT x_20 OR NOT x_7 OR x_3;
+ASSERT x_12 OR x_1 OR NOT x_10;
+ASSERT NOT x_1 OR NOT x_16 OR x_7;
+ASSERT x_11 OR NOT x_6 OR NOT x_4;
+ASSERT x_1 OR x_16 OR NOT x_20;
+ASSERT x_9 OR x_7 OR x_15;
+ASSERT NOT x_6 OR x_17 OR x_10;
+ASSERT x_8 OR x_9 OR x_17;
+ASSERT x_18 OR x_11 OR x_10;
+ASSERT x_7 OR x_1 OR NOT x_8;
+ASSERT NOT x_5 OR NOT x_12 OR x_18;
+ASSERT NOT x_6 OR x_2 OR x_15;
+ASSERT x_2 OR x_18 OR x_1;
+ASSERT NOT x_7 OR NOT x_13 OR x_16;
+ASSERT x_18 OR x_19 OR x_9;
+ASSERT x_9 OR NOT x_14 OR x_18;
+ASSERT x_14 OR x_12 OR NOT x_5;
+ASSERT NOT x_13 OR NOT x_7 OR NOT x_14;
+ASSERT NOT x_1 OR x_8 OR NOT x_16;
+ASSERT NOT x_11 OR x_4 OR x_7;
+ASSERT NOT x_4 OR x_20 OR x_5;
+ASSERT NOT x_5 OR x_2 OR x_12;
+ASSERT NOT x_5 OR x_13 OR NOT x_18;
+ASSERT NOT x_18 OR x_9 OR x_1;
+ASSERT x_10 OR NOT x_11 OR x_16;
+
+
+QUERY FALSE;
+% EXIT: 10
diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index 3dbee87eb..448933622 100644
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): barrett, dejan, cconway
+ ** Minor contributors (to current version): cconway, dejan
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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
@@ -160,21 +160,21 @@ public:
     Node b = d_nm->mkVar(*d_booleanType);
     Node c = d_nm->mkVar(*d_booleanType);
 
-    Debug("cdboolattr", "get flag 1 on a (should be F)\n");
+    Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
     TS_ASSERT(! a.getAttribute(TestFlag1cd()));
-    Debug("cdboolattr", "get flag 1 on b (should be F)\n");
+    Debug("cdboolattr") << "get flag 1 on b (should be F)\n";
     TS_ASSERT(! b.getAttribute(TestFlag1cd()));
-    Debug("cdboolattr", "get flag 1 on c (should be F)\n");
+    Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
     TS_ASSERT(! c.getAttribute(TestFlag1cd()));
 
     d_ctxt->push(); // level 1
 
     // test that all boolean flags are FALSE to start
-    Debug("cdboolattr", "get flag 1 on a (should be F)\n");
+    Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
     TS_ASSERT(! a.getAttribute(TestFlag1cd()));
-    Debug("cdboolattr", "get flag 1 on b (should be F)\n");
+    Debug("cdboolattr") << "get flag 1 on b (should be F)\n";
     TS_ASSERT(! b.getAttribute(TestFlag1cd()));
-    Debug("cdboolattr", "get flag 1 on c (should be F)\n");
+    Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
     TS_ASSERT(! c.getAttribute(TestFlag1cd()));
 
     // test that they all HAVE the boolean attributes
@@ -184,96 +184,96 @@ public:
 
     // test two-arg version of hasAttribute()
     bool bb = false;
-    Debug("cdboolattr", "get flag 1 on a (should be F)\n");
+    Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
     TS_ASSERT(a.getAttribute(TestFlag1cd(), bb));
     TS_ASSERT(! bb);
-    Debug("cdboolattr", "get flag 1 on b (should be F)\n");
+    Debug("cdboolattr") << "get flag 1 on b (should be F)\n";
     TS_ASSERT(b.getAttribute(TestFlag1cd(), bb));
     TS_ASSERT(! bb);
-    Debug("cdboolattr", "get flag 1 on c (should be F)\n");
+    Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
     TS_ASSERT(c.getAttribute(TestFlag1cd(), bb));
     TS_ASSERT(! bb);
 
     // setting boolean flags
-    Debug("cdboolattr", "set flag 1 on a to T\n");
+    Debug("cdboolattr") << "set flag 1 on a to T\n";
     a.setAttribute(TestFlag1cd(), true);
-    Debug("cdboolattr", "set flag 1 on b to F\n");
+    Debug("cdboolattr") << "set flag 1 on b to F\n";
     b.setAttribute(TestFlag1cd(), false);
-    Debug("cdboolattr", "set flag 1 on c to F\n");
+    Debug("cdboolattr") << "set flag 1 on c to F\n";
     c.setAttribute(TestFlag1cd(), false);
 
-    Debug("cdbootattr", "get flag 1 on a (should be T)\n");
+    Debug("cdboolattr") << "get flag 1 on a (should be T)\n";
     TS_ASSERT(a.getAttribute(TestFlag1cd()));
-    Debug("cdbootattr", "get flag 1 on b (should be F)\n");
+    Debug("cdboolattr") << "get flag 1 on b (should be F)\n";
     TS_ASSERT(! b.getAttribute(TestFlag1cd()));
-    Debug("cdbootattr", "get flag 1 on c (should be F)\n");
+    Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
     TS_ASSERT(! c.getAttribute(TestFlag1cd()));
 
     d_ctxt->push(); // level 2
 
-    Debug("cdbootattr", "get flag 1 on a (should be T)\n");
+    Debug("cdboolattr") << "get flag 1 on a (should be T)\n";
     TS_ASSERT(a.getAttribute(TestFlag1cd()));
-    Debug("cdbootattr", "get flag 1 on b (should be F)\n");
+    Debug("cdboolattr") << "get flag 1 on b (should be F)\n";
     TS_ASSERT(! b.getAttribute(TestFlag1cd()));
-    Debug("cdbootattr", "get flag 1 on c (should be F)\n");
+    Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
     TS_ASSERT(! c.getAttribute(TestFlag1cd()));
 
-    Debug("cdbootattr", "set flag 1 on a to F\n");
+    Debug("cdboolattr") << "set flag 1 on a to F\n";
     a.setAttribute(TestFlag1cd(), false);
-    Debug("cdbootattr", "set flag 1 on b to T\n");
+    Debug("cdboolattr") << "set flag 1 on b to T\n";
     b.setAttribute(TestFlag1cd(), true);
 
-    Debug("cdbootattr", "get flag 1 on a (should be F)\n");
+    Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
     TS_ASSERT(! a.getAttribute(TestFlag1cd()));
-    Debug("cdbootattr", "get flag 1 on b (should be T)\n");
+    Debug("cdboolattr") << "get flag 1 on b (should be T)\n";
     TS_ASSERT(b.getAttribute(TestFlag1cd()));
-    Debug("cdbootattr", "get flag 1 on c (should be F)\n");
+    Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
     TS_ASSERT(! c.getAttribute(TestFlag1cd()));
 
     d_ctxt->push(); // level 3
 
-    Debug("cdbootattr", "get flag 1 on a (should be F)\n");
+    Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
     TS_ASSERT(! a.getAttribute(TestFlag1cd()));
-    Debug("cdbootattr", "get flag 1 on b (should be T)\n");
+    Debug("cdboolattr") << "get flag 1 on b (should be T)\n";
     TS_ASSERT(b.getAttribute(TestFlag1cd()));
-    Debug("cdbootattr", "get flag 1 on c (should be F)\n");
+    Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
     TS_ASSERT(! c.getAttribute(TestFlag1cd()));
 
-    Debug("cdbootattr", "set flag 1 on c to T\n");
+    Debug("cdboolattr") << "set flag 1 on c to T\n";
     c.setAttribute(TestFlag1cd(), true);
 
-    Debug("cdbootattr", "get flag 1 on a (should be F)\n");
+    Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
     TS_ASSERT(! a.getAttribute(TestFlag1cd()));
-    Debug("cdbootattr", "get flag 1 on b (should be T)\n");
+    Debug("cdboolattr") << "get flag 1 on b (should be T)\n";
     TS_ASSERT(b.getAttribute(TestFlag1cd()));
-    Debug("cdbootattr", "get flag 1 on c (should be T)\n");
+    Debug("cdboolattr") << "get flag 1 on c (should be T)\n";
     TS_ASSERT(c.getAttribute(TestFlag1cd()));
 
     d_ctxt->pop(); // level 2
 
-    Debug("cdbootattr", "get flag 1 on a (should be F)\n");
+    Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
     TS_ASSERT(! a.getAttribute(TestFlag1cd()));
-    Debug("cdbootattr", "get flag 1 on b (should be T)\n");
+    Debug("cdboolattr") << "get flag 1 on b (should be T)\n";
     TS_ASSERT(b.getAttribute(TestFlag1cd()));
-    Debug("cdbootattr", "get flag 1 on c (should be F)\n");
+    Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
     TS_ASSERT(! c.getAttribute(TestFlag1cd()));
 
     d_ctxt->pop(); // level 1
 
-    Debug("cdbootattr", "get flag 1 on a (should be T)\n");
+    Debug("cdboolattr") << "get flag 1 on a (should be T)\n";
     TS_ASSERT(a.getAttribute(TestFlag1cd()));
-    Debug("cdbootattr", "get flag 1 on b (should be F)\n");
+    Debug("cdboolattr") << "get flag 1 on b (should be F)\n";
     TS_ASSERT(! b.getAttribute(TestFlag1cd()));
-    Debug("cdbootattr", "get flag 1 on c (should be F)\n");
+    Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
     TS_ASSERT(! c.getAttribute(TestFlag1cd()));
 
     d_ctxt->pop(); // level 0
 
-    Debug("cdbootattr", "get flag 1 on a (should be F)\n");
+    Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
     TS_ASSERT(! a.getAttribute(TestFlag1cd()));
-    Debug("cdbootattr", "get flag 1 on b (should be F)\n");
+    Debug("cdboolattr") << "get flag 1 on b (should be F)\n";
     TS_ASSERT(! b.getAttribute(TestFlag1cd()));
-    Debug("cdbootattr", "get flag 1 on c (should be F)\n");
+    Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
     TS_ASSERT(! c.getAttribute(TestFlag1cd()));
 
 #ifdef CVC4_ASSERTIONS
@@ -294,49 +294,49 @@ public:
     c.setAttribute(VarNameAttr(), "c");
 
     // test that all boolean flags are FALSE to start
-    Debug("boolattr", "get flag 1 on a (should be F)\n");
+    Debug("boolattr") << "get flag 1 on a (should be F)\n";
     TS_ASSERT(! a.getAttribute(TestFlag1()));
-    Debug("boolattr", "get flag 1 on b (should be F)\n");
+    Debug("boolattr") << "get flag 1 on b (should be F)\n";
     TS_ASSERT(! b.getAttribute(TestFlag1()));
-    Debug("boolattr", "get flag 1 on c (should be F)\n");
+    Debug("boolattr") << "get flag 1 on c (should be F)\n";
     TS_ASSERT(! c.getAttribute(TestFlag1()));
-    Debug("boolattr", "get flag 1 on unnamed (should be F)\n");
+    Debug("boolattr") << "get flag 1 on unnamed (should be F)\n";
     TS_ASSERT(! unnamed.getAttribute(TestFlag1()));
 
-    Debug("boolattr", "get flag 2 on a (should be F)\n");
+    Debug("boolattr") << "get flag 2 on a (should be F)\n";
     TS_ASSERT(! a.getAttribute(TestFlag2()));
-    Debug("boolattr", "get flag 2 on b (should be F)\n");
+    Debug("boolattr") << "get flag 2 on b (should be F)\n";
     TS_ASSERT(! b.getAttribute(TestFlag2()));
-    Debug("boolattr", "get flag 2 on c (should be F)\n");
+    Debug("boolattr") << "get flag 2 on c (should be F)\n";
     TS_ASSERT(! c.getAttribute(TestFlag2()));
-    Debug("boolattr", "get flag 2 on unnamed (should be F)\n");
+    Debug("boolattr") << "get flag 2 on unnamed (should be F)\n";
     TS_ASSERT(! unnamed.getAttribute(TestFlag2()));
 
-    Debug("boolattr", "get flag 3 on a (should be F)\n");
+    Debug("boolattr") << "get flag 3 on a (should be F)\n";
     TS_ASSERT(! a.getAttribute(TestFlag3()));
-    Debug("boolattr", "get flag 3 on b (should be F)\n");
+    Debug("boolattr") << "get flag 3 on b (should be F)\n";
     TS_ASSERT(! b.getAttribute(TestFlag3()));
-    Debug("boolattr", "get flag 3 on c (should be F)\n");
+    Debug("boolattr") << "get flag 3 on c (should be F)\n";
     TS_ASSERT(! c.getAttribute(TestFlag3()));
-    Debug("boolattr", "get flag 3 on unnamed (should be F)\n");
+    Debug("boolattr") << "get flag 3 on unnamed (should be F)\n";
     TS_ASSERT(! unnamed.getAttribute(TestFlag3()));
 
-    Debug("boolattr", "get flag 4 on a (should be F)\n");
+    Debug("boolattr") << "get flag 4 on a (should be F)\n";
     TS_ASSERT(! a.getAttribute(TestFlag4()));
-    Debug("boolattr", "get flag 4 on b (should be F)\n");
+    Debug("boolattr") << "get flag 4 on b (should be F)\n";
     TS_ASSERT(! b.getAttribute(TestFlag4()));
-    Debug("boolattr", "get flag 4 on c (should be F)\n");
+    Debug("boolattr") << "get flag 4 on c (should be F)\n";
     TS_ASSERT(! c.getAttribute(TestFlag4()));
-    Debug("boolattr", "get flag 4 on unnamed (should be F)\n");
+    Debug("boolattr") << "get flag 4 on unnamed (should be F)\n";
     TS_ASSERT(! unnamed.getAttribute(TestFlag4()));
 
-    Debug("boolattr", "get flag 5 on a (should be F)\n");
+    Debug("boolattr") << "get flag 5 on a (should be F)\n";
     TS_ASSERT(! a.getAttribute(TestFlag5()));
-    Debug("boolattr", "get flag 5 on b (should be F)\n");
+    Debug("boolattr") << "get flag 5 on b (should be F)\n";
     TS_ASSERT(! b.getAttribute(TestFlag5()));
-    Debug("boolattr", "get flag 5 on c (should be F)\n");
+    Debug("boolattr") << "get flag 5 on c (should be F)\n";
     TS_ASSERT(! c.getAttribute(TestFlag5()));
-    Debug("boolattr", "get flag 5 on unnamed (should be F)\n");
+    Debug("boolattr") << "get flag 5 on unnamed (should be F)\n";
     TS_ASSERT(! unnamed.getAttribute(TestFlag5()));
 
     // test that they all HAVE the boolean attributes
@@ -367,115 +367,115 @@ public:
 
     // test two-arg version of hasAttribute()
     bool bb;
-    Debug("boolattr", "get flag 1 on a (should be F)\n");
+    Debug("boolattr") << "get flag 1 on a (should be F)\n";
     TS_ASSERT(a.getAttribute(TestFlag1(), bb));
     TS_ASSERT(! bb);
-    Debug("boolattr", "get flag 1 on b (should be F)\n");
+    Debug("boolattr") << "get flag 1 on b (should be F)\n";
     TS_ASSERT(b.getAttribute(TestFlag1(), bb));
     TS_ASSERT(! bb);
-    Debug("boolattr", "get flag 1 on c (should be F)\n");
+    Debug("boolattr") << "get flag 1 on c (should be F)\n";
     TS_ASSERT(c.getAttribute(TestFlag1(), bb));
     TS_ASSERT(! bb);
-    Debug("boolattr", "get flag 1 on unnamed (should be F)\n");
+    Debug("boolattr") << "get flag 1 on unnamed (should be F)\n";
     TS_ASSERT(unnamed.getAttribute(TestFlag1(), bb));
     TS_ASSERT(! bb);
 
-    Debug("boolattr", "get flag 2 on a (should be F)\n");
+    Debug("boolattr") << "get flag 2 on a (should be F)\n";
     TS_ASSERT(a.getAttribute(TestFlag2(), bb));
     TS_ASSERT(! bb);
-    Debug("boolattr", "get flag 2 on b (should be F)\n");
+    Debug("boolattr") << "get flag 2 on b (should be F)\n";
     TS_ASSERT(b.getAttribute(TestFlag2(), bb));
     TS_ASSERT(! bb);
-    Debug("boolattr", "get flag 2 on c (should be F)\n");
+    Debug("boolattr") << "get flag 2 on c (should be F)\n";
     TS_ASSERT(c.getAttribute(TestFlag2(), bb));
     TS_ASSERT(! bb);
-    Debug("boolattr", "get flag 2 on unnamed (should be F)\n");
+    Debug("boolattr") << "get flag 2 on unnamed (should be F)\n";
     TS_ASSERT(unnamed.getAttribute(TestFlag2(), bb));
     TS_ASSERT(! bb);
 
-    Debug("boolattr", "get flag 3 on a (should be F)\n");
+    Debug("boolattr") << "get flag 3 on a (should be F)\n";
     TS_ASSERT(a.getAttribute(TestFlag3(), bb));
     TS_ASSERT(! bb);
-    Debug("boolattr", "get flag 3 on b (should be F)\n");
+    Debug("boolattr") << "get flag 3 on b (should be F)\n";
     TS_ASSERT(b.getAttribute(TestFlag3(), bb));
     TS_ASSERT(! bb);
-    Debug("boolattr", "get flag 3 on c (should be F)\n");
+    Debug("boolattr") << "get flag 3 on c (should be F)\n";
     TS_ASSERT(c.getAttribute(TestFlag3(), bb));
     TS_ASSERT(! bb);
-    Debug("boolattr", "get flag 3 on unnamed (should be F)\n");
+    Debug("boolattr") << "get flag 3 on unnamed (should be F)\n";
     TS_ASSERT(unnamed.getAttribute(TestFlag3(), bb));
     TS_ASSERT(! bb);
 
-    Debug("boolattr", "get flag 4 on a (should be F)\n");
+    Debug("boolattr") << "get flag 4 on a (should be F)\n";
     TS_ASSERT(a.getAttribute(TestFlag4(), bb));
     TS_ASSERT(! bb);
-    Debug("boolattr", "get flag 4 on b (should be F)\n");
+    Debug("boolattr") << "get flag 4 on b (should be F)\n";
     TS_ASSERT(b.getAttribute(TestFlag4(), bb));
     TS_ASSERT(! bb);
-    Debug("boolattr", "get flag 4 on c (should be F)\n");
+    Debug("boolattr") << "get flag 4 on c (should be F)\n";
     TS_ASSERT(c.getAttribute(TestFlag4(), bb));
     TS_ASSERT(! bb);
-    Debug("boolattr", "get flag 4 on unnamed (should be F)\n");
+    Debug("boolattr") << "get flag 4 on unnamed (should be F)\n";
     TS_ASSERT(unnamed.getAttribute(TestFlag4(), bb));
     TS_ASSERT(! bb);
 
-    Debug("boolattr", "get flag 5 on a (should be F)\n");
+    Debug("boolattr") << "get flag 5 on a (should be F)\n";
     TS_ASSERT(a.getAttribute(TestFlag5(), bb));
     TS_ASSERT(! bb);
-    Debug("boolattr", "get flag 5 on b (should be F)\n");
+    Debug("boolattr") << "get flag 5 on b (should be F)\n";
     TS_ASSERT(b.getAttribute(TestFlag5(), bb));
     TS_ASSERT(! bb);
-    Debug("boolattr", "get flag 5 on c (should be F)\n");
+    Debug("boolattr") << "get flag 5 on c (should be F)\n";
     TS_ASSERT(c.getAttribute(TestFlag5(), bb));
     TS_ASSERT(! bb);
-    Debug("boolattr", "get flag 5 on unnamed (should be F)\n");
+    Debug("boolattr") << "get flag 5 on unnamed (should be F)\n";
     TS_ASSERT(unnamed.getAttribute(TestFlag5(), bb));
     TS_ASSERT(! bb);
 
     // setting boolean flags
-    Debug("boolattr", "set flag 1 on a to T\n");
+    Debug("boolattr") << "set flag 1 on a to T\n";
     a.setAttribute(TestFlag1(), true);
-    Debug("boolattr", "set flag 1 on b to F\n");
+    Debug("boolattr") << "set flag 1 on b to F\n";
     b.setAttribute(TestFlag1(), false);
-    Debug("boolattr", "set flag 1 on c to F\n");
+    Debug("boolattr") << "set flag 1 on c to F\n";
     c.setAttribute(TestFlag1(), false);
-    Debug("boolattr", "set flag 1 on unnamed to T\n");
+    Debug("boolattr") << "set flag 1 on unnamed to T\n";
     unnamed.setAttribute(TestFlag1(), true);
 
-    Debug("boolattr", "set flag 2 on a to F\n");
+    Debug("boolattr") << "set flag 2 on a to F\n";
     a.setAttribute(TestFlag2(), false);
-    Debug("boolattr", "set flag 2 on b to T\n");
+    Debug("boolattr") << "set flag 2 on b to T\n";
     b.setAttribute(TestFlag2(), true);
-    Debug("boolattr", "set flag 2 on c to T\n");
+    Debug("boolattr") << "set flag 2 on c to T\n";
     c.setAttribute(TestFlag2(), true);
-    Debug("boolattr", "set flag 2 on unnamed to F\n");
+    Debug("boolattr") << "set flag 2 on unnamed to F\n";
     unnamed.setAttribute(TestFlag2(), false);
 
-    Debug("boolattr", "set flag 3 on a to T\n");
+    Debug("boolattr") << "set flag 3 on a to T\n";
     a.setAttribute(TestFlag3(), true);
-    Debug("boolattr", "set flag 3 on b to T\n");
+    Debug("boolattr") << "set flag 3 on b to T\n";
     b.setAttribute(TestFlag3(), true);
-    Debug("boolattr", "set flag 3 on c to T\n");
+    Debug("boolattr") << "set flag 3 on c to T\n";
     c.setAttribute(TestFlag3(), true);
-    Debug("boolattr", "set flag 3 on unnamed to T\n");
+    Debug("boolattr") << "set flag 3 on unnamed to T\n";
     unnamed.setAttribute(TestFlag3(), true);
 
-    Debug("boolattr", "set flag 4 on a to T\n");
+    Debug("boolattr") << "set flag 4 on a to T\n";
     a.setAttribute(TestFlag4(), true);
-    Debug("boolattr", "set flag 4 on b to T\n");
+    Debug("boolattr") << "set flag 4 on b to T\n";
     b.setAttribute(TestFlag4(), true);
-    Debug("boolattr", "set flag 4 on c to T\n");
+    Debug("boolattr") << "set flag 4 on c to T\n";
     c.setAttribute(TestFlag4(), true);
-    Debug("boolattr", "set flag 4 on unnamed to T\n");
+    Debug("boolattr") << "set flag 4 on unnamed to T\n";
     unnamed.setAttribute(TestFlag4(), true);
 
-    Debug("boolattr", "set flag 5 on a to T\n");
+    Debug("boolattr") << "set flag 5 on a to T\n";
     a.setAttribute(TestFlag5(), true);
-    Debug("boolattr", "set flag 5 on b to T\n");
+    Debug("boolattr") << "set flag 5 on b to T\n";
     b.setAttribute(TestFlag5(), true);
-    Debug("boolattr", "set flag 5 on c to F\n");
+    Debug("boolattr") << "set flag 5 on c to F\n";
     c.setAttribute(TestFlag5(), false);
-    Debug("boolattr", "set flag 5 on unnamed to T\n");
+    Debug("boolattr") << "set flag 5 on unnamed to T\n";
     unnamed.setAttribute(TestFlag5(), true);
 
     TS_ASSERT(a.getAttribute(VarNameAttr()) == "a");
@@ -510,49 +510,49 @@ public:
     TS_ASSERT(! c.hasAttribute(TestStringAttr2()));
     TS_ASSERT(! unnamed.hasAttribute(TestStringAttr2()));
 
-    Debug("boolattr", "get flag 1 on a (should be T)\n");
+    Debug("boolattr") << "get flag 1 on a (should be T)\n";
     TS_ASSERT(a.getAttribute(TestFlag1()));
-    Debug("boolattr", "get flag 1 on b (should be F)\n");
+    Debug("boolattr") << "get flag 1 on b (should be F)\n";
     TS_ASSERT(! b.getAttribute(TestFlag1()));
-    Debug("boolattr", "get flag 1 on c (should be F)\n");
+    Debug("boolattr") << "get flag 1 on c (should be F)\n";
     TS_ASSERT(! c.getAttribute(TestFlag1()));
-    Debug("boolattr", "get flag 1 on unnamed (should be T)\n");
+    Debug("boolattr") << "get flag 1 on unnamed (should be T)\n";
     TS_ASSERT(unnamed.getAttribute(TestFlag1()));
 
-    Debug("boolattr", "get flag 2 on a (should be F)\n");
+    Debug("boolattr") << "get flag 2 on a (should be F)\n";
     TS_ASSERT(! a.getAttribute(TestFlag2()));
-    Debug("boolattr", "get flag 2 on b (should be T)\n");
+    Debug("boolattr") << "get flag 2 on b (should be T)\n";
     TS_ASSERT(b.getAttribute(TestFlag2()));
-    Debug("boolattr", "get flag 2 on c (should be T)\n");
+    Debug("boolattr") << "get flag 2 on c (should be T)\n";
     TS_ASSERT(c.getAttribute(TestFlag2()));
-    Debug("boolattr", "get flag 2 on unnamed (should be F)\n");
+    Debug("boolattr") << "get flag 2 on unnamed (should be F)\n";
     TS_ASSERT(! unnamed.getAttribute(TestFlag2()));
 
-    Debug("boolattr", "get flag 3 on a (should be T)\n");
+    Debug("boolattr") << "get flag 3 on a (should be T)\n";
     TS_ASSERT(a.getAttribute(TestFlag3()));
-    Debug("boolattr", "get flag 3 on b (should be T)\n");
+    Debug("boolattr") << "get flag 3 on b (should be T)\n";
     TS_ASSERT(b.getAttribute(TestFlag3()));
-    Debug("boolattr", "get flag 3 on c (should be T)\n");
+    Debug("boolattr") << "get flag 3 on c (should be T)\n";
     TS_ASSERT(c.getAttribute(TestFlag3()));
-    Debug("boolattr", "get flag 3 on unnamed (should be T)\n");
+    Debug("boolattr") << "get flag 3 on unnamed (should be T)\n";
     TS_ASSERT(unnamed.getAttribute(TestFlag3()));
 
-    Debug("boolattr", "get flag 4 on a (should be T)\n");
+    Debug("boolattr") << "get flag 4 on a (should be T)\n";
     TS_ASSERT(a.getAttribute(TestFlag4()));
-    Debug("boolattr", "get flag 4 on b (should be T)\n");
+    Debug("boolattr") << "get flag 4 on b (should be T)\n";
     TS_ASSERT(b.getAttribute(TestFlag4()));
-    Debug("boolattr", "get flag 4 on c (should be T)\n");
+    Debug("boolattr") << "get flag 4 on c (should be T)\n";
     TS_ASSERT(c.getAttribute(TestFlag4()));
-    Debug("boolattr", "get flag 4 on unnamed (should be T)\n");
+    Debug("boolattr") << "get flag 4 on unnamed (should be T)\n";
     TS_ASSERT(unnamed.getAttribute(TestFlag4()));
 
-    Debug("boolattr", "get flag 5 on a (should be T)\n");
+    Debug("boolattr") << "get flag 5 on a (should be T)\n";
     TS_ASSERT(a.getAttribute(TestFlag5()));
-    Debug("boolattr", "get flag 5 on b (should be T)\n");
+    Debug("boolattr") << "get flag 5 on b (should be T)\n";
     TS_ASSERT(b.getAttribute(TestFlag5()));
-    Debug("boolattr", "get flag 5 on c (should be F)\n");
+    Debug("boolattr") << "get flag 5 on c (should be F)\n";
     TS_ASSERT(! c.getAttribute(TestFlag5()));
-    Debug("boolattr", "get flag 5 on unnamed (should be T)\n");
+    Debug("boolattr") << "get flag 5 on unnamed (should be T)\n";
     TS_ASSERT(unnamed.getAttribute(TestFlag5()));
 
     a.setAttribute(TestStringAttr1(), "foo");
diff --git a/test/unit/util/output_black.h b/test/unit/util/output_black.h
index e6a040f7b..183d8f7f1 100644
--- a/test/unit/util/output_black.h
+++ b/test/unit/util/output_black.h
@@ -5,7 +5,7 @@
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
@@ -219,6 +219,31 @@ public:
 
   }
 
+  static int expensiveFunction() {
+    // this represents an expensive function that should NOT be called
+    // when debugging/tracing is turned off
+    TS_FAIL("a function was evaluated under Debug() or Trace() when it should not have been");
+    return 0;
+  }
+
+  void testEvaluationOffWhenItsSupposedToBe() {
+    Trace.on("foo");
+#ifndef CVC4_TRACING
+    TS_ASSERT( !( Trace.isOn("foo") ) );
+    Trace("foo") << expensiveFunction() << endl;
+#else /* CVC4_TRACING */
+    TS_ASSERT( Trace.isOn("foo") );
+#endif /* CVC4_TRACING */
+
+    Debug.on("foo");
+#ifndef CVC4_DEBUG
+    TS_ASSERT( !( Debug.isOn("foo") ) );
+    Debug("foo") << expensiveFunction() << endl;
+#else /* CVC4_DEBUG */
+    TS_ASSERT( Debug.isOn("foo") );
+#endif /* CVC4_DEBUG */
+  }
+
   void testSimplePrint() {
 
 #ifdef CVC4_MUZZLE
@@ -260,11 +285,11 @@ public:
 #else /* CVC4_MUZZLE */
 
     Debug.off("yo");
-    Debug("yo", "foobar");
+    Debug("yo") << "foobar";
     TS_ASSERT_EQUALS(d_debugStream.str(), string());
     d_debugStream.str("");
     Debug.on("yo");
-    Debug("yo", "baz foo");
+    Debug("yo") << "baz foo";
 #  ifdef CVC4_DEBUG
     TS_ASSERT_EQUALS(d_debugStream.str(), string("baz foo"));
 #  else /* CVC4_DEBUG */
@@ -273,11 +298,11 @@ public:
     d_debugStream.str("");
 
     Trace.off("yo");
-    Trace("yo", "foobar");
+    Trace("yo") << "foobar";
     TS_ASSERT_EQUALS(d_traceStream.str(), string());
     d_traceStream.str("");
     Trace.on("yo");
-    Trace("yo", "baz foo");
+    Trace("yo") << "baz foo";
 #  ifdef CVC4_TRACING
     TS_ASSERT_EQUALS(d_traceStream.str(), string("baz foo"));
 #  else /* CVC4_TRACING */
@@ -285,19 +310,19 @@ public:
 #  endif /* CVC4_TRACING */
     d_traceStream.str("");
 
-    Warning("baz foo");
+    Warning() << "baz foo";
     TS_ASSERT_EQUALS(d_warningStream.str(), string("baz foo"));
     d_warningStream.str("");
 
-    Chat("baz foo");
+    Chat() << "baz foo";
     TS_ASSERT_EQUALS(d_chatStream.str(), string("baz foo"));
     d_chatStream.str("");
 
-    Message("baz foo");
+    Message() << "baz foo";
     TS_ASSERT_EQUALS(d_messageStream.str(), string("baz foo"));
     d_messageStream.str("");
 
-    Notice("baz foo");
+    Notice() << "baz foo";
     TS_ASSERT_EQUALS(d_noticeStream.str(), string("baz foo"));
     d_noticeStream.str("");