Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)

24 files changed, 162 insertions, 217 deletions

diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h
index 6c5ecdf08..96c575218 100644
--- a/test/unit/context/cdmap_black.h
+++ b/test/unit/context/cdmap_black.h
@@ -18,12 +18,12 @@
 
 #include <map>
 
-#include "base/cvc4_assert.h"
-#include "context/context.h"
+#include "base/check.h"
 #include "context/cdhashmap.h"
 #include "context/cdlist.h"
+#include "context/context.h"
+#include "test_utils.h"
 
-using CVC4::AssertionException;
 using CVC4::context::Context;
 using CVC4::context::CDHashMap;
 
@@ -163,10 +163,8 @@ class CDMapBlack : public CxxTest::TestSuite {
         TS_ASSERT(
             ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 317}}));
 
-        TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 317),
-                         AssertionException&);
-        TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 472),
-                         AssertionException&);
+        TS_UTILS_EXPECT_ABORT(map.insertAtContextLevelZero(23, 317));
+        TS_UTILS_EXPECT_ABORT(map.insertAtContextLevelZero(23, 472));
         map.insert(23, 472);
 
         TS_ASSERT(
@@ -177,8 +175,7 @@ class CDMapBlack : public CxxTest::TestSuite {
           TS_ASSERT(
             ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}}));
 
-          TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0),
-                           AssertionException&);
+          TS_UTILS_EXPECT_ABORT(map.insertAtContextLevelZero(23, 0));
           map.insert(23, 1024);
 
           TS_ASSERT(
@@ -194,8 +191,7 @@ 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_UTILS_EXPECT_ABORT(map.insertAtContextLevelZero(23, 0));
       map.insert(23, 477);
 
       TS_ASSERT(
@@ -203,7 +199,7 @@ class CDMapBlack : public CxxTest::TestSuite {
       d_context->pop();
     }
 
-    TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0), AssertionException&);
+    TS_UTILS_EXPECT_ABORT(map.insertAtContextLevelZero(23, 0));
 
     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 1a1f683bc..d22ecc7f1 100644
--- a/test/unit/context/cdmap_white.h
+++ b/test/unit/context/cdmap_white.h
@@ -16,8 +16,9 @@
 
 #include <cxxtest/TestSuite.h>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "context/cdhashmap.h"
+#include "test_utils.h"
 
 using namespace std;
 using namespace CVC4;
@@ -38,12 +39,12 @@ class CDMapWhite : public CxxTest::TestSuite {
 
     TS_ASSERT_THROWS_NOTHING(map.makeCurrent());
 
-    TS_ASSERT_THROWS(map.update(), UnreachableCodeException&);
+    TS_UTILS_EXPECT_ABORT(map.update());
 
-    TS_ASSERT_THROWS(map.save(d_context->getCMM()), UnreachableCodeException&);
-    TS_ASSERT_THROWS(map.restore(&map), UnreachableCodeException&);
+    TS_UTILS_EXPECT_ABORT(map.save(d_context->getCMM()));
+    TS_UTILS_EXPECT_ABORT(map.restore(&map));
 
     d_context->push();
-    TS_ASSERT_THROWS(map.makeCurrent(), UnreachableCodeException&);
+    TS_UTILS_EXPECT_ABORT(map.makeCurrent());
   }
 };
diff --git a/test/unit/context/cdo_black.h b/test/unit/context/cdo_black.h
index 4f927abfc..4e1efb7b1 100644
--- a/test/unit/context/cdo_black.h
+++ b/test/unit/context/cdo_black.h
@@ -19,7 +19,7 @@
 #include <iostream>
 #include <vector>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "context/cdlist.h"
 #include "context/cdo.h"
 #include "context/context.h"
diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h
index 3659d3494..258c3fd9b 100644
--- a/test/unit/context/context_black.h
+++ b/test/unit/context/context_black.h
@@ -19,11 +19,11 @@
 #include <iostream>
 #include <vector>
 
-#include "base/cvc4_assert.h"
+#include "base/exception.h"
 #include "context/cdlist.h"
 #include "context/cdo.h"
 #include "context/context.h"
-
+#include "test_utils.h"
 
 using namespace std;
 using namespace CVC4;
@@ -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_UTILS_EXPECT_ABORT(d_context->pop());
+    TS_UTILS_EXPECT_ABORT(d_context->pop());
 #endif /* CVC4_ASSERTIONS */
   }
 
diff --git a/test/unit/context/context_mm_black.h b/test/unit/context/context_mm_black.h
index 15f9b09de..cd5ff8242 100644
--- a/test/unit/context/context_mm_black.h
+++ b/test/unit/context/context_mm_black.h
@@ -22,8 +22,7 @@
 #include <iostream>
 
 #include "context/context_mm.h"
-
-#include "base/cvc4_assert.h"
+#include "test_utils.h"
 
 using namespace std;
 using namespace CVC4::context;
@@ -90,7 +89,7 @@ private:
     }
 
     // Try popping out of scope
-    TS_ASSERT_THROWS(d_cmm->pop(), CVC4::AssertionException&);
+    TS_UTILS_EXPECT_ABORT(d_cmm->pop());
 #endif /* __CVC4__CONTEXT__CONTEXT_MM_H */
   }
 
diff --git a/test/unit/context/context_white.h b/test/unit/context/context_white.h
index 515ffb848..87ff73cce 100644
--- a/test/unit/context/context_white.h
+++ b/test/unit/context/context_white.h
@@ -16,9 +16,9 @@
 
 #include <cxxtest/TestSuite.h>
 
-#include "base/cvc4_assert.h"
-#include "context/context.h"
+#include "base/check.h"
 #include "context/cdo.h"
+#include "context/context.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index d109efdfd..745264b83 100644
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -18,7 +18,7 @@
 
 #include <string>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "expr/attribute.h"
 #include "expr/node.h"
 #include "expr/node_builder.h"
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 287704f39..e4a0dbb36 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -27,6 +27,7 @@
 #include "expr/node_builder.h"
 #include "expr/node_manager.h"
 #include "expr/node_value.h"
+#include "test_utils.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -179,8 +180,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_UTILS_EXPECT_ABORT(Node::null()[-1]);
+    TS_UTILS_EXPECT_ABORT(Node::null()[0]);
 #endif /* CVC4_ASSERTIONS */
 
     // Basic access check
@@ -198,8 +199,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_UTILS_EXPECT_ABORT(ite == ite[-1]);
+    TS_UTILS_EXPECT_ABORT(ite == ite[4]);
 #endif /* CVC4_ASSERTIONS */
   }
 
@@ -459,10 +460,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_UTILS_EXPECT_ABORT(testNaryExpForSize(AND, 0));
+    TS_UTILS_EXPECT_ABORT(testNaryExpForSize(AND, 1));
+    TS_UTILS_EXPECT_ABORT(testNaryExpForSize(NOT, 0));
+    TS_UTILS_EXPECT_ABORT(testNaryExpForSize(NOT, 2));
 #endif /* CVC4_ASSERTIONS */
   }
 
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index 2ece96cb8..473557e07 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -20,11 +20,12 @@
 #include <limits.h>
 #include <sstream>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "expr/kind.h"
 #include "expr/node.h"
 #include "expr/node_builder.h"
 #include "expr/node_manager.h"
+#include "test_utils.h"
 #include "util/rational.h"
 
 using namespace CVC4;
@@ -90,9 +91,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_UTILS_EXPECT_ABORT(def.getNumChildren());
+    TS_UTILS_EXPECT_ABORT(def.begin());
+    TS_UTILS_EXPECT_ABORT(def.end());
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<> spec(specKind);
@@ -104,9 +105,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_UTILS_EXPECT_ABORT(from_nm.getNumChildren());
+    TS_UTILS_EXPECT_ABORT(from_nm.begin());
+    TS_UTILS_EXPECT_ABORT(from_nm.end());
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<> from_nm_kind(d_nm, specKind);
@@ -120,9 +121,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_UTILS_EXPECT_ABORT(ws.getNumChildren());
+    TS_UTILS_EXPECT_ABORT(ws.begin());
+    TS_UTILS_EXPECT_ABORT(ws.end());
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<K> ws_kind(specKind);
@@ -134,9 +135,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_UTILS_EXPECT_ABORT(ws_from_nm.getNumChildren());
+    TS_UTILS_EXPECT_ABORT(ws_from_nm.begin());
+    TS_UTILS_EXPECT_ABORT(ws_from_nm.end());
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<K> ws_from_nm_kind(d_nm, specKind);
@@ -158,33 +159,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_UTILS_EXPECT_ABORT(copy.getNumChildren());
+    TS_UTILS_EXPECT_ABORT(copy.begin());
+    TS_UTILS_EXPECT_ABORT(copy.end());
 #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_UTILS_EXPECT_ABORT(cp_ws.getNumChildren());
+    TS_UTILS_EXPECT_ABORT(cp_ws.begin());
+    TS_UTILS_EXPECT_ABORT(cp_ws.end());
 #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_UTILS_EXPECT_ABORT(cp_from_larger.getNumChildren());
+    TS_UTILS_EXPECT_ABORT(cp_from_larger.begin());
+    TS_UTILS_EXPECT_ABORT(cp_from_larger.end());
 #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_UTILS_EXPECT_ABORT(cp_from_smaller.getNumChildren());
+    TS_UTILS_EXPECT_ABORT(cp_from_smaller.begin());
+    TS_UTILS_EXPECT_ABORT(cp_from_smaller.end());
 #endif /* CVC4_ASSERTIONS */
   }
 
@@ -282,7 +283,7 @@ private:
     Node n = noKind;
 
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(noKind.getKind(), AssertionException&);
+    TS_UTILS_EXPECT_ABORT(noKind.getKind());
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<> spec(PLUS);
@@ -297,7 +298,7 @@ private:
 
     NodeBuilder<> nb;
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException&);
+    TS_UTILS_EXPECT_ABORT(nb.getNumChildren());
 #endif /* CVC4_ASSERTIONS */
     nb << PLUS << x << x;
 
@@ -309,7 +310,7 @@ private:
     Node n = nb;// avoid warning on clear()
     nb.clear();
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException&);
+    TS_UTILS_EXPECT_ABORT(nb.getNumChildren());
 #endif /* CVC4_ASSERTIONS */
     nb.clear(PLUS);
     TS_ASSERT_EQUALS(nb.getNumChildren(), 0u);
@@ -321,16 +322,16 @@ private:
     TS_ASSERT_EQUALS(nb.getNumChildren(), 6u);
 
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(nb << PLUS, AssertionException&);
+    TS_UTILS_EXPECT_ABORT(nb << PLUS);
     n = nb;
-    TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException&);
+    TS_UTILS_EXPECT_ABORT(nb.getNumChildren());
 #endif /* CVC4_ASSERTIONS */
   }
 
   void testOperatorSquare() {
     /*
       Node operator[](int i) const {
-      Assert(i >= 0 && i < d_ev->getNumChildren());
+      TS_ASSERT(i >= 0 && i < d_ev->getNumChildren());
       return Node(d_ev->d_children[i]);
       }
     */
@@ -341,8 +342,8 @@ private:
     Node i_K = d_nm->mkNode(NOT, i_0);
 
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(arr[-1], AssertionException&);
-    TS_ASSERT_THROWS(arr[0], AssertionException&);
+    TS_UTILS_EXPECT_ABORT(arr[-1]);
+    TS_UTILS_EXPECT_ABORT(arr[0]);
 #endif /* CVC4_ASSERTIONS */
 
     arr << i_0;
@@ -375,7 +376,7 @@ private:
 
 #ifdef CVC4_ASSERTIONS
     Node n = arr;
-    TS_ASSERT_THROWS(arr[0], AssertionException&);
+    TS_UTILS_EXPECT_ABORT(arr[0]);
 #endif /* CVC4_ASSERTIONS */
   }
 
@@ -385,9 +386,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_UTILS_EXPECT_ABORT(nb.getNumChildren());
+    TS_UTILS_EXPECT_ABORT(nb.begin());
+    TS_UTILS_EXPECT_ABORT(nb.end());
 #endif /* CVC4_ASSERTIONS */
 
     nb << specKind;
@@ -402,9 +403,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_UTILS_EXPECT_ABORT(nb.getNumChildren());
+    TS_UTILS_EXPECT_ABORT(nb.begin());
+    TS_UTILS_EXPECT_ABORT(nb.end());
 #endif /* CVC4_ASSERTIONS */
 
     nb << specKind;
@@ -427,9 +428,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_UTILS_EXPECT_ABORT(nb.getNumChildren());
+    TS_UTILS_EXPECT_ABORT(nb.begin());
+    TS_UTILS_EXPECT_ABORT(nb.end());
 #endif /* CVC4_ASSERTIONS */
   }
 
@@ -438,7 +439,7 @@ private:
 
 #ifdef CVC4_ASSERTIONS
     NodeBuilder<> spec(specKind);
-    TS_ASSERT_THROWS(spec << PLUS, AssertionException&);
+    TS_UTILS_EXPECT_ABORT(spec << PLUS);
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<> noSpec;
@@ -457,12 +458,12 @@ private:
     nb.clear(PLUS);
 
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(n = nb, AssertionException&);
+    TS_UTILS_EXPECT_ABORT(n = nb);
     nb.clear(PLUS);
 #endif /* CVC4_ASSERTIONS */
 
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(nb << PLUS, AssertionException&);
+    TS_UTILS_EXPECT_ABORT(nb << PLUS);
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<> testRef;
@@ -470,7 +471,7 @@ private:
 
 #ifdef CVC4_ASSERTIONS
     NodeBuilder<> testTwo;
-    TS_ASSERT_THROWS(testTwo << specKind << PLUS, AssertionException&);
+    TS_UTILS_EXPECT_ABORT(testTwo << specKind << PLUS);
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<> testMixOrder1;
@@ -494,7 +495,7 @@ private:
 
 #ifdef CVC4_ASSERTIONS
     Node n = nb;
-    TS_ASSERT_THROWS(nb << n, AssertionException&);
+    TS_UTILS_EXPECT_ABORT(nb << n);
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<> overflow(specKind);
@@ -527,7 +528,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_UTILS_EXPECT_ABORT(d_nm->mkNode(XOR, y, x, x));
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<> b(specKind);
@@ -588,7 +589,7 @@ private:
     TS_ASSERT_EQUALS(nexplicit.getNumChildren(), K);
 
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(Node blah = implicit, AssertionException&);
+    TS_UTILS_EXPECT_ABORT(Node blah = implicit);
 #endif /* CVC4_ASSERTIONS */
   }
 
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index e568fc9df..4b9c42bd0 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -22,6 +22,7 @@
 #include "base/output.h"
 #include "expr/node_manager.h"
 #include "expr/node_manager_attributes.h"
+#include "test_utils.h"
 #include "util/integer.h"
 #include "util/rational.h"
 
@@ -300,7 +301,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_UTILS_EXPECT_ABORT(d_nodeManager->mkNode(AND, x));
 #endif
   }
 
@@ -319,7 +320,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_UTILS_EXPECT_ABORT(d_nodeManager->mkNode(AND, vars));
 #endif
   }
 };
diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h
index c2888a708..6f7729f74 100644
--- a/test/unit/expr/node_manager_white.h
+++ b/test/unit/expr/node_manager_white.h
@@ -19,6 +19,7 @@
 #include <string>
 
 #include "expr/node_manager.h"
+#include "test_utils.h"
 #include "util/integer.h"
 #include "util/rational.h"
 
@@ -57,7 +58,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_UTILS_EXPECT_ABORT(nb.realloc(100));
 #endif /* CVC4_ASSERTIONS */
     TS_ASSERT_THROWS_NOTHING(nb.realloc(257));
     TS_ASSERT_THROWS_NOTHING(nb.realloc(4000));
@@ -67,7 +68,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_UTILS_EXPECT_ABORT(nb.realloc(67108863));
 #endif /* CVC4_ASSERTIONS */
   }
 
diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h
index e9a3112cf..c95c46e02 100644
--- a/test/unit/expr/node_white.h
+++ b/test/unit/expr/node_white.h
@@ -18,7 +18,7 @@
 
 #include <string>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "expr/node.h"
 #include "expr/node_builder.h"
 #include "expr/node_manager.h"
diff --git a/test/unit/expr/symbol_table_black.h b/test/unit/expr/symbol_table_black.h
index ef65e8773..1ac1fa315 100644
--- a/test/unit/expr/symbol_table_black.h
+++ b/test/unit/expr/symbol_table_black.h
@@ -19,7 +19,7 @@
 #include <sstream>
 #include <string>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "base/exception.h"
 #include "context/context.h"
 #include "expr/expr.h"
diff --git a/test/unit/memory.h b/test/unit/memory.h
index 49b0885b1..9c92ba918 100644
--- a/test/unit/memory.h
+++ b/test/unit/memory.h
@@ -36,8 +36,8 @@
 #include <sys/resource.h>
 #include <sys/time.h>
 
+#include "base/check.h"
 #include "base/configuration_private.h"
-#include "base/cvc4_assert.h"
 
 // Conditionally define CVC4_MEMORY_LIMITING_DISABLED.
 #ifdef __APPLE__
diff --git a/test/unit/preprocessing/pass_bv_gauss_white.h b/test/unit/preprocessing/pass_bv_gauss_white.h
index 7f7af40b9..4037c7191 100644
--- a/test/unit/preprocessing/pass_bv_gauss_white.h
+++ b/test/unit/preprocessing/pass_bv_gauss_white.h
@@ -20,6 +20,7 @@
 #include "preprocessing/passes/bv_gauss.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
+#include "test_utils.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 #include "util/bitvector.h"
@@ -116,14 +117,6 @@ static void testGaussElimX(Integer prime,
   }
 }
 
-template <class T>
-static void testGaussElimT(Integer prime,
-                           std::vector<Integer> rhs,
-                           std::vector<std::vector<Integer>> lhs)
-{
-  TS_ASSERT_THROWS(BVGauss::gaussElim(prime, rhs, lhs), T);
-}
-
 class TheoryBVGaussWhite : public CxxTest::TestSuite
 {
   ExprManager *d_em;
@@ -319,7 +312,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
            {Integer(2), Integer(3), Integer(5)},
            {Integer(4), Integer(0), Integer(5)}};
     std::cout << "matrix 0, modulo 0" << std::endl;  // throws
-    testGaussElimT<AssertionException>(Integer(0), rhs, lhs);
+    TS_UTILS_EXPECT_ABORT(BVGauss::gaussElim(Integer(0), rhs, lhs));
     std::cout << "matrix 0, modulo 1" << std::endl;
     testGaussElimX(Integer(1), rhs, lhs, BVGauss::Result::UNIQUE);
     std::cout << "matrix 0, modulo 2" << std::endl;
diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h
index 7aaf1f4de..70357ea1b 100644
--- a/test/unit/prop/cnf_stream_white.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -18,7 +18,7 @@
 /* #include <gmock/gmock.h> */
 /* #include <gtest/gtest.h> */
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "context/context.h"
 #include "expr/expr_manager.h"
 #include "expr/node_manager.h"
diff --git a/test/unit/test_utils.h b/test/unit/test_utils.h
index 67bc34456..474f2e78b 100644
--- a/test/unit/test_utils.h
+++ b/test/unit/test_utils.h
@@ -18,7 +18,7 @@
 
 /**
  * Use TS_UTILS_EXPECT_ABORT if you expect the expression to abort() when a
- * CVC4_CHECK or CVC4_DCHECK is triggered.
+ * AlwaysAssert or Assert is triggered.
  */
 #define TS_UTILS_EXPECT_ABORT(expr) \
   do                                \
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index d357b200e..88f8ed6dd 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -25,7 +25,7 @@
 #include <memory>
 #include <string>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "context/context.h"
 #include "expr/kind.h"
 #include "expr/node.h"
diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.h b/test/unit/theory/theory_quantifiers_bv_inverter_white.h
index 5be92b19e..03fcaab69 100644
--- a/test/unit/theory/theory_quantifiers_bv_inverter_white.h
+++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.h
@@ -47,9 +47,9 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
                    Node x,
                    Node (*getsc)(bool, Kind, Node, Node))
   {
-    Assert(k == BITVECTOR_ULT || k == BITVECTOR_SLT || k == EQUAL
-           || k == BITVECTOR_UGT || k == BITVECTOR_SGT);
-    Assert(k != EQUAL || pol == false);
+    TS_ASSERT(k == BITVECTOR_ULT || k == BITVECTOR_SLT || k == EQUAL
+              || k == BITVECTOR_UGT || k == BITVECTOR_SGT);
+    TS_ASSERT(k != EQUAL || pol == false);
 
     Node sc = getsc(pol, k, d_sk, d_t);
     Kind ksc = sc.getKind();
@@ -78,7 +78,7 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
       }
       else
       {
-        Assert(k == EQUAL);
+        TS_ASSERT(k == EQUAL);
         k = DISTINCT;
       }
     }
@@ -95,10 +95,10 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
                unsigned idx,
                Node (*getsc)(bool, Kind, Kind, unsigned, Node, Node, Node))
   {
-    Assert(k == BITVECTOR_MULT || k == BITVECTOR_UREM_TOTAL
-           || k == BITVECTOR_UDIV_TOTAL || k == BITVECTOR_AND
-           || k == BITVECTOR_OR || k == BITVECTOR_LSHR || k == BITVECTOR_ASHR
-           || k == BITVECTOR_SHL);
+    TS_ASSERT(k == BITVECTOR_MULT || k == BITVECTOR_UREM_TOTAL
+              || k == BITVECTOR_UDIV_TOTAL || k == BITVECTOR_AND
+              || k == BITVECTOR_OR || k == BITVECTOR_LSHR || k == BITVECTOR_ASHR
+              || k == BITVECTOR_SHL);
 
     Node sc = getsc(pol, litk, k, idx, d_sk, d_s, d_t);
     TS_ASSERT(!sc.isNull());
@@ -148,7 +148,7 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
     }
     else
     {
-      Assert(idx == 2);
+      TS_ASSERT(idx == 2);
       s1 = d_nm->mkVar("s1", d_nm->mkBitVectorType(4));
       s2 = d_nm->mkVar("s2", d_nm->mkBitVectorType(4));
       x = d_nm->mkBoundVar(s2.getType());
diff --git a/test/unit/util/array_store_all_black.h b/test/unit/util/array_store_all_black.h
index 0b8313222..c0d1474e9 100644
--- a/test/unit/util/array_store_all_black.h
+++ b/test/unit/util/array_store_all_black.h
@@ -21,24 +21,22 @@
 #include "expr/expr_manager.h"
 #include "expr/expr_manager_scope.h"
 #include "expr/type.h"
+#include "test_utils.h"
 
 using namespace CVC4;
 using namespace std;
 
 class ArrayStoreAllBlack : public CxxTest::TestSuite {
   ExprManager* d_em;
-  ExprManagerScope* d_scope;
 
  public:
   void setUp() override
   {
     d_em = new ExprManager();
-    d_scope = new ExprManagerScope(*d_em);
   }
 
   void tearDown() override
   {
-    delete d_scope;
     delete d_em;
   }
 
@@ -55,15 +53,15 @@ class ArrayStoreAllBlack : public CxxTest::TestSuite {
         d_em->mkConst(Rational(0)));
   }
 
-  void testTypeErrors() {
-    // these two throw an AssertionException in assertions-enabled builds, and
-    // an IllegalArgumentException in production builds
-    TS_ASSERT_THROWS_ANYTHING(ArrayStoreAll(
-        d_em->integerType(),
-        d_em->mkConst(UninterpretedConstant(d_em->mkSort("U"), 0))));
-    TS_ASSERT_THROWS_ANYTHING(
-        ArrayStoreAll(d_em->integerType(), d_em->mkConst(Rational(9, 2))));
-
+  void testTypeErrors()
+  {
+    TS_ASSERT_THROWS(ArrayStoreAll(d_em->integerType(),
+                                   d_em->mkConst(UninterpretedConstant(
+                                       d_em->mkSort("U"), 0))),
+                     IllegalArgumentException&);
+    TS_ASSERT_THROWS(
+        ArrayStoreAll(d_em->integerType(), d_em->mkConst(Rational(9, 2))),
+        IllegalArgumentException&);
     TS_ASSERT_THROWS(
         ArrayStoreAll(d_em->mkArrayType(d_em->integerType(), d_em->mkSort("U")),
                       d_em->mkConst(Rational(9, 2))),
diff --git a/test/unit/util/assert_white.h b/test/unit/util/assert_white.h
index 47acbcc6d..03afcdbf7 100644
--- a/test/unit/util/assert_white.h
+++ b/test/unit/util/assert_white.h
@@ -19,96 +19,49 @@
 #include <string>
 #include <cstring>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
+#include "test_utils.h"
 
 using namespace CVC4;
 using namespace std;
 
 class AssertWhite : public CxxTest::TestSuite {
 public:
-
-  void testAssert() {
+ void testAssert()
+ {
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(Assert(false), AssertionException&);
-    TS_ASSERT_THROWS(AssertArgument(false, "x"), AssertArgumentException&);
+   TS_UTILS_EXPECT_ABORT(Assert(false));
+   TS_ASSERT_THROWS(AssertArgument(false, "x"), AssertArgumentException&);
 #else /* CVC4_ASSERTIONS */
-    TS_ASSERT_THROWS_NOTHING( Assert(false) );
-    TS_ASSERT_THROWS_NOTHING( AssertArgument(false, "x") );
+   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_NOTHING( AssertArgument(true, "x") );
-    TS_ASSERT_THROWS_NOTHING( AssertArgument(true, "x") );
-  }
-
-  void testReallyLongAssert() {
-    string msg(1034, 'x');
-    try {
-      AlwaysAssert(false, msg.c_str());
-      TS_FAIL("Should have thrown an exception !");
-    } catch(AssertionException& e) {
-      // we don't want to match on the entire string, because it may
-      // have an absolute path to the unit test binary, line number
-      // info, etc.
-      std::string s = e.toString();
-      const char* theString = s.c_str();
-      const char* firstPart =
-        "Assertion failure\nvoid AssertWhite::testReallyLongAssert()\n";
-      string lastPartStr = "\n\n  false\n" + msg;
-      const char* lastPart = lastPartStr.c_str();
-      TS_ASSERT(strncmp(theString, firstPart, strlen(firstPart)) == 0);
-      TS_ASSERT(strncmp(theString + strlen(theString) - strlen(lastPart),
-                        lastPart, strlen(lastPart)) == 0);
-    } catch(...) {
-      TS_FAIL("Threw the wrong kind of exception !");
-    }
-
-    // Now test an assert with a format that drives it over the 512
-    // byte initial buffer.  This was a bug in r1441, see bug:
-    // https://github.com/CVC4/CVC4/issues/465
-    string fmt = string(200, 'x') + " %s " + string(200, 'x');
-    string arg(200, 'y');
-    try {
-      AlwaysAssert(false, fmt.c_str(), arg.c_str());
-      TS_FAIL("Should have thrown an exception !");
-    } catch(AssertionException& e) {
-      // we don't want to match on the entire string, because it may
-      // have an absolute path to the unit test binary, line number
-      // info, etc.
-      std::string s = e.toString();
-      const char* theString = s.c_str();
-      const char* firstPart =
-        "Assertion failure\nvoid AssertWhite::testReallyLongAssert()\n";
-      string lastPartStr = "\n\n  false\n" + string(200, 'x') + " " +
-        string(200, 'y') + " " + string(200, 'x');
-      const char* lastPart = lastPartStr.c_str();
-      TS_ASSERT(strncmp(theString, firstPart, strlen(firstPart)) == 0);
-      TS_ASSERT(strncmp(theString + strlen(theString) - strlen(lastPart),
-                        lastPart, strlen(lastPart)) == 0);
-    } catch(...) {
-      TS_FAIL("Threw the wrong kind of exception !");
-    }
-  }
+   TS_ASSERT_THROWS_NOTHING(Assert(true));
+   TS_UTILS_EXPECT_ABORT(AlwaysAssert(false));
+   TS_UTILS_EXPECT_ABORT(Unreachable());
+   TS_UTILS_EXPECT_ABORT(Unhandled());
+   TS_UTILS_EXPECT_ABORT(Unimplemented());
+   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"));
+ }
 
   void testUnreachable() {
-    TS_ASSERT_THROWS(Unreachable(), UnreachableCodeException&);
-    TS_ASSERT_THROWS(Unreachable("hello"), UnreachableCodeException&);
-    TS_ASSERT_THROWS(Unreachable("hello %s", "world"),
-                     UnreachableCodeException&);
+    TS_UTILS_EXPECT_ABORT(Unreachable());
+    TS_UTILS_EXPECT_ABORT(Unreachable() << "hello");
+    TS_UTILS_EXPECT_ABORT(Unreachable() << "hello "
+                                        << "world");
 
     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_UTILS_EXPECT_ABORT(Unhandled());
+    TS_UTILS_EXPECT_ABORT(Unhandled() << x);
+    TS_UTILS_EXPECT_ABORT(Unhandled() << "foo");
+    TS_UTILS_EXPECT_ABORT(Unhandled() << "foo "
+                                      << "bar"
+                                      << " baz");
   }
 
 };
diff --git a/test/unit/util/binary_heap_black.h b/test/unit/util/binary_heap_black.h
index 192237b49..3cb18c974 100644
--- a/test/unit/util/binary_heap_black.h
+++ b/test/unit/util/binary_heap_black.h
@@ -19,6 +19,7 @@
 #include <iostream>
 #include <sstream>
 
+#include "test_utils.h"
 #include "util/bin_heap.h"
 
 using namespace CVC4;
@@ -43,8 +44,8 @@ class BinaryHeapBlack : public CxxTest::TestSuite {
     TS_ASSERT_EQUALS(heap.size(), 0u);
     TS_ASSERT(heap.empty());
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS_ANYTHING(heap.top());
-    TS_ASSERT_THROWS_ANYTHING(heap.pop());
+    TS_UTILS_EXPECT_ABORT(heap.top());
+    TS_UTILS_EXPECT_ABORT(heap.pop());
 #endif /* CVC4_ASSERTIONS */
     TS_ASSERT_EQUALS(heap.begin(), heap.end());
 
@@ -60,8 +61,8 @@ class BinaryHeapBlack : public CxxTest::TestSuite {
     TS_ASSERT(heap.empty());
     TS_ASSERT_EQUALS(heap.size(), 0u);
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS_ANYTHING(heap.top());
-    TS_ASSERT_THROWS_ANYTHING(heap.pop());
+    TS_UTILS_EXPECT_ABORT(heap.top());
+    TS_UTILS_EXPECT_ABORT(heap.pop());
 #endif /* CVC4_ASSERTIONS */
 
     // Next test a heap of 4 elements
@@ -118,8 +119,8 @@ class BinaryHeapBlack : public CxxTest::TestSuite {
     TS_ASSERT(heap.empty());
     TS_ASSERT_EQUALS(heap.size(), 0u);
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS_ANYTHING(heap.top());
-    TS_ASSERT_THROWS_ANYTHING(heap.pop());
+    TS_UTILS_EXPECT_ABORT(heap.top());
+    TS_UTILS_EXPECT_ABORT(heap.pop());
 #endif /* CVC4_ASSERTIONS */
 
     // Now with a few updates
diff --git a/test/unit/util/check_white.h b/test/unit/util/check_white.h
index 052a35110..1a169f320 100644
--- a/test/unit/util/check_white.h
+++ b/test/unit/util/check_white.h
@@ -19,7 +19,7 @@
 #include <cstring>
 #include <string>
 
-#include "base/cvc4_check.h"
+#include "base/check.h"
 #include "test_utils.h"
 
 using namespace std;
@@ -40,25 +40,25 @@ class CheckWhite : public CxxTest::TestSuite
                     "return type.";
   }
 
-  void testCheck() { CVC4_CHECK(kOne >= 0) << kOne << " must be positive"; }
+  void testCheck() { AlwaysAssert(kOne >= 0) << kOne << " must be positive"; }
   void testDCheck()
   {
-    CVC4_DCHECK(kOne == 1) << "always passes";
+    Assert(kOne == 1) << "always passes";
 #ifndef CVC4_ASSERTIONS
-    CVC4_DCHECK(false) << "Will not be compiled in when CVC4_ASSERTIONS off.";
+    Assert(false) << "Will not be compiled in when CVC4_ASSERTIONS off.";
 #endif /* CVC4_ASSERTIONS */
   }
 
   void testPointerTypeCanBeTheCondition()
   {
     const int* one_pointer = &kOne;
-    CVC4_CHECK(one_pointer);
+    AlwaysAssert(one_pointer);
   }
 
   void testExpectAbort()
   {
-    TS_UTILS_EXPECT_ABORT(CVC4_CHECK(false));
-    TS_UTILS_EXPECT_ABORT(CVC4_DCHECK(false));
+    TS_UTILS_EXPECT_ABORT(AlwaysAssert(false));
+    TS_UTILS_EXPECT_ABORT(Assert(false));
   }
 };
 
diff --git a/test/unit/util/stats_black.h b/test/unit/util/stats_black.h
index 5cb6c2099..9c40d8a47 100644
--- a/test/unit/util/stats_black.h
+++ b/test/unit/util/stats_black.h
@@ -46,8 +46,8 @@ public:
     // StatisticsRegistry
     //static void flushStatistics(std::ostream& out);
 
-    //static inline void registerStat(Stat* s) throw (AssertionException);
-    //static inline void unregisterStat(Stat* s) throw (AssertionException);
+    // static inline void registerStat(Stat* s);
+    // static inline void unregisterStat(Stat* s);
 
     string empty, bar = "bar", baz = "baz";
     ReferenceStat<string> refStr("stat #1", empty);