A handful of build system fixes:

* (test/unit/Makefile.am) libtool was being passed relative paths of
  sources in .cpp, confusing lcov if -b wasn't given.  Fixed.
  Closes bug #102.

* (configure.ac) --enable-coverage now implies --enable-static
  --enable-static-binary --disable-shared.

* (configure.ac) Create top-level config.status for informational and
  re-configuration purposes.

* (configure.ac) Remove -fvisibility=hidden for debug builds.
  Closes bug #104.

* (test/unit/Makefile.am) Build unit tests with -Wall.

* (various unit tests) Fixed trivially-fixable warnings in building
  unit tests.  (Signedness in comparison, unused variables, etc.)

* (Makefile.builds.in) Copy the binary correctly if it is static.
  (It was failing, but only with --enable-static --enable-shared
  --enable-static-binary.)  Closes bug #103.

* (src/parser/Makefile.am) libcvc4parser.so now links with libcvc4.so.

* Other minor cleanups to the build system.

13 files changed, 116 insertions, 118 deletions

diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 4ff65a672..c52ac5d1c 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -48,7 +48,7 @@ if HAVE_CXXTESTGEN
 AM_CPPFLAGS = \
 	-I. "-I@CXXTEST@" "-I@top_srcdir@/src/include" "-I@top_srcdir@/src" \
 	$(TEST_CPPFLAGS)
-AM_CXXFLAGS = $(TEST_CXXFLAGS)
+AM_CXXFLAGS = -Wall $(TEST_CXXFLAGS)
 AM_LDFLAGS = $(TEST_LDFLAGS)
 
 AM_CXXFLAGS_WHITE = -fno-access-control -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST
@@ -85,13 +85,13 @@ $(UNIT_TESTS:%=%.cpp): %.cpp: %.h
 	$(AM_V_at)mkdir -p `dirname "$@"`
 	$(AM_V_GEN)$(CXXTESTGEN) --have-eh --have-std --error-printer -o "$@" "$<"
 $(WHITE_TESTS): %_white: %_white.cpp $(TEST_DEPS)
-	$(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -c -o $@.lo $<
+	$(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -c -o $@.lo @abs_builddir@/$<
 	$(AM_V_CXXLD)$(unit_LINK) $(AM_LDFLAGS_WHITE) $@.lo
 $(BLACK_TESTS): %_black: %_black.cpp $(TEST_DEPS)
-	$(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_BLACK) -c -o $@.lo $<
+	$(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_BLACK) -c -o $@.lo @abs_builddir@/$<
 	$(AM_V_CXXLD)$(unit_LINK) $(AM_LDFLAGS_BLACK) $@.lo
 $(PUBLIC_TESTS): %_public: %_public.cpp $(TEST_DEPS)
-	$(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -c -o $@.lo $<
+	$(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -c -o $@.lo @abs_builddir@/$<
 	$(AM_V_CXXLD)$(unit_LINK) $(AM_LDFLAGS_PUBLIC) $@.lo
 
 else
diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h
index b083f4794..f31d5f273 100644
--- a/test/unit/context/cdlist_black.h
+++ b/test/unit/context/cdlist_black.h
@@ -48,21 +48,21 @@ public:
 
     TS_ASSERT(list.empty());
     for(int i = 0; i < N; ++i) {
-      TS_ASSERT(list.size() == i);
+      TS_ASSERT_EQUALS(list.size(), unsigned(i));
       list.push_back(i);
       TS_ASSERT(!list.empty());
-      TS_ASSERT(list.back() == i);
+      TS_ASSERT_EQUALS(list.back(), i);
       int i2 = 0;
       for(CDList<int>::const_iterator j = list.begin();
           j != list.end();
           ++j) {
-        TS_ASSERT(*j == i2++);
+        TS_ASSERT_EQUALS(*j, i2++);
       }
     }
-    TS_ASSERT(list.size() == N);
+    TS_ASSERT_EQUALS(list.size(), unsigned(N));
 
     for(int i = 0; i < N; ++i) {
-      TS_ASSERT(list[i] == i);
+      TS_ASSERT_EQUALS(list[i], i);
     }
   }
 
diff --git a/test/unit/context/context_mm_black.h b/test/unit/context/context_mm_black.h
index bda1cb141..e25d1f336 100644
--- a/test/unit/context/context_mm_black.h
+++ b/test/unit/context/context_mm_black.h
@@ -10,7 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** Black box testing of CVC4::Node.
+ ** Black box testing of CVC4::context::ContextMemoryManager.
  **/
 
 #include <cxxtest/TestSuite.h>
@@ -40,23 +40,24 @@ public:
     // Push, then allocate, then pop
     // We make sure that we don't allocate too much so that all the regions
     // should be reclaimed
-    int chunkSizeBytes = 16384;
-    int maxFreeChunks = 100;
-    int piecesPerChunk = 13;
-    int len = chunkSizeBytes / piecesPerChunk; // Length of the individual block
-    int N = maxFreeChunks*piecesPerChunk;
-    for (int p = 0; p < 5; ++ p) {
+    unsigned chunkSizeBytes = 16384;
+    unsigned maxFreeChunks = 100;
+    unsigned piecesPerChunk = 13;
+    unsigned len = chunkSizeBytes / piecesPerChunk; // Length of the individual block
+    unsigned N = maxFreeChunks*piecesPerChunk;
+    for(unsigned p = 0; p < 5; ++ p) {
       d_cmm->push();
-      for (int i = 0; i < N; ++i) {
+      for(unsigned i = 0; i < N; ++i) {
         char* newMem = (char*)d_cmm->newData(len);
         // We only setup the memory in the first run, the others should
         // reclaim the same memory
-        if (p == 0) {
-          for(int k = 0; k < len - 1; k ++)
+        if(p == 0) {
+          for(unsigned k = 0; k < len - 1; k ++) {
             newMem[k] = 'a';
+          }
           newMem[len-1] = 0;
         }
-        if (strlen(newMem) != len - 1) {
+        if(strlen(newMem) != len - 1) {
           cout << strlen(newMem) << " : " << len - 1 << endl;
         }
         TS_ASSERT(strlen(newMem) == len - 1);
@@ -64,22 +65,23 @@ public:
       d_cmm->pop();
     }
 
-    int factor = 3;
-    N = 16384/factor;
+    unsigned factor = 3;
+    N = 16384 / factor;
 
     // Push, then allocate, then pop all at once
-    for (int p = 0; p < 5; ++ p) {
+    for(unsigned p = 0; p < 5; ++ p) {
       d_cmm->push();
-      for (int i = 1; i < N; ++i) {
-        int len = i*factor;
+      for(unsigned i = 1; i < N; ++i) {
+        unsigned len = i * factor;
         char* newMem = (char*)d_cmm->newData(len);
-        for(int k = 0; k < len - 1; k ++)
+        for(unsigned k = 0; k < len - 1; k ++) {
           newMem[k] = 'a';
+        }
         newMem[len-1] = 0;
         TS_ASSERT(strlen(newMem) == len - 1);
       }
     }
-    for (int p = 0; p < 5; ++ p) {
+    for(unsigned p = 0; p < 5; ++ p) {
       d_cmm->pop();
     }
 
diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index e0d9d6bf4..e3b7811a4 100644
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -149,8 +149,6 @@ public:
   }
 
   void testCDAttributes() {
-    AttributeManager& am = d_nm->d_attrManager;
-
     //Debug.on("boolattr");
 
     Node a = d_nm->mkVar(d_booleanType);
@@ -279,8 +277,6 @@ public:
   }
 
   void testAttributes() {
-    AttributeManager& am = d_nm->d_attrManager;
-
     //Debug.on("boolattr");
 
     Node a = d_nm->mkVar(d_booleanType);
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 17657683d..23d1daf4e 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -423,10 +423,10 @@ public:
 #endif /* CVC4_ASSERTIONS */
   }
 
-  void testNaryExpForSize(Kind k, int N) {
+  void testNaryExpForSize(Kind k, unsigned N) {
     NodeBuilder<> nbz(k);
     Node trueNode = d_nodeManager->mkConst(true);
-    for(int i = 0; i < N; ++i) {
+    for(unsigned i = 0; i < N; ++i) {
       nbz << trueNode;
     }
     Node result = nbz;
@@ -452,7 +452,7 @@ public:
     srand(0);
     int trials = 500;
     for(int i = 0; i < trials; ++i) {
-      int N = rand() % 1000 + 2;
+      unsigned N = rand() % 1000 + 2;
       testNaryExpForSize(AND, N);
     }
 
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index eec6949f0..4521f3bf6 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -64,8 +64,8 @@ public:
     }
   }
 
-#define K 30
-#define LARGE_K UINT_MAX/40
+#define K 30u
+#define LARGE_K UINT_MAX / 40
 
   Kind specKind;
 
@@ -84,23 +84,23 @@ public:
     /* default size tests */
     NodeBuilder<> def;
     TS_ASSERT_EQUALS(def.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_EQUALS(def.getNumChildren(), 0);
+    TS_ASSERT_EQUALS(def.getNumChildren(), 0u);
     TS_ASSERT_EQUALS(def.begin(), def.end());
 
     NodeBuilder<> spec(specKind);
     TS_ASSERT_EQUALS(spec.getKind(), specKind);
-    TS_ASSERT_EQUALS(spec.getNumChildren(), 0);
+    TS_ASSERT_EQUALS(spec.getNumChildren(), 0u);
     TS_ASSERT_EQUALS(spec.begin(), spec.end());
 
 
     NodeBuilder<> from_nm(d_nm);
     TS_ASSERT_EQUALS(from_nm.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_EQUALS(from_nm.getNumChildren(), 0);
+    TS_ASSERT_EQUALS(from_nm.getNumChildren(), 0u);
     TS_ASSERT_EQUALS(from_nm.begin(), from_nm.end());
 
     NodeBuilder<> from_nm_kind(d_nm, specKind);
     TS_ASSERT_EQUALS(from_nm_kind.getKind(), specKind);
-    TS_ASSERT_EQUALS(from_nm_kind.getNumChildren(), 0);
+    TS_ASSERT_EQUALS(from_nm_kind.getNumChildren(), 0u);
     TS_ASSERT_EQUALS(from_nm_kind.begin(), from_nm_kind.end());
 
 
@@ -108,23 +108,23 @@ public:
 
     NodeBuilder<K> ws;
     TS_ASSERT_EQUALS(ws.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_EQUALS(ws.getNumChildren(), 0);
+    TS_ASSERT_EQUALS(ws.getNumChildren(), 0u);
     TS_ASSERT_EQUALS(ws.begin(), ws.end());
 
     NodeBuilder<K> ws_kind(specKind);
     TS_ASSERT_EQUALS(ws_kind.getKind(), specKind);
-    TS_ASSERT_EQUALS(ws_kind.getNumChildren(), 0);
+    TS_ASSERT_EQUALS(ws_kind.getNumChildren(), 0u);
     TS_ASSERT_EQUALS(ws_kind.begin(), ws_kind.end());
 
 
     NodeBuilder<K> ws_from_nm(d_nm);
     TS_ASSERT_EQUALS(ws_from_nm.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_EQUALS(ws_from_nm.getNumChildren(), 0);
+    TS_ASSERT_EQUALS(ws_from_nm.getNumChildren(), 0u);
     TS_ASSERT_EQUALS(ws_from_nm.begin(), ws_from_nm.end());
 
     NodeBuilder<K> ws_from_nm_kind(d_nm, specKind);
     TS_ASSERT_EQUALS(ws_from_nm_kind.getKind(), specKind);
-    TS_ASSERT_EQUALS(ws_from_nm_kind.getNumChildren(), 0);
+    TS_ASSERT_EQUALS(ws_from_nm_kind.getNumChildren(), 0u);
     TS_ASSERT_EQUALS(ws_from_nm_kind.begin(), ws_from_nm_kind.end());
 
 
@@ -137,23 +137,23 @@ public:
 
     NodeBuilder<> copy(def);
     TS_ASSERT_EQUALS(copy.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_EQUALS(copy.getNumChildren(), 0);
+    TS_ASSERT_EQUALS(copy.getNumChildren(), 0u);
     TS_ASSERT_EQUALS(copy.begin(), copy.end());
 
     NodeBuilder<K> cp_ws(ws);
     TS_ASSERT_EQUALS(cp_ws.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_EQUALS(cp_ws.getNumChildren(), 0);
+    TS_ASSERT_EQUALS(cp_ws.getNumChildren(), 0u);
     TS_ASSERT_EQUALS(cp_ws.begin(), cp_ws.end());
 
 
     NodeBuilder<K-10> cp_from_larger(ws);
     TS_ASSERT_EQUALS(cp_from_larger.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_EQUALS(cp_from_larger.getNumChildren(), 0);
+    TS_ASSERT_EQUALS(cp_from_larger.getNumChildren(), 0u);
     TS_ASSERT_EQUALS(cp_from_larger.begin(), cp_from_larger.end());
 
     NodeBuilder<K+10> cp_from_smaller(ws);
     TS_ASSERT_EQUALS(cp_from_smaller.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_EQUALS(cp_from_smaller.getNumChildren(), 0);
+    TS_ASSERT_EQUALS(cp_from_smaller.getNumChildren(), 0u);
     TS_ASSERT_EQUALS(cp_from_smaller.begin(), cp_from_smaller.end());
 
   }
@@ -174,14 +174,14 @@ public:
     TS_ASSERT_DIFFERS(ws.begin(), ws.end());
 
     NodeBuilder<K>::iterator iter = ws.begin();
-    for(int i = 0; i < K; ++i){
+    for(unsigned i = 0; i < K; ++i){
       TS_ASSERT_DIFFERS(iter, ws.end());
       ++iter;
     }
     TS_ASSERT_EQUALS(iter, ws.end());
 
     NodeBuilder<K>::const_iterator citer = ws.begin();
-    for(int i = 0; i < K; ++i){
+    for(unsigned i = 0; i < K; ++i){
       TS_ASSERT_DIFFERS(citer, ws.end());
       ++citer;
     }
@@ -196,14 +196,14 @@ public:
     TS_ASSERT_DIFFERS(smaller.begin(), smaller.end());
 
     NodeBuilder<>::iterator smaller_iter = smaller.begin();
-    for(int i = 0; i < K; ++i){
+    for(unsigned i = 0; i < K; ++i){
       TS_ASSERT_DIFFERS(smaller_iter, smaller.end());
       ++smaller_iter;
     }
     TS_ASSERT_EQUALS(iter, ws.end());
 
     NodeBuilder<>::const_iterator smaller_citer = smaller.begin();
-    for(int i = 0; i < K; ++i){
+    for(unsigned i = 0; i < K; ++i){
       TS_ASSERT_DIFFERS(smaller_citer, smaller.end());
       ++smaller_citer;
     }
@@ -261,24 +261,24 @@ public:
     /* unsigned getNumChildren() const; */
 
     NodeBuilder<> noKind;
-    TS_ASSERT_EQUALS(noKind.getNumChildren(), 0);
+    TS_ASSERT_EQUALS(noKind.getNumChildren(), 0u);
     push_back(noKind, K);
 
     TS_ASSERT_EQUALS(noKind.getNumChildren(), K);
 
     push_back(noKind, K);
-    TS_ASSERT_EQUALS(noKind.getNumChildren(), K+K);
+    TS_ASSERT_EQUALS(noKind.getNumChildren(), K + K);
 
     noKind << AND;// avoid exception on marking it used
     Node n = noKind;// avoid warning on clear()
     noKind.clear();
-    TS_ASSERT_EQUALS(noKind.getNumChildren(), 0);
+    TS_ASSERT_EQUALS(noKind.getNumChildren(), 0u);
     push_back(noKind, K);
 
     TS_ASSERT_EQUALS(noKind.getNumChildren(), K);
 
     push_back(noKind, K);
-    TS_ASSERT_EQUALS(noKind.getNumChildren(), K+K);
+    TS_ASSERT_EQUALS(noKind.getNumChildren(), K + K);
 
 #ifdef CVC4_ASSERTIONS
     noKind << specKind;
@@ -320,7 +320,7 @@ public:
 
     TS_ASSERT_EQUALS(arr[0], i_0);
     TS_ASSERT_EQUALS(arr[2], i_2);
-    for(int i = 3; i < K; ++i) {
+    for(unsigned i = 3; i < K; ++i) {
       TS_ASSERT_EQUALS(arr[i], d_nm->mkConst(true));
     }
 
@@ -328,7 +328,7 @@ public:
 
     TS_ASSERT_EQUALS(arr[0], i_0);
     TS_ASSERT_EQUALS(arr[2], i_2);
-    for(int i = 3; i < K; ++i) {
+    for(unsigned i = 3; i < K; ++i) {
       TS_ASSERT_EQUALS(arr[i], d_nm->mkConst(true));
     }
     TS_ASSERT_EQUALS(arr[K], i_K);
@@ -344,7 +344,7 @@ public:
     NodeBuilder<> nb;
 
     TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_EQUALS(nb.getNumChildren(), 0);
+    TS_ASSERT_EQUALS(nb.getNumChildren(), 0u);
     TS_ASSERT_EQUALS(nb.begin(), nb.end());
 
     nb << specKind;
@@ -358,7 +358,7 @@ public:
     nb.clear();
 
     TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_EQUALS(nb.getNumChildren(), 0);
+    TS_ASSERT_EQUALS(nb.getNumChildren(), 0u);
     TS_ASSERT_EQUALS(nb.begin(), nb.end());
 
     nb << specKind;
@@ -372,7 +372,7 @@ public:
     nb.clear(specKind);
 
     TS_ASSERT_EQUALS(nb.getKind(), specKind);
-    TS_ASSERT_EQUALS(nb.getNumChildren(), 0);
+    TS_ASSERT_EQUALS(nb.getNumChildren(), 0u);
     TS_ASSERT_EQUALS(nb.begin(), nb.end());
 
     push_back(nb, K);
@@ -380,7 +380,7 @@ public:
     nb.clear();
 
     TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_EQUALS(nb.getNumChildren(), 0);
+    TS_ASSERT_EQUALS(nb.getNumChildren(), 0u);
     TS_ASSERT_EQUALS(nb.begin(), nb.end());
 
   }
@@ -437,7 +437,7 @@ public:
     /* NodeBuilder& operator<<(const Node& n); */
     NodeBuilder<K> nb(specKind);
     TS_ASSERT_EQUALS(nb.getKind(), specKind);
-    TS_ASSERT_EQUALS(nb.getNumChildren(), 0);
+    TS_ASSERT_EQUALS(nb.getNumChildren(), 0u);
     TS_ASSERT_EQUALS(nb.begin(), nb.end());
     push_back(nb,K);
     TS_ASSERT_EQUALS(nb.getKind(), specKind);
@@ -451,13 +451,13 @@ public:
 
     NodeBuilder<> overflow(specKind);
     TS_ASSERT_EQUALS(overflow.getKind(), specKind);
-    TS_ASSERT_EQUALS(overflow.getNumChildren(), 0);
+    TS_ASSERT_EQUALS(overflow.getNumChildren(), 0u);
     TS_ASSERT_EQUALS(overflow.begin(), overflow.end());
 
     push_back(overflow,5*K+1);
 
     TS_ASSERT_EQUALS(overflow.getKind(), specKind);
-    TS_ASSERT_EQUALS(overflow.getNumChildren(), 5*K+1);
+    TS_ASSERT_EQUALS(overflow.getNumChildren(), 5 * K + 1);
     TS_ASSERT_DIFFERS(overflow.begin(), overflow.end());
 
   }
@@ -598,16 +598,16 @@ public:
     Node f = d_nm->mkVar(d_booleanType);
 
     Node m = a && b;
-    Node n = a && b || c;
+    Node n = (a && b) || c;
     Node o = d + e - b;
-    Node p = a && o || c;
+    Node p = (a && o) || c;
 
     Node x = d + e + o - m;
     Node y = f - a - c + e;
 
     Node q = a && b && c;
 
-    Node r = e && d && b && a || x && y || f || q && a;
+    Node r = (e && d && b && a) || (x && y) || f || (q && a);
 
     TS_ASSERT_EQUALS(m, d_nm->mkNode(AND, a, b));
     TS_ASSERT_EQUALS(n, d_nm->mkNode(OR, m, c));
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index 3e65be0b7..e059fa509 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -52,7 +52,7 @@ public:
   void testMkNode1() {
     Node x = d_nodeManager->mkVar("x",d_nodeManager->booleanType());
     Node n = d_nodeManager->mkNode(NOT, x);
-    TS_ASSERT_EQUALS( n.getNumChildren(), 1 );
+    TS_ASSERT_EQUALS( n.getNumChildren(), 1u );
     TS_ASSERT_EQUALS( n.getKind(), NOT);
     TS_ASSERT_EQUALS( n[0], x);
   }
@@ -61,7 +61,7 @@ public:
     Node x = d_nodeManager->mkVar("x",d_nodeManager->booleanType());
     Node y = d_nodeManager->mkVar("y",d_nodeManager->booleanType());
     Node n = d_nodeManager->mkNode(IMPLIES, x, y);
-    TS_ASSERT_EQUALS( n.getNumChildren(), 2 );
+    TS_ASSERT_EQUALS( n.getNumChildren(), 2u );
     TS_ASSERT_EQUALS( n.getKind(), IMPLIES);
     TS_ASSERT_EQUALS( n[0], x);
     TS_ASSERT_EQUALS( n[1], y);
@@ -72,7 +72,7 @@ public:
     Node y = d_nodeManager->mkVar("y",d_nodeManager->booleanType());
     Node z = d_nodeManager->mkVar("z",d_nodeManager->booleanType());
     Node n = d_nodeManager->mkNode(AND, x, y, z);
-    TS_ASSERT_EQUALS( n.getNumChildren(), 3 );
+    TS_ASSERT_EQUALS( n.getNumChildren(), 3u );
     TS_ASSERT_EQUALS( n.getKind(), AND);
     TS_ASSERT_EQUALS( n[0], x);
     TS_ASSERT_EQUALS( n[1], y);
@@ -85,12 +85,12 @@ public:
     Node x3 = d_nodeManager->mkVar("x3",d_nodeManager->booleanType());
     Node x4 = d_nodeManager->mkVar("x4",d_nodeManager->booleanType());
     Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4);
-    TS_ASSERT_EQUALS( n.getNumChildren(), 4 );
-    TS_ASSERT_EQUALS( n.getKind(), AND);
-    TS_ASSERT_EQUALS( n[0], x1);
-    TS_ASSERT_EQUALS( n[1], x2);
-    TS_ASSERT_EQUALS( n[2], x3);
-    TS_ASSERT_EQUALS( n[3], x4);
+    TS_ASSERT_EQUALS( n.getNumChildren(), 4u );
+    TS_ASSERT_EQUALS( n.getKind(), AND );
+    TS_ASSERT_EQUALS( n[0], x1 );
+    TS_ASSERT_EQUALS( n[1], x2 );
+    TS_ASSERT_EQUALS( n[2], x3 );
+    TS_ASSERT_EQUALS( n[3], x4 );
   }
 
   void testMkNode5() {
@@ -100,7 +100,7 @@ public:
     Node x4 = d_nodeManager->mkVar("x4",d_nodeManager->booleanType());
     Node x5 = d_nodeManager->mkVar("x5",d_nodeManager->booleanType());
     Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4, x5);
-    TS_ASSERT_EQUALS( n.getNumChildren(), 5 );
+    TS_ASSERT_EQUALS( n.getNumChildren(), 5u );
     TS_ASSERT_EQUALS( n.getKind(), AND);
     TS_ASSERT_EQUALS( n[0], x1);
     TS_ASSERT_EQUALS( n[1], x2);
@@ -120,7 +120,7 @@ public:
     Node n = d_nodeManager->mkNode(AND, args);
     TS_ASSERT_EQUALS( n.getNumChildren(), args.size() );
     TS_ASSERT_EQUALS( n.getKind(), AND);
-    for( int i=0; i < args.size(); ++i ) {
+    for( unsigned i = 0; i < args.size(); ++i ) {
       TS_ASSERT_EQUALS( n[i], args[i]);
     }
   }
@@ -136,7 +136,7 @@ public:
     Node n = d_nodeManager->mkNode(AND, args);
     TS_ASSERT_EQUALS( n.getNumChildren(), args.size() );
     TS_ASSERT_EQUALS( n.getKind(), AND);
-    for( int i=0; i < args.size(); ++i ) {
+    for( unsigned i = 0; i < args.size(); ++i ) {
       TS_ASSERT_EQUALS( n[i], args[i]);
     }
   }
@@ -145,7 +145,7 @@ public:
     Type* booleanType = d_nodeManager->booleanType();
     Node x = d_nodeManager->mkVar(booleanType);
     TS_ASSERT_EQUALS(x.getKind(),VARIABLE);
-    TS_ASSERT_EQUALS(x.getNumChildren(),0);
+    TS_ASSERT_EQUALS(x.getNumChildren(),0u);
     TS_ASSERT_EQUALS(x.getType(),booleanType);
   }
 
@@ -153,7 +153,7 @@ public:
     Type* booleanType = d_nodeManager->booleanType();
     Node x = d_nodeManager->mkVar("x", booleanType);
     TS_ASSERT_EQUALS(x.getKind(),VARIABLE);
-    TS_ASSERT_EQUALS(x.getNumChildren(),0);
+    TS_ASSERT_EQUALS(x.getNumChildren(),0u);
     TS_ASSERT_EQUALS(x.getAttribute(VarNameAttr()),"x");
     TS_ASSERT_EQUALS(x.getType(),booleanType);
   }
@@ -219,7 +219,7 @@ public:
     TS_ASSERT( t->isFunction() );
 
     FunctionType* ft = (FunctionType*)t;
-    TS_ASSERT_EQUALS(ft->getArgTypes().size(), 1);
+    TS_ASSERT_EQUALS(ft->getArgTypes().size(), 1u);
     TS_ASSERT_EQUALS(ft->getArgTypes()[0], booleanType);
     TS_ASSERT_EQUALS(ft->getRangeType(), booleanType);
 
diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h
index 28dbde933..9facd00f6 100644
--- a/test/unit/expr/node_white.h
+++ b/test/unit/expr/node_white.h
@@ -51,7 +51,7 @@ public:
   }
 
   void testNull() {
-    Node::s_null;
+    TS_ASSERT_EQUALS(Node::null(), Node::s_null);
   }
 
   void testCopyCtor() {
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 905294c27..24c8e407c 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -228,7 +228,7 @@ public:
 
     TS_ASSERT_EQUALS(got, f_x_eq_x);
 
-    TS_ASSERT_EQUALS(5, d_dummy->d_registered.size());
+    TS_ASSERT_EQUALS(5u, d_dummy->d_registered.size());
     TS_ASSERT(d_dummy->d_registered.find(x) != d_dummy->d_registered.end());
     TS_ASSERT(d_dummy->d_registered.find(f) != d_dummy->d_registered.end());
     TS_ASSERT(d_dummy->d_registered.find(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 369be5a16..c02214a25 100644
--- a/test/unit/theory/theory_uf_white.h
+++ b/test/unit/theory/theory_uf_white.h
@@ -145,7 +145,7 @@ public:
     d_euf->assertFact( f5_x_eq_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);
diff --git a/test/unit/util/integer_black.h b/test/unit/util/integer_black.h
index afd2145e3..c09db2207 100644
--- a/test/unit/util/integer_black.h
+++ b/test/unit/util/integer_black.h
@@ -45,16 +45,16 @@ public:
     TS_ASSERT_EQUALS(z4.getLong(), 0);
 
     Integer z5("7896890");
-    TS_ASSERT_EQUALS(z5.getUnsignedLong(), 7896890);
+    TS_ASSERT_EQUALS(z5.getUnsignedLong(), 7896890ul);
 
     Integer z6(z5);
-    TS_ASSERT_EQUALS(z5.getUnsignedLong(), 7896890);
-    TS_ASSERT_EQUALS(z6.getUnsignedLong(), 7896890);
+    TS_ASSERT_EQUALS(z5.getUnsignedLong(), 7896890ul);
+    TS_ASSERT_EQUALS(z6.getUnsignedLong(), 7896890ul);
 
 
     string bigValue("1536729");
     Integer z7(bigValue);
-    TS_ASSERT_EQUALS(z7.getUnsignedLong(), 1536729);
+    TS_ASSERT_EQUALS(z7.getUnsignedLong(), 1536729ul);
   }
 
   void testOperatorAssign(){
@@ -62,24 +62,24 @@ public:
     Integer y(79);
     Integer z(45789);
 
-    TS_ASSERT_EQUALS(x.getUnsignedLong(), 0);
-    TS_ASSERT_EQUALS(y.getUnsignedLong(), 79);
-    TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789);
+    TS_ASSERT_EQUALS(x.getUnsignedLong(), 0ul);
+    TS_ASSERT_EQUALS(y.getUnsignedLong(), 79ul);
+    TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789ul);
 
     x = y = z;
 
-    TS_ASSERT_EQUALS(x.getUnsignedLong(), 45789);
-    TS_ASSERT_EQUALS(y.getUnsignedLong(), 45789);
-    TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789);
+    TS_ASSERT_EQUALS(x.getUnsignedLong(), 45789ul);
+    TS_ASSERT_EQUALS(y.getUnsignedLong(), 45789ul);
+    TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789ul);
 
     Integer a(2);
 
     y = a;
 
-    TS_ASSERT_EQUALS(a.getUnsignedLong(), 2);
-    TS_ASSERT_EQUALS(y.getUnsignedLong(), 2);
-    TS_ASSERT_EQUALS(x.getUnsignedLong(), 45789);
-    TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789);
+    TS_ASSERT_EQUALS(a.getUnsignedLong(), 2ul);
+    TS_ASSERT_EQUALS(y.getUnsignedLong(), 2ul);
+    TS_ASSERT_EQUALS(x.getUnsignedLong(), 45789ul);
+    TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789ul);
   }
 
   void testOperatorEquals(){
diff --git a/test/unit/util/integer_white.h b/test/unit/util/integer_white.h
index ef0e0b92f..3a86289a3 100644
--- a/test/unit/util/integer_white.h
+++ b/test/unit/util/integer_white.h
@@ -33,9 +33,9 @@ public:
     Integer fits_in_16_bytes("7890D789D33234027890D789D3323402", 16);
 
 
-    TS_ASSERT_THROWS_NOTHING(size_t res0 = zero.hash());
-    TS_ASSERT_THROWS_NOTHING(size_t res1 = fits_in_2_bytes.hash());
-    TS_ASSERT_THROWS_NOTHING(size_t res2 = fits_in_16_bytes.hash());
-    TS_ASSERT_THROWS_NOTHING(size_t res3 = large.hash());
+    TS_ASSERT_THROWS_NOTHING(zero.hash());
+    TS_ASSERT_THROWS_NOTHING(fits_in_2_bytes.hash());
+    TS_ASSERT_THROWS_NOTHING(fits_in_16_bytes.hash());
+    TS_ASSERT_THROWS_NOTHING(large.hash());
   }
 };
diff --git a/test/unit/util/rational_white.h b/test/unit/util/rational_white.h
index 559b457cb..8a7f04fd3 100644
--- a/test/unit/util/rational_white.h
+++ b/test/unit/util/rational_white.h
@@ -104,26 +104,26 @@ public:
     Rational y(78,6);
     Rational z(45789,1);
 
-    TS_ASSERT_EQUALS(x.getNumerator().getUnsignedLong(), 0);
-    TS_ASSERT_EQUALS(y.getNumerator().getUnsignedLong(), 13);
-    TS_ASSERT_EQUALS(z.getNumerator().getUnsignedLong(), 45789);
+    TS_ASSERT_EQUALS(x.getNumerator().getUnsignedLong(), 0ul);
+    TS_ASSERT_EQUALS(y.getNumerator().getUnsignedLong(), 13ul);
+    TS_ASSERT_EQUALS(z.getNumerator().getUnsignedLong(), 45789ul);
 
     x = y = z;
 
-    TS_ASSERT_EQUALS(x.getNumerator().getUnsignedLong(), 45789);
-    TS_ASSERT_EQUALS(y.getNumerator().getUnsignedLong(), 45789);
-    TS_ASSERT_EQUALS(z.getNumerator().getUnsignedLong(), 45789);
+    TS_ASSERT_EQUALS(x.getNumerator().getUnsignedLong(), 45789ul);
+    TS_ASSERT_EQUALS(y.getNumerator().getUnsignedLong(), 45789ul);
+    TS_ASSERT_EQUALS(z.getNumerator().getUnsignedLong(), 45789ul);
 
     Rational a(78,91);
 
     y = a;
 
-    TS_ASSERT_EQUALS(a.getNumerator().getUnsignedLong(), 6);
-    TS_ASSERT_EQUALS(a.getDenominator().getUnsignedLong(), 7);
-    TS_ASSERT_EQUALS(y.getNumerator().getUnsignedLong(), 6);
-    TS_ASSERT_EQUALS(y.getDenominator().getUnsignedLong(), 7);
-    TS_ASSERT_EQUALS(x.getNumerator().getUnsignedLong(), 45789);
-    TS_ASSERT_EQUALS(z.getNumerator().getUnsignedLong(), 45789);
+    TS_ASSERT_EQUALS(a.getNumerator().getUnsignedLong(), 6ul);
+    TS_ASSERT_EQUALS(a.getDenominator().getUnsignedLong(), 7ul);
+    TS_ASSERT_EQUALS(y.getNumerator().getUnsignedLong(), 6ul);
+    TS_ASSERT_EQUALS(y.getDenominator().getUnsignedLong(), 7ul);
+    TS_ASSERT_EQUALS(x.getNumerator().getUnsignedLong(), 45789ul);
+    TS_ASSERT_EQUALS(z.getNumerator().getUnsignedLong(), 45789ul);
   }
 
   void testToStringStuff(){
@@ -416,8 +416,8 @@ public:
     Rational one_word(75890L,590L);
     Rational two_words("7890D789D33234027890D789D3323402", 16);
 
-    TS_ASSERT_EQUALS(zero.hash(), 1);
-    TS_ASSERT_EQUALS(one_word.hash(), 7589 xor 59);
+    TS_ASSERT_EQUALS(zero.hash(), 1u);
+    TS_ASSERT_EQUALS(one_word.hash(), 7589u xor 59u);
     TS_ASSERT_EQUALS(two_words.hash(),
 		     (two_words.getNumerator().hash()) xor 1);
     TS_ASSERT_EQUALS(large.hash(),