Fix "catching polymorphic type by value" warnings (#2556)

When using the `TS_ASSERT_THROWS` marco from CxxTest, we have to make
sure that we use a reference type for the exception, otherwise the unit
test tries to catch the exception by value, resulting in "catching
polymorphic type by value" warnings.

22 files changed, 248 insertions, 211 deletions

diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h
index 8a31f70ca..b6b7f436c 100644
--- a/test/unit/context/cdlist_black.h
+++ b/test/unit/context/cdlist_black.h
@@ -142,11 +142,12 @@ class CDListBlack : public CxxTest::TestSuite {
         {
           // We cap it at UINT_MAX, preferring to terminate with a
           // failure than run indefinitely.
-          for (unsigned i = 0; i < UINT_MAX; ++i) {
+          for (unsigned i = 0; i < UINT_MAX; ++i)
+          {
             list.push_back(i);
           }
         },
-        bad_alloc);
+        bad_alloc&);
 
 #endif /* CVC4_MEMORY_LIMITING_DISABLED */
   }
diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h
index 2d2b3f409..1cb7e50e7 100644
--- a/test/unit/context/cdmap_black.h
+++ b/test/unit/context/cdmap_black.h
@@ -164,9 +164,9 @@ class CDMapBlack : public CxxTest::TestSuite {
             ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 317}}));
 
         TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 317),
-                         AssertionException);
+                         AssertionException&);
         TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 472),
-                         AssertionException);
+                         AssertionException&);
         map.insert(23, 472);
 
         TS_ASSERT(
@@ -178,7 +178,7 @@ class CDMapBlack : public CxxTest::TestSuite {
             ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}}));
 
           TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0),
-                           AssertionException);
+                           AssertionException&);
           map.insert(23, 1024);
 
           TS_ASSERT(
@@ -194,7 +194,8 @@ class CDMapBlack : public CxxTest::TestSuite {
       TS_ASSERT(
           ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}, {23, 317}}));
 
-      TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0), AssertionException);
+      TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0),
+                       AssertionException&);
       map.insert(23, 477);
 
       TS_ASSERT(
@@ -202,7 +203,7 @@ class CDMapBlack : public CxxTest::TestSuite {
       d_context->pop();
     }
 
-    TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0), AssertionException);
+    TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0), AssertionException&);
 
     TS_ASSERT(
         ElementsAre(map, {{3, 4}, {23, 317}}));
diff --git a/test/unit/context/cdmap_white.h b/test/unit/context/cdmap_white.h
index 0f111cd61..53d523c82 100644
--- a/test/unit/context/cdmap_white.h
+++ b/test/unit/context/cdmap_white.h
@@ -38,12 +38,12 @@ class CDMapWhite : public CxxTest::TestSuite {
 
     TS_ASSERT_THROWS_NOTHING(map.makeCurrent());
 
-    TS_ASSERT_THROWS(map.update(), UnreachableCodeException);
+    TS_ASSERT_THROWS(map.update(), UnreachableCodeException&);
 
-    TS_ASSERT_THROWS(map.save(d_context->getCMM()), UnreachableCodeException);
-    TS_ASSERT_THROWS(map.restore(&map), 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);
+    TS_ASSERT_THROWS(map.makeCurrent(), UnreachableCodeException&);
   }
 };
diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h
index b4be4197c..4f867525d 100644
--- a/test/unit/context/context_black.h
+++ b/test/unit/context/context_black.h
@@ -106,8 +106,8 @@ private:
     d_context->push();
     d_context->pop();
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS( d_context->pop(), AssertionException );
-    TS_ASSERT_THROWS( d_context->pop(), AssertionException );
+    TS_ASSERT_THROWS(d_context->pop(), AssertionException&);
+    TS_ASSERT_THROWS(d_context->pop(), AssertionException&);
 #endif /* CVC4_ASSERTIONS */
   }
 
diff --git a/test/unit/context/context_mm_black.h b/test/unit/context/context_mm_black.h
index beace137e..2684d643c 100644
--- a/test/unit/context/context_mm_black.h
+++ b/test/unit/context/context_mm_black.h
@@ -90,7 +90,7 @@ private:
     }
 
     // Try popping out of scope
-    TS_ASSERT_THROWS(d_cmm->pop(), CVC4::AssertionException);
+    TS_ASSERT_THROWS(d_cmm->pop(), CVC4::AssertionException&);
 #endif /* __CVC4__CONTEXT__CONTEXT_MM_H */
   }
 
diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h
index 9c604aa52..c2a33cc59 100644
--- a/test/unit/expr/expr_manager_public.h
+++ b/test/unit/expr/expr_manager_public.h
@@ -70,7 +70,7 @@ private:
     {
       delete d_exprManager;
     }
-    catch (Exception e)
+    catch (Exception& e)
     {
       cerr << "Exception during tearDown():" << endl << e;
       throw;
@@ -118,12 +118,14 @@ private:
 
   void testMkAssociativeTooFew() {
     std::vector<Expr> vars = mkVars(d_exprManager->booleanType(), 1);
-    TS_ASSERT_THROWS( d_exprManager->mkAssociative(AND,vars), IllegalArgumentException);
+    TS_ASSERT_THROWS(d_exprManager->mkAssociative(AND, vars),
+                     IllegalArgumentException&);
   }
 
   void testMkAssociativeBadKind() {
     std::vector<Expr> vars = mkVars(d_exprManager->integerType(), 10);
-    TS_ASSERT_THROWS( d_exprManager->mkAssociative(LEQ,vars), IllegalArgumentException);
+    TS_ASSERT_THROWS(d_exprManager->mkAssociative(LEQ, vars),
+                     IllegalArgumentException&);
   }
 
 };
diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index d8774db82..9ff5e6578 100644
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -80,7 +80,7 @@ private:
       r1 = new Expr(d_em->mkConst(Rational(1, 5)));
       r2 = new Expr(d_em->mkConst(Rational("0")));
     }
-    catch (Exception e)
+    catch (Exception& e)
     {
       cerr << "Exception during setUp():" << endl << e;
       throw;
@@ -106,7 +106,9 @@ private:
       delete a_bool;
 
       delete d_em;
-    } catch(Exception e) {
+    }
+    catch (Exception& e)
+    {
       cerr << "Exception during tearDown():" << endl << e;
       throw;
     }
@@ -265,13 +267,13 @@ private:
     TS_ASSERT(d_apply_fun_bool->hasOperator());
     TS_ASSERT(!null->hasOperator());
 
-    TS_ASSERT_THROWS(a_bool->getOperator(), IllegalArgumentException);
-    TS_ASSERT_THROWS(b_bool->getOperator(), IllegalArgumentException);
+    TS_ASSERT_THROWS(a_bool->getOperator(), IllegalArgumentException&);
+    TS_ASSERT_THROWS(b_bool->getOperator(), IllegalArgumentException&);
     TS_ASSERT(c_bool_and->getOperator() == *and_op);
-    TS_ASSERT_THROWS(plus_op->getOperator(), IllegalArgumentException);
-    TS_ASSERT_THROWS(and_op->getOperator(), IllegalArgumentException);
+    TS_ASSERT_THROWS(plus_op->getOperator(), IllegalArgumentException&);
+    TS_ASSERT_THROWS(and_op->getOperator(), IllegalArgumentException&);
     TS_ASSERT(d_apply_fun_bool->getOperator() == *fun_op);
-    TS_ASSERT_THROWS(null->getOperator(), IllegalArgumentException);
+    TS_ASSERT_THROWS(null->getOperator(), IllegalArgumentException&);
   }
 
   void testGetType() {
@@ -281,11 +283,11 @@ private:
     TS_ASSERT(a_bool->getType(true) == d_em->booleanType());
     TS_ASSERT(b_bool->getType(false) == d_em->booleanType());
     TS_ASSERT(b_bool->getType(true) == d_em->booleanType());
-    TS_ASSERT_THROWS(d_em->mkExpr(MULT,*a_bool,*b_bool).getType(true),
-                     TypeCheckingException);
-// These need better support for operators
-//    TS_ASSERT(and_op->getType().isNull());
-//    TS_ASSERT(plus_op->getType().isNull());
+    TS_ASSERT_THROWS(d_em->mkExpr(MULT, *a_bool, *b_bool).getType(true),
+                     TypeCheckingException&);
+    // These need better support for operators
+    //    TS_ASSERT(and_op->getType().isNull());
+    //    TS_ASSERT(plus_op->getType().isNull());
     TS_ASSERT(d_apply_fun_bool->getType() == d_em->booleanType());
     TS_ASSERT(i1->getType().isInteger());
     TS_ASSERT(i2->getType().isInteger());
@@ -426,25 +428,26 @@ private:
     /* template <class T>
        const T& getConst() const; */
 
-    TS_ASSERT_THROWS(a_bool->getConst<Kind>(), IllegalArgumentException);
-    TS_ASSERT_THROWS(b_bool->getConst<Kind>(), IllegalArgumentException);
-    TS_ASSERT_THROWS(c_bool_and->getConst<Kind>(), IllegalArgumentException);
+    TS_ASSERT_THROWS(a_bool->getConst<Kind>(), IllegalArgumentException&);
+    TS_ASSERT_THROWS(b_bool->getConst<Kind>(), IllegalArgumentException&);
+    TS_ASSERT_THROWS(c_bool_and->getConst<Kind>(), IllegalArgumentException&);
     TS_ASSERT(and_op->getConst<Kind>() == AND);
-    TS_ASSERT_THROWS(and_op->getConst<Rational>(), IllegalArgumentException);
+    TS_ASSERT_THROWS(and_op->getConst<Rational>(), IllegalArgumentException&);
     TS_ASSERT(plus_op->getConst<Kind>() == PLUS);
-    TS_ASSERT_THROWS(plus_op->getConst<Rational>(), IllegalArgumentException);
-    TS_ASSERT_THROWS(d_apply_fun_bool->getConst<Kind>(), IllegalArgumentException);
-    TS_ASSERT_THROWS(null->getConst<Kind>(), IllegalArgumentException);
+    TS_ASSERT_THROWS(plus_op->getConst<Rational>(), IllegalArgumentException&);
+    TS_ASSERT_THROWS(d_apply_fun_bool->getConst<Kind>(),
+                     IllegalArgumentException&);
+    TS_ASSERT_THROWS(null->getConst<Kind>(), IllegalArgumentException&);
 
     TS_ASSERT(i1->getConst<Rational>() == 0);
     TS_ASSERT(i2->getConst<Rational>() == 23);
     TS_ASSERT(r1->getConst<Rational>() == Rational(1, 5));
     TS_ASSERT(r2->getConst<Rational>() == Rational("0"));
 
-    TS_ASSERT_THROWS(i1->getConst<Kind>(), IllegalArgumentException);
-    TS_ASSERT_THROWS(i2->getConst<Kind>(), IllegalArgumentException);
-    TS_ASSERT_THROWS(r1->getConst<Kind>(), IllegalArgumentException);
-    TS_ASSERT_THROWS(r2->getConst<Kind>(), IllegalArgumentException);
+    TS_ASSERT_THROWS(i1->getConst<Kind>(), IllegalArgumentException&);
+    TS_ASSERT_THROWS(i2->getConst<Kind>(), IllegalArgumentException&);
+    TS_ASSERT_THROWS(r1->getConst<Kind>(), IllegalArgumentException&);
+    TS_ASSERT_THROWS(r2->getConst<Kind>(), IllegalArgumentException&);
   }
 
   void testGetExprManager() {
diff --git a/test/unit/expr/kind_map_black.h b/test/unit/expr/kind_map_black.h
index ef2cc8881..33af64580 100644
--- a/test/unit/expr/kind_map_black.h
+++ b/test/unit/expr/kind_map_black.h
@@ -100,7 +100,7 @@ public:
     TS_ASSERT(!(AND ^ AND ^ AND).isEmpty());
 
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(~LAST_KIND, AssertArgumentException);
+    TS_ASSERT_THROWS(~LAST_KIND, AssertArgumentException&);
 #endif /* CVC4_ASSERTIONS */
   }
 
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 461d59498..2415bd5e4 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -179,8 +179,8 @@ class NodeBlack : public CxxTest::TestSuite {
 
 #ifdef CVC4_ASSERTIONS
     // Basic bounds check on a node w/out children
-    TS_ASSERT_THROWS(Node::null()[-1], AssertionException);
-    TS_ASSERT_THROWS(Node::null()[0], AssertionException);
+    TS_ASSERT_THROWS(Node::null()[-1], AssertionException&);
+    TS_ASSERT_THROWS(Node::null()[0], AssertionException&);
 #endif /* CVC4_ASSERTIONS */
 
     // Basic access check
@@ -198,8 +198,8 @@ class NodeBlack : public CxxTest::TestSuite {
 
 #ifdef CVC4_ASSERTIONS
     // Bounds check on a node with children
-    TS_ASSERT_THROWS(ite == ite[-1], AssertionException);
-    TS_ASSERT_THROWS(ite == ite[4], AssertionException);
+    TS_ASSERT_THROWS(ite == ite[-1], AssertionException&);
+    TS_ASSERT_THROWS(ite == ite[4], AssertionException&);
 #endif /* CVC4_ASSERTIONS */
   }
 
@@ -420,8 +420,8 @@ class NodeBlack : public CxxTest::TestSuite {
 
     TS_ASSERT(f == fa.getOperator());
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(f.getOperator(), IllegalArgumentException);
-    TS_ASSERT_THROWS(a.getOperator(), IllegalArgumentException);
+    TS_ASSERT_THROWS(f.getOperator(), IllegalArgumentException&);
+    TS_ASSERT_THROWS(a.getOperator(), IllegalArgumentException&);
 #endif /* CVC4_ASSERTIONS */
   }
 
@@ -459,10 +459,10 @@ class NodeBlack : public CxxTest::TestSuite {
     }
 
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(testNaryExpForSize(AND, 0), AssertionException);
-    TS_ASSERT_THROWS(testNaryExpForSize(AND, 1), AssertionException);
-    TS_ASSERT_THROWS(testNaryExpForSize(NOT, 0), AssertionException);
-    TS_ASSERT_THROWS(testNaryExpForSize(NOT, 2), AssertionException);
+    TS_ASSERT_THROWS(testNaryExpForSize(AND, 0), AssertionException&);
+    TS_ASSERT_THROWS(testNaryExpForSize(AND, 1), AssertionException&);
+    TS_ASSERT_THROWS(testNaryExpForSize(NOT, 0), AssertionException&);
+    TS_ASSERT_THROWS(testNaryExpForSize(NOT, 2), AssertionException&);
 #endif /* CVC4_ASSERTIONS */
   }
 
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index f4fbbb5d9..963219291 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -90,9 +90,9 @@ private:
     NodeBuilder<> def;
     TS_ASSERT_EQUALS(def.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(def.getNumChildren(), AssertionException);
-    TS_ASSERT_THROWS(def.begin(), AssertionException);
-    TS_ASSERT_THROWS(def.end(), AssertionException);
+    TS_ASSERT_THROWS(def.getNumChildren(), AssertionException&);
+    TS_ASSERT_THROWS(def.begin(), AssertionException&);
+    TS_ASSERT_THROWS(def.end(), AssertionException&);
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<> spec(specKind);
@@ -104,9 +104,9 @@ private:
     NodeBuilder<> from_nm(d_nm);
     TS_ASSERT_EQUALS(from_nm.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(from_nm.getNumChildren(), AssertionException);
-    TS_ASSERT_THROWS(from_nm.begin(), AssertionException);
-    TS_ASSERT_THROWS(from_nm.end(), AssertionException);
+    TS_ASSERT_THROWS(from_nm.getNumChildren(), AssertionException&);
+    TS_ASSERT_THROWS(from_nm.begin(), AssertionException&);
+    TS_ASSERT_THROWS(from_nm.end(), AssertionException&);
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<> from_nm_kind(d_nm, specKind);
@@ -120,9 +120,9 @@ private:
     NodeBuilder<K> ws;
     TS_ASSERT_EQUALS(ws.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(ws.getNumChildren(), AssertionException);
-    TS_ASSERT_THROWS(ws.begin(), AssertionException);
-    TS_ASSERT_THROWS(ws.end(), AssertionException);
+    TS_ASSERT_THROWS(ws.getNumChildren(), AssertionException&);
+    TS_ASSERT_THROWS(ws.begin(), AssertionException&);
+    TS_ASSERT_THROWS(ws.end(), AssertionException&);
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<K> ws_kind(specKind);
@@ -134,9 +134,9 @@ private:
     NodeBuilder<K> ws_from_nm(d_nm);
     TS_ASSERT_EQUALS(ws_from_nm.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(ws_from_nm.getNumChildren(), AssertionException);
-    TS_ASSERT_THROWS(ws_from_nm.begin(), AssertionException);
-    TS_ASSERT_THROWS(ws_from_nm.end(), AssertionException);
+    TS_ASSERT_THROWS(ws_from_nm.getNumChildren(), AssertionException&);
+    TS_ASSERT_THROWS(ws_from_nm.begin(), AssertionException&);
+    TS_ASSERT_THROWS(ws_from_nm.end(), AssertionException&);
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<K> ws_from_nm_kind(d_nm, specKind);
@@ -158,33 +158,33 @@ private:
     NodeBuilder<> copy(def);
     TS_ASSERT_EQUALS(copy.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(copy.getNumChildren(), AssertionException);
-    TS_ASSERT_THROWS(copy.begin(), AssertionException);
-    TS_ASSERT_THROWS(copy.end(), AssertionException);
+    TS_ASSERT_THROWS(copy.getNumChildren(), AssertionException&);
+    TS_ASSERT_THROWS(copy.begin(), AssertionException&);
+    TS_ASSERT_THROWS(copy.end(), AssertionException&);
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<K> cp_ws(ws);
     TS_ASSERT_EQUALS(cp_ws.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(cp_ws.getNumChildren(), AssertionException);
-    TS_ASSERT_THROWS(cp_ws.begin(), AssertionException);
-    TS_ASSERT_THROWS(cp_ws.end(), AssertionException);
+    TS_ASSERT_THROWS(cp_ws.getNumChildren(), AssertionException&);
+    TS_ASSERT_THROWS(cp_ws.begin(), AssertionException&);
+    TS_ASSERT_THROWS(cp_ws.end(), AssertionException&);
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<K-10> cp_from_larger(ws);
     TS_ASSERT_EQUALS(cp_from_larger.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(cp_from_larger.getNumChildren(), AssertionException);
-    TS_ASSERT_THROWS(cp_from_larger.begin(), AssertionException);
-    TS_ASSERT_THROWS(cp_from_larger.end(), AssertionException);
+    TS_ASSERT_THROWS(cp_from_larger.getNumChildren(), AssertionException&);
+    TS_ASSERT_THROWS(cp_from_larger.begin(), AssertionException&);
+    TS_ASSERT_THROWS(cp_from_larger.end(), AssertionException&);
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<K+10> cp_from_smaller(ws);
     TS_ASSERT_EQUALS(cp_from_smaller.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(cp_from_smaller.getNumChildren(), AssertionException);
-    TS_ASSERT_THROWS(cp_from_smaller.begin(), AssertionException);
-    TS_ASSERT_THROWS(cp_from_smaller.end(), AssertionException);
+    TS_ASSERT_THROWS(cp_from_smaller.getNumChildren(), AssertionException&);
+    TS_ASSERT_THROWS(cp_from_smaller.begin(), AssertionException&);
+    TS_ASSERT_THROWS(cp_from_smaller.end(), AssertionException&);
 #endif /* CVC4_ASSERTIONS */
   }
 
@@ -282,7 +282,7 @@ private:
     Node n = noKind;
 
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(noKind.getKind(), AssertionException);
+    TS_ASSERT_THROWS(noKind.getKind(), AssertionException&);
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<> spec(PLUS);
@@ -297,7 +297,7 @@ private:
 
     NodeBuilder<> nb;
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException);
+    TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException&);
 #endif /* CVC4_ASSERTIONS */
     nb << PLUS << x << x;
 
@@ -309,7 +309,7 @@ private:
     Node n = nb;// avoid warning on clear()
     nb.clear();
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException);
+    TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException&);
 #endif /* CVC4_ASSERTIONS */
     nb.clear(PLUS);
     TS_ASSERT_EQUALS(nb.getNumChildren(), 0u);
@@ -321,9 +321,9 @@ private:
     TS_ASSERT_EQUALS(nb.getNumChildren(), 6u);
 
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS( nb << PLUS, AssertionException );
+    TS_ASSERT_THROWS(nb << PLUS, AssertionException&);
     n = nb;
-    TS_ASSERT_THROWS( nb.getNumChildren(), AssertionException );
+    TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException&);
 #endif /* CVC4_ASSERTIONS */
   }
 
@@ -342,7 +342,7 @@ private:
 
 #ifdef CVC4_ASSERTIONS
     TS_ASSERT_THROWS(arr[-1], AssertionException&);
-    TS_ASSERT_THROWS(arr[0], AssertionException);
+    TS_ASSERT_THROWS(arr[0], AssertionException&);
 #endif /* CVC4_ASSERTIONS */
 
     arr << i_0;
@@ -375,7 +375,7 @@ private:
 
 #ifdef CVC4_ASSERTIONS
     Node n = arr;
-    TS_ASSERT_THROWS(arr[0], AssertionException);
+    TS_ASSERT_THROWS(arr[0], AssertionException&);
 #endif /* CVC4_ASSERTIONS */
   }
 
@@ -385,9 +385,9 @@ private:
 
     TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException);
-    TS_ASSERT_THROWS(nb.begin(), AssertionException);
-    TS_ASSERT_THROWS(nb.end(), AssertionException);
+    TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException&);
+    TS_ASSERT_THROWS(nb.begin(), AssertionException&);
+    TS_ASSERT_THROWS(nb.end(), AssertionException&);
 #endif /* CVC4_ASSERTIONS */
 
     nb << specKind;
@@ -402,9 +402,9 @@ private:
 
     TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException);
-    TS_ASSERT_THROWS(nb.begin(), AssertionException);
-    TS_ASSERT_THROWS(nb.end(), AssertionException);
+    TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException&);
+    TS_ASSERT_THROWS(nb.begin(), AssertionException&);
+    TS_ASSERT_THROWS(nb.end(), AssertionException&);
 #endif /* CVC4_ASSERTIONS */
 
     nb << specKind;
@@ -427,9 +427,9 @@ private:
 
     TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException);
-    TS_ASSERT_THROWS(nb.begin(), AssertionException);
-    TS_ASSERT_THROWS(nb.end(), AssertionException);
+    TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException&);
+    TS_ASSERT_THROWS(nb.begin(), AssertionException&);
+    TS_ASSERT_THROWS(nb.end(), AssertionException&);
 #endif /* CVC4_ASSERTIONS */
   }
 
@@ -438,7 +438,7 @@ private:
 
 #ifdef CVC4_ASSERTIONS
     NodeBuilder<> spec(specKind);
-    TS_ASSERT_THROWS( spec << PLUS, AssertionException );
+    TS_ASSERT_THROWS(spec << PLUS, AssertionException&);
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<> noSpec;
@@ -457,12 +457,12 @@ private:
     nb.clear(PLUS);
 
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(n = nb, AssertionException);
+    TS_ASSERT_THROWS(n = nb, AssertionException&);
     nb.clear(PLUS);
 #endif /* CVC4_ASSERTIONS */
 
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS( nb << PLUS, AssertionException );
+    TS_ASSERT_THROWS(nb << PLUS, AssertionException&);
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<> testRef;
@@ -470,7 +470,7 @@ private:
 
 #ifdef CVC4_ASSERTIONS
     NodeBuilder<> testTwo;
-    TS_ASSERT_THROWS(testTwo << specKind << PLUS, AssertionException);
+    TS_ASSERT_THROWS(testTwo << specKind << PLUS, AssertionException&);
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<> testMixOrder1;
@@ -494,7 +494,7 @@ private:
 
 #ifdef CVC4_ASSERTIONS
     Node n = nb;
-    TS_ASSERT_THROWS(nb << n, AssertionException);
+    TS_ASSERT_THROWS(nb << n, AssertionException&);
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<> overflow(specKind);
@@ -527,7 +527,7 @@ private:
     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);
+    TS_ASSERT_THROWS(d_nm->mkNode(XOR, y, x, x), AssertionException&);
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<> b(specKind);
@@ -588,7 +588,7 @@ private:
     TS_ASSERT_EQUALS(nexplicit.getNumChildren(), K);
 
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(Node blah = implicit, AssertionException);
+    TS_ASSERT_THROWS(Node blah = implicit, AssertionException&);
 #endif /* CVC4_ASSERTIONS */
   }
 
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index 5da55916b..d04e69446 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -300,7 +300,7 @@ class NodeManagerBlack : public CxxTest::TestSuite {
   void testMkNodeTooFew() {
 #ifdef CVC4_ASSERTIONS
     Node x = d_nodeManager->mkSkolem( "x", d_nodeManager->booleanType() );
-    TS_ASSERT_THROWS( d_nodeManager->mkNode(AND, x), AssertionException );
+    TS_ASSERT_THROWS(d_nodeManager->mkNode(AND, x), AssertionException&);
 #endif
   }
 
@@ -319,7 +319,7 @@ class NodeManagerBlack : public CxxTest::TestSuite {
       vars.push_back(skolem_j);
       vars.push_back(orNode);
     }
-    TS_ASSERT_THROWS(d_nodeManager->mkNode(AND, vars), AssertionException);
+    TS_ASSERT_THROWS(d_nodeManager->mkNode(AND, vars), AssertionException&);
 #endif
   }
 };
diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h
index 016ea7793..a0716671f 100644
--- a/test/unit/expr/node_manager_white.h
+++ b/test/unit/expr/node_manager_white.h
@@ -57,7 +57,7 @@ class NodeManagerWhite : public CxxTest::TestSuite {
     TS_ASSERT_THROWS_NOTHING(nb.realloc(25));
     TS_ASSERT_THROWS_NOTHING(nb.realloc(256));
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(nb.realloc(100), AssertionException);
+    TS_ASSERT_THROWS(nb.realloc(100), AssertionException&);
 #endif /* CVC4_ASSERTIONS */
     TS_ASSERT_THROWS_NOTHING(nb.realloc(257));
     TS_ASSERT_THROWS_NOTHING(nb.realloc(4000));
@@ -67,7 +67,7 @@ class NodeManagerWhite : public CxxTest::TestSuite {
     TS_ASSERT_THROWS_NOTHING(nb.realloc(65536));
     TS_ASSERT_THROWS_NOTHING(nb.realloc(67108863));
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(nb.realloc(67108863), AssertionException);
+    TS_ASSERT_THROWS(nb.realloc(67108863), AssertionException&);
 #endif /* CVC4_ASSERTIONS */
   }
 };
diff --git a/test/unit/expr/symbol_table_black.h b/test/unit/expr/symbol_table_black.h
index 2f6f88c27..99799544f 100644
--- a/test/unit/expr/symbol_table_black.h
+++ b/test/unit/expr/symbol_table_black.h
@@ -44,7 +44,7 @@ private:
     {
       d_exprManager = new ExprManager;
     }
-    catch (Exception e)
+    catch (Exception& e)
     {
       cerr << "Exception during setUp():" << endl << e;
       throw;
@@ -55,7 +55,9 @@ private:
   {
     try {
       delete d_exprManager;
-    } catch(Exception e) {
+    }
+    catch (Exception& e)
+    {
       cerr << "Exception during tearDown():" << endl << e;
       throw;
     }
@@ -160,6 +162,6 @@ private:
   void testBadPop() {
     SymbolTable symtab;
     // TODO: What kind of exception gets thrown here?
-    TS_ASSERT_THROWS( symtab.popScope(), ScopeException );
+    TS_ASSERT_THROWS(symtab.popScope(), ScopeException&);
   }
 };/* class SymbolTableBlack */
diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index f5ef8e15e..427bcc34d 100644
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -457,27 +457,41 @@ public:
     LogicInfo info;
     TS_ASSERT( !info.isLocked() );
 
-    TS_ASSERT_THROWS( info.getLogicString(), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BUILTIN ), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BOOL ), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_UF ), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARITH ), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARRAYS ), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BV ), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_DATATYPES ), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_QUANTIFIERS ), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( ! info.isPure( THEORY_BUILTIN ), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( ! info.isPure( THEORY_BOOL ), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( ! info.isPure( THEORY_UF ), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( ! info.isPure( THEORY_ARITH ), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( ! info.isPure( THEORY_ARRAYS ), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( ! info.isPure( THEORY_BV ), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( ! info.isPure( THEORY_DATATYPES ), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( ! info.isPure( THEORY_QUANTIFIERS ), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( info.isQuantified(), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( info.areIntegersUsed(), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( info.areRealsUsed(), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( !info.isLinear(), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS(info.getLogicString(), CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(info.isTheoryEnabled(THEORY_BUILTIN),
+                     CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(info.isTheoryEnabled(THEORY_BOOL),
+                     CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(info.isTheoryEnabled(THEORY_UF),
+                     CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(info.isTheoryEnabled(THEORY_ARITH),
+                     CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(info.isTheoryEnabled(THEORY_ARRAYS),
+                     CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(info.isTheoryEnabled(THEORY_BV),
+                     CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(info.isTheoryEnabled(THEORY_DATATYPES),
+                     CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(info.isTheoryEnabled(THEORY_QUANTIFIERS),
+                     CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(!info.isPure(THEORY_BUILTIN),
+                     CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(!info.isPure(THEORY_BOOL),
+                     CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(!info.isPure(THEORY_UF), CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(!info.isPure(THEORY_ARITH),
+                     CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(!info.isPure(THEORY_ARRAYS),
+                     CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(!info.isPure(THEORY_BV), CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(!info.isPure(THEORY_DATATYPES),
+                     CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(!info.isPure(THEORY_QUANTIFIERS),
+                     CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(info.isQuantified(), CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(info.areIntegersUsed(), CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(info.areRealsUsed(), CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(!info.isLinear(), CVC4::IllegalArgumentException&);
 
     info.lock();
     TS_ASSERT( info.isLocked() );
@@ -505,15 +519,20 @@ public:
     TS_ASSERT(info.areTranscendentalsUsed());
     TS_ASSERT( !info.isLinear() );
 
-    TS_ASSERT_THROWS( info.arithOnlyLinear(), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( info.disableIntegers(), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( info.disableQuantifiers(), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( info.disableTheory(THEORY_BV), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( info.disableTheory(THEORY_DATATYPES), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( info.enableIntegers(), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( info.disableReals(), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( info.disableTheory(THEORY_ARITH), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( info.disableTheory(THEORY_UF), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS(info.arithOnlyLinear(), CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(info.disableIntegers(), CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(info.disableQuantifiers(),
+                     CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(info.disableTheory(THEORY_BV),
+                     CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(info.disableTheory(THEORY_DATATYPES),
+                     CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(info.enableIntegers(), CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(info.disableReals(), CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(info.disableTheory(THEORY_ARITH),
+                     CVC4::IllegalArgumentException&);
+    TS_ASSERT_THROWS(info.disableTheory(THEORY_UF),
+                     CVC4::IllegalArgumentException&);
 
     info = info.getUnlockedCopy();
     TS_ASSERT( !info.isLocked() );
@@ -565,11 +584,11 @@ public:
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
-    TS_ASSERT_THROWS( info.isLinear(), IllegalArgumentException );
-    TS_ASSERT_THROWS( info.areIntegersUsed(), IllegalArgumentException );
-    TS_ASSERT_THROWS( info.isDifferenceLogic(), IllegalArgumentException );
-    TS_ASSERT_THROWS( info.areRealsUsed(), IllegalArgumentException );
-    TS_ASSERT_THROWS(info.areTranscendentalsUsed(), IllegalArgumentException);
+    TS_ASSERT_THROWS(info.isLinear(), IllegalArgumentException&);
+    TS_ASSERT_THROWS(info.areIntegersUsed(), IllegalArgumentException&);
+    TS_ASSERT_THROWS(info.isDifferenceLogic(), IllegalArgumentException&);
+    TS_ASSERT_THROWS(info.areRealsUsed(), IllegalArgumentException&);
+    TS_ASSERT_THROWS(info.areTranscendentalsUsed(), IllegalArgumentException&);
 
     // check copy is unchanged
     info = info.getUnlockedCopy();
@@ -585,11 +604,11 @@ public:
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
-    TS_ASSERT_THROWS( info.isLinear(), IllegalArgumentException );
-    TS_ASSERT_THROWS( info.areIntegersUsed(), IllegalArgumentException );
-    TS_ASSERT_THROWS( info.isDifferenceLogic(), IllegalArgumentException );
-    TS_ASSERT_THROWS( info.areRealsUsed(), IllegalArgumentException );
-    TS_ASSERT_THROWS(info.areTranscendentalsUsed(), IllegalArgumentException);
+    TS_ASSERT_THROWS(info.isLinear(), IllegalArgumentException&);
+    TS_ASSERT_THROWS(info.areIntegersUsed(), IllegalArgumentException&);
+    TS_ASSERT_THROWS(info.isDifferenceLogic(), IllegalArgumentException&);
+    TS_ASSERT_THROWS(info.areRealsUsed(), IllegalArgumentException&);
+    TS_ASSERT_THROWS(info.areTranscendentalsUsed(), IllegalArgumentException&);
 
     // check all-included logic
     info = info.getUnlockedCopy();
diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h
index b68941843..b0f69d32e 100644
--- a/test/unit/theory/type_enumerator_white.h
+++ b/test/unit/theory/type_enumerator_white.h
@@ -59,11 +59,11 @@ class TypeEnumeratorWhite : public CxxTest::TestSuite {
     TS_ASSERT( ! te.isFinished() );
     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(true));
     TS_ASSERT( ! te.isFinished() );
-    TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+    TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
     TS_ASSERT( te.isFinished() );
-    TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+    TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
     TS_ASSERT( te.isFinished() );
-    TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+    TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
     TS_ASSERT( te.isFinished() );
   }
 
@@ -161,9 +161,9 @@ class TypeEnumeratorWhite : public CxxTest::TestSuite {
     TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("green")));
     TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("blue")));
     TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("violet")));
-    TS_ASSERT_THROWS(*++te, NoMoreValuesException);
-    TS_ASSERT_THROWS(*++te, NoMoreValuesException);
-    TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+    TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
+    TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
+    TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
   }
 
   void testDatatypesInfinite1() {
@@ -267,9 +267,9 @@ class TypeEnumeratorWhite : public CxxTest::TestSuite {
     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 5u)));
     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 6u)));
     TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 7u)));
-    TS_ASSERT_THROWS(*++te, NoMoreValuesException);
-    TS_ASSERT_THROWS(*++te, NoMoreValuesException);
-    TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+    TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
+    TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
+    TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
   }
 
 };/* class TypeEnumeratorWhite */
diff --git a/test/unit/util/array_store_all_black.h b/test/unit/util/array_store_all_black.h
index c668e8c8f..21274389b 100644
--- a/test/unit/util/array_store_all_black.h
+++ b/test/unit/util/array_store_all_black.h
@@ -67,7 +67,7 @@ class ArrayStoreAllBlack : public CxxTest::TestSuite {
     TS_ASSERT_THROWS(
         ArrayStoreAll(d_em->mkArrayType(d_em->integerType(), d_em->mkSort("U")),
                       d_em->mkConst(Rational(9, 2))),
-        IllegalArgumentException);
+        IllegalArgumentException&);
   }
 
   void testConstError() {
diff --git a/test/unit/util/assert_white.h b/test/unit/util/assert_white.h
index 41d97b65b..e45d15296 100644
--- a/test/unit/util/assert_white.h
+++ b/test/unit/util/assert_white.h
@@ -29,22 +29,22 @@ public:
 
   void testAssert() {
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS( Assert(false), AssertionException );
-    TS_ASSERT_THROWS( AssertArgument(false, "x"), AssertArgumentException );
+    TS_ASSERT_THROWS(Assert(false), AssertionException&);
+    TS_ASSERT_THROWS(AssertArgument(false, "x"), AssertArgumentException&);
 #else /* CVC4_ASSERTIONS */
     TS_ASSERT_THROWS_NOTHING( Assert(false) );
     TS_ASSERT_THROWS_NOTHING( AssertArgument(false, "x") );
 #endif /* CVC4_ASSERTIONS */
 
     TS_ASSERT_THROWS_NOTHING( Assert(true) );
-    TS_ASSERT_THROWS( AlwaysAssert(false), AssertionException );
-    TS_ASSERT_THROWS( Unreachable(), UnreachableCodeException );
-    TS_ASSERT_THROWS( Unhandled(), UnhandledCaseException );
-    TS_ASSERT_THROWS( Unimplemented(), UnimplementedOperationException );
-    TS_ASSERT_THROWS( IllegalArgument("x"), IllegalArgumentException );
-    TS_ASSERT_THROWS( CheckArgument(false, "x"), IllegalArgumentException );
-    TS_ASSERT_THROWS( AlwaysAssertArgument(false, "x"),
-                      AssertArgumentException );
+    TS_ASSERT_THROWS(AlwaysAssert(false), AssertionException&);
+    TS_ASSERT_THROWS(Unreachable(), UnreachableCodeException&);
+    TS_ASSERT_THROWS(Unhandled(), UnhandledCaseException&);
+    TS_ASSERT_THROWS(Unimplemented(), UnimplementedOperationException&);
+    TS_ASSERT_THROWS(IllegalArgument("x"), IllegalArgumentException&);
+    TS_ASSERT_THROWS(CheckArgument(false, "x"), IllegalArgumentException&);
+    TS_ASSERT_THROWS(AlwaysAssertArgument(false, "x"),
+                     AssertArgumentException&);
     TS_ASSERT_THROWS_NOTHING( AssertArgument(true, "x") );
     TS_ASSERT_THROWS_NOTHING( AssertArgument(true, "x") );
   }
@@ -99,15 +99,16 @@ public:
   }
 
   void testUnreachable() {
-    TS_ASSERT_THROWS( Unreachable(), UnreachableCodeException );
-    TS_ASSERT_THROWS( Unreachable("hello"), UnreachableCodeException );
-    TS_ASSERT_THROWS( Unreachable("hello %s", "world"), UnreachableCodeException );
+    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 );
+    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/bitvector_black.h b/test/unit/util/bitvector_black.h
index c75368196..1446008e6 100644
--- a/test/unit/util/bitvector_black.h
+++ b/test/unit/util/bitvector_black.h
@@ -93,8 +93,8 @@ public:
     BitVector b = one.concat(zero);
     TS_ASSERT_EQUALS(b.toString(), "00010000");
     TS_ASSERT_EQUALS(b.extract(7, 4), one);
-    TS_ASSERT_THROWS(b.extract(4, 7), IllegalArgumentException);
-    TS_ASSERT_THROWS(b.extract(8, 3), IllegalArgumentException);
+    TS_ASSERT_THROWS(b.extract(4, 7), IllegalArgumentException&);
+    TS_ASSERT_THROWS(b.extract(8, 3), IllegalArgumentException&);
     TS_ASSERT_EQUALS(b.concat(BitVector()), b);
   }
 
@@ -116,10 +116,10 @@ public:
     TS_ASSERT(negOne.signedLessThanEq(negOne));
 
     BitVector b = negOne.concat(negOne);
-    TS_ASSERT_THROWS(b.unsignedLessThan(negOne), IllegalArgumentException);
-    TS_ASSERT_THROWS(negOne.unsignedLessThanEq(b), IllegalArgumentException);
-    TS_ASSERT_THROWS(b.signedLessThan(negOne), IllegalArgumentException);
-    TS_ASSERT_THROWS(negOne.signedLessThanEq(b), IllegalArgumentException);
+    TS_ASSERT_THROWS(b.unsignedLessThan(negOne), IllegalArgumentException&);
+    TS_ASSERT_THROWS(negOne.unsignedLessThanEq(b), IllegalArgumentException&);
+    TS_ASSERT_THROWS(b.signedLessThan(negOne), IllegalArgumentException&);
+    TS_ASSERT_THROWS(negOne.signedLessThanEq(b), IllegalArgumentException&);
   }
 
   void testBitwiseOps()
@@ -145,10 +145,10 @@ public:
     TS_ASSERT_EQUALS(negOne.unsignedRemTotal(two), one);
 
     BitVector b = negOne.concat(negOne);
-    TS_ASSERT_THROWS(b + negOne, IllegalArgumentException);
-    TS_ASSERT_THROWS(negOne * b, IllegalArgumentException);
-    TS_ASSERT_THROWS(b.unsignedDivTotal(negOne), IllegalArgumentException);
-    TS_ASSERT_THROWS(negOne.unsignedRemTotal(b), IllegalArgumentException);
+    TS_ASSERT_THROWS(b + negOne, IllegalArgumentException&);
+    TS_ASSERT_THROWS(negOne * b, IllegalArgumentException&);
+    TS_ASSERT_THROWS(b.unsignedDivTotal(negOne), IllegalArgumentException&);
+    TS_ASSERT_THROWS(negOne.unsignedRemTotal(b), IllegalArgumentException&);
   }
 
   void testExtendOps()
diff --git a/test/unit/util/boolean_simplification_black.h b/test/unit/util/boolean_simplification_black.h
index 2654c1c07..445103407 100644
--- a/test/unit/util/boolean_simplification_black.h
+++ b/test/unit/util/boolean_simplification_black.h
@@ -130,7 +130,8 @@ public:
 
 #ifdef CVC4_ASSERTIONS
     in = Node();
-    TS_ASSERT_THROWS( BooleanSimplification::negate(in), AssertArgumentException );
+    TS_ASSERT_THROWS(BooleanSimplification::negate(in),
+                     AssertArgumentException&);
 #endif /* CVC4_ASSERTIONS */
   }
 
@@ -165,7 +166,8 @@ public:
 
 #ifdef CVC4_ASSERTIONS
     in = d_nm->mkNode(kind::AND, a, b);
-    TS_ASSERT_THROWS( BooleanSimplification::simplifyClause(in), AssertArgumentException );
+    TS_ASSERT_THROWS(BooleanSimplification::simplifyClause(in),
+                     AssertArgumentException&);
 #endif /* CVC4_ASSERTIONS */
   }
 
@@ -190,7 +192,8 @@ public:
 
 #ifdef CVC4_ASSERTIONS
     in = d_nm->mkNode(kind::OR, a, b);
-    TS_ASSERT_THROWS( BooleanSimplification::simplifyHornClause(in), AssertArgumentException );
+    TS_ASSERT_THROWS(BooleanSimplification::simplifyHornClause(in),
+                     AssertArgumentException&);
 #endif /* CVC4_ASSERTIONS */
   }
 
@@ -211,7 +214,8 @@ public:
 
 #ifdef CVC4_ASSERTIONS
     in = d_nm->mkNode(kind::OR, a, b);
-    TS_ASSERT_THROWS( BooleanSimplification::simplifyConflict(in), AssertArgumentException );
+    TS_ASSERT_THROWS(BooleanSimplification::simplifyConflict(in),
+                     AssertArgumentException&);
 #endif /* CVC4_ASSERTIONS */
   }
 
diff --git a/test/unit/util/cardinality_public.h b/test/unit/util/cardinality_public.h
index 449a88946..ee4a23fd3 100644
--- a/test/unit/util/cardinality_public.h
+++ b/test/unit/util/cardinality_public.h
@@ -34,9 +34,11 @@ public:
     Cardinality two(2);
 
     Cardinality invalid(0);
-    TS_ASSERT_THROWS( invalid = Cardinality(-1), IllegalArgumentException);
-    TS_ASSERT_THROWS( invalid = Cardinality(-2), IllegalArgumentException);
-    TS_ASSERT_THROWS( invalid = Cardinality(Integer("-3983982192391747295721957")), IllegalArgumentException);
+    TS_ASSERT_THROWS(invalid = Cardinality(-1), IllegalArgumentException&);
+    TS_ASSERT_THROWS(invalid = Cardinality(-2), IllegalArgumentException&);
+    TS_ASSERT_THROWS(
+        invalid = Cardinality(Integer("-3983982192391747295721957")),
+        IllegalArgumentException&);
     invalid = one; // test assignment
     invalid = Cardinality(5); // test assignment to temporary
 
@@ -121,16 +123,16 @@ public:
     TS_ASSERT( two.getFiniteCardinality() == 2 );
     TS_ASSERT( copy.getFiniteCardinality() == 1 );
     TS_ASSERT( invalid.getFiniteCardinality() == 5 );
-    TS_ASSERT_THROWS( big.getFiniteCardinality(), IllegalArgumentException );
-    TS_ASSERT_THROWS( i.getFiniteCardinality(), IllegalArgumentException );
-    TS_ASSERT_THROWS( r.getFiniteCardinality(), IllegalArgumentException );
-
-    TS_ASSERT_THROWS( zero.getBethNumber(), IllegalArgumentException );
-    TS_ASSERT_THROWS( one.getBethNumber(), IllegalArgumentException );
-    TS_ASSERT_THROWS( two.getBethNumber(), IllegalArgumentException );
-    TS_ASSERT_THROWS( copy.getBethNumber(), IllegalArgumentException );
-    TS_ASSERT_THROWS( invalid.getBethNumber(), IllegalArgumentException );
-    TS_ASSERT_THROWS( big.getBethNumber(), IllegalArgumentException );
+    TS_ASSERT_THROWS(big.getFiniteCardinality(), IllegalArgumentException&);
+    TS_ASSERT_THROWS(i.getFiniteCardinality(), IllegalArgumentException&);
+    TS_ASSERT_THROWS(r.getFiniteCardinality(), IllegalArgumentException&);
+
+    TS_ASSERT_THROWS(zero.getBethNumber(), IllegalArgumentException&);
+    TS_ASSERT_THROWS(one.getBethNumber(), IllegalArgumentException&);
+    TS_ASSERT_THROWS(two.getBethNumber(), IllegalArgumentException&);
+    TS_ASSERT_THROWS(copy.getBethNumber(), IllegalArgumentException&);
+    TS_ASSERT_THROWS(invalid.getBethNumber(), IllegalArgumentException&);
+    TS_ASSERT_THROWS(big.getBethNumber(), IllegalArgumentException&);
     TS_ASSERT( i.getBethNumber() == 0 );
     TS_ASSERT( r.getBethNumber() == 1 );
 
@@ -211,7 +213,7 @@ public:
     TS_ASSERT( x.compare(y) == Cardinality::LESS );
     TS_ASSERT( y.compare(z) == Cardinality::LESS );
 
-    TS_ASSERT_THROWS( big.getBethNumber(), IllegalArgumentException );
+    TS_ASSERT_THROWS(big.getBethNumber(), IllegalArgumentException&);
     TS_ASSERT( x.getBethNumber() == 0 );
     TS_ASSERT( y.getBethNumber() == 1 );
     TS_ASSERT( z.getBethNumber() == 2 );
diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h
index c2086c415..160f25e6f 100644
--- a/test/unit/util/datatype_black.h
+++ b/test/unit/util/datatype_black.h
@@ -70,8 +70,9 @@ class DatatypeBlack : public CxxTest::TestSuite {
     const Datatype& colorsDT = colorsType.getDatatype();
     TS_ASSERT(colorsDT.getConstructor("blue") == ctor);
     TS_ASSERT(colorsDT["blue"].getConstructor() == ctor);
-    TS_ASSERT_THROWS(colorsDT["blue"].getSelector("foo"), IllegalArgumentException);
-    TS_ASSERT_THROWS(colorsDT["blue"]["foo"], IllegalArgumentException);
+    TS_ASSERT_THROWS(colorsDT["blue"].getSelector("foo"),
+                     IllegalArgumentException&);
+    TS_ASSERT_THROWS(colorsDT["blue"]["foo"], IllegalArgumentException&);
 
     TS_ASSERT(! colorsType.getDatatype().isParametric());
     TS_ASSERT(colorsType.getDatatype().isFinite());
@@ -130,7 +131,8 @@ class DatatypeBlack : public CxxTest::TestSuite {
     Expr ctor = treeType.getDatatype()[1].getConstructor();
     TS_ASSERT(treeType.getConstructor("leaf") == ctor);
     TS_ASSERT(treeType.getConstructor("leaf") == ctor);
-    TS_ASSERT_THROWS(treeType.getConstructor("leff"), IllegalArgumentException);
+    TS_ASSERT_THROWS(treeType.getConstructor("leff"),
+                     IllegalArgumentException&);
 
     TS_ASSERT(! treeType.getDatatype().isParametric());
     TS_ASSERT(! treeType.getDatatype().isFinite());
diff --git a/test/unit/util/integer_black.h b/test/unit/util/integer_black.h
index 6c183c972..9297429b4 100644
--- a/test/unit/util/integer_black.h
+++ b/test/unit/util/integer_black.h
@@ -293,14 +293,14 @@ public:
   }
 
   void testParseErrors() {
-    TS_ASSERT_THROWS(Integer("abracadabra"), std::invalid_argument);
-    TS_ASSERT_THROWS(Integer("+-1"), std::invalid_argument);
-    TS_ASSERT_THROWS(Integer("-+1"), std::invalid_argument);
-    TS_ASSERT_THROWS(Integer("5i"), std::invalid_argument);
-    TS_ASSERT_THROWS(Integer("10xyz"), std::invalid_argument);
-    TS_ASSERT_THROWS(Integer("0xff", 10), std::invalid_argument);
-    TS_ASSERT_THROWS(Integer("#x5", 0), std::invalid_argument);
-    TS_ASSERT_THROWS(Integer("0b123", 0), std::invalid_argument);
+    TS_ASSERT_THROWS(Integer("abracadabra"), std::invalid_argument&);
+    TS_ASSERT_THROWS(Integer("+-1"), std::invalid_argument&);
+    TS_ASSERT_THROWS(Integer("-+1"), std::invalid_argument&);
+    TS_ASSERT_THROWS(Integer("5i"), std::invalid_argument&);
+    TS_ASSERT_THROWS(Integer("10xyz"), std::invalid_argument&);
+    TS_ASSERT_THROWS(Integer("0xff", 10), std::invalid_argument&);
+    TS_ASSERT_THROWS(Integer("#x5", 0), std::invalid_argument&);
+    TS_ASSERT_THROWS(Integer("0b123", 0), std::invalid_argument&);
   }
 
   void testPow() {