google test: Infrastructure and first api test. (#5548)

This sets up the infrastructure for migrating unit tests from CxxTest to
Google Test. It further migrates api/datatype_api_black to the new
infrastructure.

17 files changed, 302 insertions, 250 deletions

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index acc13c2ee..5da6b4208 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -61,10 +61,12 @@ jobs:
       run: |
         sudo apt-get update
         sudo apt-get install -y \
+          build-essential \
           ccache \
           cxxtest \
           libcln-dev \
           libgmp-dev \
+          libgtest-dev \
           libedit-dev \
           flex \
           libfl-dev \
@@ -72,6 +74,10 @@ jobs:
         python3 -m pip install toml
         python3 -m pip install setuptools
         python3 -m pip install pexpect
+        cd /usr/src/googletest
+        sudo cmake .
+        sudo cmake --build . --target install
+        cd -
         echo "/usr/lib/ccache" >> $GITHUB_PATH
 
     # Note: macOS comes with a libedit; it does not need to brew-installed
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 8eab22e4a..6c3ed4bbc 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -8,7 +8,7 @@
 ## All rights reserved.  See the file COPYING in the top-level source
 ## directory for licensing information.
 ##
-cmake_minimum_required(VERSION 3.4)
+cmake_minimum_required(VERSION 3.9)
 
 #-----------------------------------------------------------------------------#
 # Project configuration
diff --git a/INSTALL.md b/INSTALL.md
index b3308726b..5693dbc1c 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -46,7 +46,7 @@ compatible.
 
 - [GNU C and C++ (gcc and g++)](https://gcc.gnu.org)
   or [Clang](https://clang.llvm.org) (reasonably recent versions)
-- [CMake >= 3.1](https://cmake.org)
+- [CMake >= 3.9](https://cmake.org)
 - [GNU Bash](https://www.gnu.org/software/bash/)
 - [Python >= 2.7](https://www.python.org)
   + module [toml](https://pypi.org/project/toml/)
@@ -195,6 +195,12 @@ provided with CVC4.
 See [Testing CVC4](#Testing-CVC4) below for more details.
 
 
+### Google Test Unit Testing Framework (Unit Tests)
+
+[Google Test](https://github.com/google/googletest) is required to optionally
+run CVC4's unit tests (included with the distribution). 
+See [Testing CVC4](#Testing-CVC4) below for more details.
+
 ## Language bindings
 
 CVC4 provides a complete and flexible C++ API (see `examples/api` for
diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
index bb53c15b0..d65e022c9 100644
--- a/test/unit/CMakeLists.txt
+++ b/test/unit/CMakeLists.txt
@@ -13,6 +13,8 @@
 # custom finder modules).
 set(CxxTest_HOME ${CXXTEST_DIR})
 find_package(CxxTest REQUIRED)
+find_package(GTest REQUIRED)
+include(GoogleTest)
 
 include_directories(.)
 include_directories(${PROJECT_SOURCE_DIR}/src)
@@ -36,9 +38,47 @@ set(CVC4_CXXTEST_FLAGS_BLACK
 set(CVC4_CXXTEST_FLAGS_WHITE -fno-access-control ${CVC4_CXXTEST_FLAGS_BLACK})
 
 # Generate and add unit test.
+macro(cvc4_add_unit_test is_white name output_dir)
+  set(test_src ${CMAKE_CURRENT_LIST_DIR}/${name}.cpp)
+  add_executable(${name} ${test_src})
+  gtest_add_tests(TARGET ${name})
+  target_link_libraries(${name} main-test)
+  target_link_libraries(${name} GTest::GTest)
+  target_link_libraries(${name} GTest::Main)
+  if(USE_LFSC)
+    # We don't link against LFSC, because CVC4 is already linked against it.
+    target_include_directories(${name} PRIVATE ${LFSC_INCLUDE_DIR})
+  endif()
+  if(USE_POLY)
+    # We don't link against libpoly, because CVC4 is already linked against it.
+    target_include_directories(${name} PRIVATE ${POLY_INCLUDE_DIR})
+  endif()
+  if(${is_white})
+    target_compile_options(${name} PRIVATE -fno-access-control)
+  endif()
+  add_dependencies(build-units ${name})
+  # Generate into bin/test/unit/<output_dir>.
+  set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/unit/${output_dir})
+  set_target_properties(${name}
+    PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${test_bin_dir})
+  # The test target is prefixed with test identifier 'unit/' and the path,
+  # e.g., for '<output_dir>/myunittest.h'
+  #   we create test target 'unit/<output_dir>/myunittest'
+  #   and run it with 'ctest -R "example/<output_dir>/myunittest"'.
+  if("${output_dir}" STREQUAL "")
+    set(test_name unit/${name})
+  else()
+    set(test_name unit/${output_dir}/${name})
+  endif()
+  add_test(${test_name} ${test_bin_dir}/${name})
+  set_tests_properties(${test_name} PROPERTIES LABELS "unit")
+endmacro()
+
+# Generate and add unit test.
 # Note: we do not use cxxtest_add_test from the FindCxxTest module since it
 #       does not allow test names containing '/'.
-macro(cvc4_add_unit_test is_white name output_dir)
+# !! This macro will be removed when all unit tests are migrated to Google Test.
+macro(cvc4_add_cxx_unit_test is_white name output_dir)
   # generate the test sources
   set(test_src ${CMAKE_CURRENT_BINARY_DIR}/${name}.cpp)
   set(test_header ${CMAKE_CURRENT_LIST_DIR}/${name}.h)
@@ -110,6 +150,15 @@ macro(cvc4_add_unit_test_white name output_dir)
   cvc4_add_unit_test(TRUE ${name} ${output_dir})
 endmacro()
 
+# !! Will be removed when all unit tests are migrated to Google Test.
+macro(cvc4_add_cxx_unit_test_black name output_dir)
+  cvc4_add_cxx_unit_test(FALSE ${name} ${output_dir})
+endmacro()
+# !! Will be removed when all unit tests are migrated to Google Test.
+macro(cvc4_add_cxx_unit_test_white name output_dir)
+  cvc4_add_cxx_unit_test(TRUE ${name} ${output_dir})
+endmacro()
+
 add_subdirectory(api)
 add_subdirectory(base)
 add_subdirectory(context)
diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt
index 1412c7f66..9fcf881a8 100644
--- a/test/unit/api/CMakeLists.txt
+++ b/test/unit/api/CMakeLists.txt
@@ -12,10 +12,10 @@
 # Add unit tests
 
 cvc4_add_unit_test_black(datatype_api_black api)
-cvc4_add_unit_test_black(op_black api)
-cvc4_add_unit_test_black(result_black api)
-cvc4_add_unit_test_black(solver_black api)
-cvc4_add_unit_test_black(sort_black api)
-cvc4_add_unit_test_black(term_black api)
-cvc4_add_unit_test_black(grammar_black api)
+cvc4_add_cxx_unit_test_black(op_black api)
+cvc4_add_cxx_unit_test_black(result_black api)
+cvc4_add_cxx_unit_test_black(solver_black api)
+cvc4_add_cxx_unit_test_black(sort_black api)
+cvc4_add_cxx_unit_test_black(term_black api)
+cvc4_add_cxx_unit_test_black(grammar_black api)
 
diff --git a/test/unit/api/datatype_api_black.h b/test/unit/api/datatype_api_black.cpp
index 4564b261a..f61637221 100644
--- a/test/unit/api/datatype_api_black.h
+++ b/test/unit/api/datatype_api_black.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file datatype_api_black.h
+/*! \file datatype_api_black.cpp
  ** \verbatim
  ** Top contributors (to current version):
  **   Andrew Reynolds, Aina Niemetz, Andres Noetzli
@@ -14,39 +14,11 @@
  ** Black box testing of the datatype classes of the C++ API.
  **/
 
-#include <cxxtest/TestSuite.h>
-
-#include "api/cvc4cpp.h"
+#include "test_api.h"
 
 using namespace CVC4::api;
 
-class DatatypeBlack : public CxxTest::TestSuite
-{
- public:
-  void setUp() override;
-  void tearDown() override;
-
-  void testMkDatatypeSort();
-  void testMkDatatypeSorts();
-
-  void testDatatypeStructs();
-  void testDatatypeNames();
-
-  void testParametricDatatype();
-
-  void testDatatypeSimplyRec();
-
-  void testDatatypeSpecializedCons();
-
- private:
-  Solver d_solver;
-};
-
-void DatatypeBlack::setUp() {}
-
-void DatatypeBlack::tearDown() {}
-
-void DatatypeBlack::testMkDatatypeSort()
+TEST_F(TestApi, mkDatatypeSort)
 {
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
   DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
@@ -58,12 +30,12 @@ void DatatypeBlack::testMkDatatypeSort()
   Datatype d = listSort.getDatatype();
   DatatypeConstructor consConstr = d[0];
   DatatypeConstructor nilConstr = d[1];
-  TS_ASSERT_THROWS(d[2], CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(consConstr.getConstructorTerm());
-  TS_ASSERT_THROWS_NOTHING(nilConstr.getConstructorTerm());
+  EXPECT_THROW(d[2], CVC4ApiException);
+  ASSERT_NO_THROW(consConstr.getConstructorTerm());
+  ASSERT_NO_THROW(nilConstr.getConstructorTerm());
 }
 
-void DatatypeBlack::testMkDatatypeSorts()
+TEST_F(TestApi, mkDatatypeSorts)
 {
   /* Create two mutual datatypes corresponding to this definition
    * block:
@@ -103,33 +75,32 @@ void DatatypeBlack::testMkDatatypeSorts()
   dtdecls.push_back(tree);
   dtdecls.push_back(list);
   std::vector<Sort> dtsorts;
-  TS_ASSERT_THROWS_NOTHING(dtsorts =
-                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
-  TS_ASSERT(dtsorts.size() == dtdecls.size());
-  for (unsigned i = 0, ndecl = dtdecls.size(); i < ndecl; i++)
+  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  ASSERT_EQ(dtsorts.size(), dtdecls.size());
+  for (size_t i = 0, ndecl = dtdecls.size(); i < ndecl; i++)
   {
-    TS_ASSERT(dtsorts[i].isDatatype());
-    TS_ASSERT(!dtsorts[i].getDatatype().isFinite());
-    TS_ASSERT(dtsorts[i].getDatatype().getName() == dtdecls[i].getName());
+    ASSERT_TRUE(dtsorts[i].isDatatype());
+    EXPECT_FALSE(dtsorts[i].getDatatype().isFinite());
+    EXPECT_EQ(dtsorts[i].getDatatype().getName(), dtdecls[i].getName());
   }
   // verify the resolution was correct
   Datatype dtTree = dtsorts[0].getDatatype();
   DatatypeConstructor dtcTreeNode = dtTree[0];
-  TS_ASSERT(dtcTreeNode.getName() == "node");
+  EXPECT_EQ(dtcTreeNode.getName(), "node");
   DatatypeSelector dtsTreeNodeLeft = dtcTreeNode[0];
-  TS_ASSERT(dtsTreeNodeLeft.getName() == "left");
+  EXPECT_EQ(dtsTreeNodeLeft.getName(), "left");
   // argument type should have resolved to be recursive
-  TS_ASSERT(dtsTreeNodeLeft.getRangeSort().isDatatype());
-  TS_ASSERT(dtsTreeNodeLeft.getRangeSort() == dtsorts[0]);
+  EXPECT_TRUE(dtsTreeNodeLeft.getRangeSort().isDatatype());
+  EXPECT_EQ(dtsTreeNodeLeft.getRangeSort(), dtsorts[0]);
 
   // fails due to empty datatype
   std::vector<DatatypeDecl> dtdeclsBad;
   DatatypeDecl emptyD = d_solver.mkDatatypeDecl("emptyD");
   dtdeclsBad.push_back(emptyD);
-  TS_ASSERT_THROWS(d_solver.mkDatatypeSorts(dtdeclsBad), CVC4ApiException&);
+  EXPECT_THROW(d_solver.mkDatatypeSorts(dtdeclsBad), CVC4ApiException);
 }
 
-void DatatypeBlack::testDatatypeStructs()
+TEST_F(TestApi, datatypeStructs)
 {
   Sort intSort = d_solver.getIntegerSort();
   Sort boolSort = d_solver.getBooleanSort();
@@ -140,21 +111,21 @@ void DatatypeBlack::testDatatypeStructs()
   cons.addSelector("head", intSort);
   cons.addSelectorSelf("tail");
   Sort nullSort;
-  TS_ASSERT_THROWS(cons.addSelector("null", nullSort), CVC4ApiException&);
+  EXPECT_THROW(cons.addSelector("null", nullSort), CVC4ApiException);
   dtypeSpec.addConstructor(cons);
   DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   dtypeSpec.addConstructor(nil);
   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
   Datatype dt = dtypeSort.getDatatype();
-  TS_ASSERT(!dt.isCodatatype());
-  TS_ASSERT(!dt.isTuple());
-  TS_ASSERT(!dt.isRecord());
-  TS_ASSERT(!dt.isFinite());
-  TS_ASSERT(dt.isWellFounded());
+  EXPECT_FALSE(dt.isCodatatype());
+  EXPECT_FALSE(dt.isTuple());
+  EXPECT_FALSE(dt.isRecord());
+  EXPECT_FALSE(dt.isFinite());
+  EXPECT_TRUE(dt.isWellFounded());
   // get constructor
   DatatypeConstructor dcons = dt[0];
   Term consTerm = dcons.getConstructorTerm();
-  TS_ASSERT(dcons.getNumSelectors() == 2);
+  EXPECT_EQ(dcons.getNumSelectors(), 2);
 
   // create datatype sort to test
   DatatypeDecl dtypeSpecEnum = d_solver.mkDatatypeDecl("enum");
@@ -166,8 +137,8 @@ void DatatypeBlack::testDatatypeStructs()
   dtypeSpecEnum.addConstructor(cc);
   Sort dtypeSortEnum = d_solver.mkDatatypeSort(dtypeSpecEnum);
   Datatype dtEnum = dtypeSortEnum.getDatatype();
-  TS_ASSERT(!dtEnum.isTuple());
-  TS_ASSERT(dtEnum.isFinite());
+  EXPECT_FALSE(dtEnum.isTuple());
+  EXPECT_TRUE(dtEnum.isFinite());
 
   // create codatatype
   DatatypeDecl dtypeSpecStream = d_solver.mkDatatypeDecl("stream", true);
@@ -178,39 +149,39 @@ void DatatypeBlack::testDatatypeStructs()
   dtypeSpecStream.addConstructor(consStream);
   Sort dtypeSortStream = d_solver.mkDatatypeSort(dtypeSpecStream);
   Datatype dtStream = dtypeSortStream.getDatatype();
-  TS_ASSERT(dtStream.isCodatatype());
-  TS_ASSERT(!dtStream.isFinite());
+  EXPECT_TRUE(dtStream.isCodatatype());
+  EXPECT_FALSE(dtStream.isFinite());
   // codatatypes may be well-founded
-  TS_ASSERT(dtStream.isWellFounded());
+  EXPECT_TRUE(dtStream.isWellFounded());
 
   // create tuple
   Sort tupSort = d_solver.mkTupleSort({boolSort});
   Datatype dtTuple = tupSort.getDatatype();
-  TS_ASSERT(dtTuple.isTuple());
-  TS_ASSERT(!dtTuple.isRecord());
-  TS_ASSERT(dtTuple.isFinite());
-  TS_ASSERT(dtTuple.isWellFounded());
+  EXPECT_TRUE(dtTuple.isTuple());
+  EXPECT_FALSE(dtTuple.isRecord());
+  EXPECT_TRUE(dtTuple.isFinite());
+  EXPECT_TRUE(dtTuple.isWellFounded());
 
   // create record
   std::vector<std::pair<std::string, Sort>> fields = {
       std::make_pair("b", boolSort), std::make_pair("i", intSort)};
   Sort recSort = d_solver.mkRecordSort(fields);
-  TS_ASSERT(recSort.isDatatype());
+  EXPECT_TRUE(recSort.isDatatype());
   Datatype dtRecord = recSort.getDatatype();
-  TS_ASSERT(!dtRecord.isTuple());
-  TS_ASSERT(dtRecord.isRecord());
-  TS_ASSERT(!dtRecord.isFinite());
-  TS_ASSERT(dtRecord.isWellFounded());
+  EXPECT_FALSE(dtRecord.isTuple());
+  EXPECT_TRUE(dtRecord.isRecord());
+  EXPECT_FALSE(dtRecord.isFinite());
+  EXPECT_TRUE(dtRecord.isWellFounded());
 }
 
-void DatatypeBlack::testDatatypeNames()
+TEST_F(TestApi, datatypeNames)
 {
   Sort intSort = d_solver.getIntegerSort();
 
   // create datatype sort to test
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
-  TS_ASSERT_THROWS_NOTHING(dtypeSpec.getName());
-  TS_ASSERT(dtypeSpec.getName() == std::string("list"));
+  ASSERT_NO_THROW(dtypeSpec.getName());
+  EXPECT_EQ(dtypeSpec.getName(), std::string("list"));
   DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", intSort);
   cons.addSelectorSelf("tail");
@@ -219,28 +190,28 @@ void DatatypeBlack::testDatatypeNames()
   dtypeSpec.addConstructor(nil);
   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
   Datatype dt = dtypeSort.getDatatype();
-  TS_ASSERT(dt.getName() == std::string("list"));
-  TS_ASSERT_THROWS_NOTHING(dt.getConstructor("nil"));
-  TS_ASSERT_THROWS_NOTHING(dt["cons"]);
-  TS_ASSERT_THROWS(dt.getConstructor("head"), CVC4ApiException&);
-  TS_ASSERT_THROWS(dt.getConstructor(""), CVC4ApiException&);
+  EXPECT_EQ(dt.getName(), std::string("list"));
+  ASSERT_NO_THROW(dt.getConstructor("nil"));
+  ASSERT_NO_THROW(dt["cons"]);
+  ASSERT_THROW(dt.getConstructor("head"), CVC4ApiException);
+  ASSERT_THROW(dt.getConstructor(""), CVC4ApiException);
 
   DatatypeConstructor dcons = dt[0];
-  TS_ASSERT(dcons.getName() == std::string("cons"));
-  TS_ASSERT_THROWS_NOTHING(dcons.getSelector("head"));
-  TS_ASSERT_THROWS_NOTHING(dcons["tail"]);
-  TS_ASSERT_THROWS(dcons.getSelector("cons"), CVC4ApiException&);
+  EXPECT_EQ(dcons.getName(), std::string("cons"));
+  ASSERT_NO_THROW(dcons.getSelector("head"));
+  ASSERT_NO_THROW(dcons["tail"]);
+  ASSERT_THROW(dcons.getSelector("cons"), CVC4ApiException);
 
   // get selector
   DatatypeSelector dselTail = dcons[1];
-  TS_ASSERT(dselTail.getName() == std::string("tail"));
-  TS_ASSERT(dselTail.getRangeSort() == dtypeSort);
+  EXPECT_EQ(dselTail.getName(), std::string("tail"));
+  EXPECT_EQ(dselTail.getRangeSort(), dtypeSort);
 
   // possible to construct null datatype declarations if not using solver
-  TS_ASSERT_THROWS(DatatypeDecl().getName(), CVC4ApiException&);
+  ASSERT_THROW(DatatypeDecl().getName(), CVC4ApiException);
 }
 
-void DatatypeBlack::testParametricDatatype()
+TEST_F(TestApi, parametricDatatype)
 {
   std::vector<Sort> v;
   Sort t1 = d_solver.mkParamSort("T1");
@@ -257,7 +228,7 @@ void DatatypeBlack::testParametricDatatype()
 
   Sort pairType = d_solver.mkDatatypeSort(pairSpec);
 
-  TS_ASSERT(pairType.getDatatype().isParametric());
+  EXPECT_TRUE(pairType.getDatatype().isParametric());
 
   v.clear();
   v.push_back(d_solver.getIntegerSort());
@@ -276,49 +247,49 @@ void DatatypeBlack::testParametricDatatype()
   v.push_back(d_solver.getRealSort());
   Sort pairIntReal = pairType.instantiate(v);
 
-  TS_ASSERT_DIFFERS(pairIntInt, pairRealReal);
-  TS_ASSERT_DIFFERS(pairIntReal, pairRealReal);
-  TS_ASSERT_DIFFERS(pairRealInt, pairRealReal);
-  TS_ASSERT_DIFFERS(pairIntInt, pairIntReal);
-  TS_ASSERT_DIFFERS(pairIntInt, pairRealInt);
-  TS_ASSERT_DIFFERS(pairIntReal, pairRealInt);
-
-  TS_ASSERT(pairRealReal.isComparableTo(pairRealReal));
-  TS_ASSERT(!pairIntReal.isComparableTo(pairRealReal));
-  TS_ASSERT(!pairRealInt.isComparableTo(pairRealReal));
-  TS_ASSERT(!pairIntInt.isComparableTo(pairRealReal));
-  TS_ASSERT(!pairRealReal.isComparableTo(pairRealInt));
-  TS_ASSERT(!pairIntReal.isComparableTo(pairRealInt));
-  TS_ASSERT(pairRealInt.isComparableTo(pairRealInt));
-  TS_ASSERT(!pairIntInt.isComparableTo(pairRealInt));
-  TS_ASSERT(!pairRealReal.isComparableTo(pairIntReal));
-  TS_ASSERT(pairIntReal.isComparableTo(pairIntReal));
-  TS_ASSERT(!pairRealInt.isComparableTo(pairIntReal));
-  TS_ASSERT(!pairIntInt.isComparableTo(pairIntReal));
-  TS_ASSERT(!pairRealReal.isComparableTo(pairIntInt));
-  TS_ASSERT(!pairIntReal.isComparableTo(pairIntInt));
-  TS_ASSERT(!pairRealInt.isComparableTo(pairIntInt));
-  TS_ASSERT(pairIntInt.isComparableTo(pairIntInt));
-
-  TS_ASSERT(pairRealReal.isSubsortOf(pairRealReal));
-  TS_ASSERT(!pairIntReal.isSubsortOf(pairRealReal));
-  TS_ASSERT(!pairRealInt.isSubsortOf(pairRealReal));
-  TS_ASSERT(!pairIntInt.isSubsortOf(pairRealReal));
-  TS_ASSERT(!pairRealReal.isSubsortOf(pairRealInt));
-  TS_ASSERT(!pairIntReal.isSubsortOf(pairRealInt));
-  TS_ASSERT(pairRealInt.isSubsortOf(pairRealInt));
-  TS_ASSERT(!pairIntInt.isSubsortOf(pairRealInt));
-  TS_ASSERT(!pairRealReal.isSubsortOf(pairIntReal));
-  TS_ASSERT(pairIntReal.isSubsortOf(pairIntReal));
-  TS_ASSERT(!pairRealInt.isSubsortOf(pairIntReal));
-  TS_ASSERT(!pairIntInt.isSubsortOf(pairIntReal));
-  TS_ASSERT(!pairRealReal.isSubsortOf(pairIntInt));
-  TS_ASSERT(!pairIntReal.isSubsortOf(pairIntInt));
-  TS_ASSERT(!pairRealInt.isSubsortOf(pairIntInt));
-  TS_ASSERT(pairIntInt.isSubsortOf(pairIntInt));
+  EXPECT_NE(pairIntInt, pairRealReal);
+  EXPECT_NE(pairIntReal, pairRealReal);
+  EXPECT_NE(pairRealInt, pairRealReal);
+  EXPECT_NE(pairIntInt, pairIntReal);
+  EXPECT_NE(pairIntInt, pairRealInt);
+  EXPECT_NE(pairIntReal, pairRealInt);
+
+  EXPECT_TRUE(pairRealReal.isComparableTo(pairRealReal));
+  EXPECT_FALSE(pairIntReal.isComparableTo(pairRealReal));
+  EXPECT_FALSE(pairRealInt.isComparableTo(pairRealReal));
+  EXPECT_FALSE(pairIntInt.isComparableTo(pairRealReal));
+  EXPECT_FALSE(pairRealReal.isComparableTo(pairRealInt));
+  EXPECT_FALSE(pairIntReal.isComparableTo(pairRealInt));
+  EXPECT_TRUE(pairRealInt.isComparableTo(pairRealInt));
+  EXPECT_FALSE(pairIntInt.isComparableTo(pairRealInt));
+  EXPECT_FALSE(pairRealReal.isComparableTo(pairIntReal));
+  EXPECT_TRUE(pairIntReal.isComparableTo(pairIntReal));
+  EXPECT_FALSE(pairRealInt.isComparableTo(pairIntReal));
+  EXPECT_FALSE(pairIntInt.isComparableTo(pairIntReal));
+  EXPECT_FALSE(pairRealReal.isComparableTo(pairIntInt));
+  EXPECT_FALSE(pairIntReal.isComparableTo(pairIntInt));
+  EXPECT_FALSE(pairRealInt.isComparableTo(pairIntInt));
+  EXPECT_TRUE(pairIntInt.isComparableTo(pairIntInt));
+
+  EXPECT_TRUE(pairRealReal.isSubsortOf(pairRealReal));
+  EXPECT_FALSE(pairIntReal.isSubsortOf(pairRealReal));
+  EXPECT_FALSE(pairRealInt.isSubsortOf(pairRealReal));
+  EXPECT_FALSE(pairIntInt.isSubsortOf(pairRealReal));
+  EXPECT_FALSE(pairRealReal.isSubsortOf(pairRealInt));
+  EXPECT_FALSE(pairIntReal.isSubsortOf(pairRealInt));
+  EXPECT_TRUE(pairRealInt.isSubsortOf(pairRealInt));
+  EXPECT_FALSE(pairIntInt.isSubsortOf(pairRealInt));
+  EXPECT_FALSE(pairRealReal.isSubsortOf(pairIntReal));
+  EXPECT_TRUE(pairIntReal.isSubsortOf(pairIntReal));
+  EXPECT_FALSE(pairRealInt.isSubsortOf(pairIntReal));
+  EXPECT_FALSE(pairIntInt.isSubsortOf(pairIntReal));
+  EXPECT_FALSE(pairRealReal.isSubsortOf(pairIntInt));
+  EXPECT_FALSE(pairIntReal.isSubsortOf(pairIntInt));
+  EXPECT_FALSE(pairRealInt.isSubsortOf(pairIntInt));
+  EXPECT_TRUE(pairIntInt.isSubsortOf(pairIntInt));
 }
 
-void DatatypeBlack::testDatatypeSimplyRec()
+TEST_F(TestApi, datatypeSimplyRec)
 {
   /* Create mutual datatypes corresponding to this definition block:
    *
@@ -365,15 +336,14 @@ void DatatypeBlack::testDatatypeSimplyRec()
   dtdecls.push_back(ns);
   // this is well-founded and has no nested recursion
   std::vector<Sort> dtsorts;
-  TS_ASSERT_THROWS_NOTHING(dtsorts =
-                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
-  TS_ASSERT(dtsorts.size() == 3);
-  TS_ASSERT(dtsorts[0].getDatatype().isWellFounded());
-  TS_ASSERT(dtsorts[1].getDatatype().isWellFounded());
-  TS_ASSERT(dtsorts[2].getDatatype().isWellFounded());
-  TS_ASSERT(!dtsorts[0].getDatatype().hasNestedRecursion());
-  TS_ASSERT(!dtsorts[1].getDatatype().hasNestedRecursion());
-  TS_ASSERT(!dtsorts[2].getDatatype().hasNestedRecursion());
+  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  ASSERT_EQ(dtsorts.size(), 3);
+  EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded());
+  EXPECT_TRUE(dtsorts[1].getDatatype().isWellFounded());
+  EXPECT_TRUE(dtsorts[2].getDatatype().isWellFounded());
+  EXPECT_FALSE(dtsorts[0].getDatatype().hasNestedRecursion());
+  EXPECT_FALSE(dtsorts[1].getDatatype().hasNestedRecursion());
+  EXPECT_FALSE(dtsorts[2].getDatatype().hasNestedRecursion());
 
   /* Create mutual datatypes corresponding to this definition block:
    *   DATATYPE
@@ -397,14 +367,13 @@ void DatatypeBlack::testDatatypeSimplyRec()
 
   dtsorts.clear();
   // this is not well-founded due to non-simple recursion
-  TS_ASSERT_THROWS_NOTHING(dtsorts =
-                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
-  TS_ASSERT(dtsorts.size() == 1);
-  TS_ASSERT(dtsorts[0].getDatatype()[0][0].getRangeSort().isArray());
-  TS_ASSERT(dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort()
-            == dtsorts[0]);
-  TS_ASSERT(dtsorts[0].getDatatype().isWellFounded());
-  TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion());
+  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  ASSERT_EQ(dtsorts.size(), 1);
+  ASSERT_TRUE(dtsorts[0].getDatatype()[0][0].getRangeSort().isArray());
+  EXPECT_EQ(dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort(),
+            dtsorts[0]);
+  EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded());
+  EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
 
   /* Create mutual datatypes corresponding to this definition block:
    *   DATATYPE
@@ -437,13 +406,12 @@ void DatatypeBlack::testDatatypeSimplyRec()
 
   dtsorts.clear();
   // both are well-founded and have nested recursion
-  TS_ASSERT_THROWS_NOTHING(dtsorts =
-                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
-  TS_ASSERT(dtsorts.size() == 2);
-  TS_ASSERT(dtsorts[0].getDatatype().isWellFounded());
-  TS_ASSERT(dtsorts[1].getDatatype().isWellFounded());
-  TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion());
-  TS_ASSERT(dtsorts[1].getDatatype().hasNestedRecursion());
+  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  ASSERT_EQ(dtsorts.size(), 2);
+  EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded());
+  EXPECT_TRUE(dtsorts[1].getDatatype().isWellFounded());
+  EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
+  EXPECT_TRUE(dtsorts[1].getDatatype().hasNestedRecursion());
 
   /* Create mutual datatypes corresponding to this definition block:
    *   DATATYPE
@@ -476,13 +444,12 @@ void DatatypeBlack::testDatatypeSimplyRec()
 
   dtsorts.clear();
   // both are well-founded and have nested recursion
-  TS_ASSERT_THROWS_NOTHING(dtsorts =
-                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
-  TS_ASSERT(dtsorts.size() == 2);
-  TS_ASSERT(dtsorts[0].getDatatype().isWellFounded());
-  TS_ASSERT(dtsorts[1].getDatatype().isWellFounded());
-  TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion());
-  TS_ASSERT(dtsorts[1].getDatatype().hasNestedRecursion());
+  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  ASSERT_EQ(dtsorts.size(), 2);
+  EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded());
+  EXPECT_TRUE(dtsorts[1].getDatatype().isWellFounded());
+  EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
+  EXPECT_TRUE(dtsorts[1].getDatatype().hasNestedRecursion());
 
   /* Create mutual datatypes corresponding to this definition block:
    *   DATATYPE
@@ -515,14 +482,13 @@ void DatatypeBlack::testDatatypeSimplyRec()
   dtdecls.push_back(list5);
 
   // well-founded and has nested recursion
-  TS_ASSERT_THROWS_NOTHING(dtsorts =
-                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
-  TS_ASSERT(dtsorts.size() == 1);
-  TS_ASSERT(dtsorts[0].getDatatype().isWellFounded());
-  TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion());
+  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  ASSERT_EQ(dtsorts.size(), 1);
+  EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded());
+  EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
 }
 
-void DatatypeBlack::testDatatypeSpecializedCons()
+TEST_F(TestApi, datatypeSpecializedCons)
 {
   /* Create mutual datatypes corresponding to this definition block:
    *   DATATYPE
@@ -555,9 +521,8 @@ void DatatypeBlack::testDatatypeSpecializedCons()
 
   std::vector<Sort> dtsorts;
   // make the datatype sorts
-  TS_ASSERT_THROWS_NOTHING(dtsorts =
-                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
-  TS_ASSERT(dtsorts.size() == 1);
+  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  ASSERT_EQ(dtsorts.size(), 1);
   Datatype d = dtsorts[0].getDatatype();
   DatatypeConstructor nilc = d[0];
 
@@ -568,9 +533,8 @@ void DatatypeBlack::testDatatypeSpecializedCons()
 
   Term testConsTerm;
   // get the specialized constructor term for list[Int]
-  TS_ASSERT_THROWS_NOTHING(testConsTerm =
-                               nilc.getSpecializedConstructorTerm(listInt));
-  TS_ASSERT(testConsTerm != nilc.getConstructorTerm());
+  ASSERT_NO_THROW(testConsTerm = nilc.getSpecializedConstructorTerm(listInt));
+  EXPECT_NE(testConsTerm, nilc.getConstructorTerm());
   // error to get the specialized constructor term for Int
-  TS_ASSERT_THROWS(nilc.getSpecializedConstructorTerm(isort), CVC4ApiException&);
+  EXPECT_THROW(nilc.getSpecializedConstructorTerm(isort), CVC4ApiException);
 }
diff --git a/test/unit/base/CMakeLists.txt b/test/unit/base/CMakeLists.txt
index 81d27c040..8274a5a46 100644
--- a/test/unit/base/CMakeLists.txt
+++ b/test/unit/base/CMakeLists.txt
@@ -11,4 +11,4 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(map_util_black base)
+cvc4_add_cxx_unit_test_black(map_util_black base)
diff --git a/test/unit/context/CMakeLists.txt b/test/unit/context/CMakeLists.txt
index 6752f0e78..51465c622 100644
--- a/test/unit/context/CMakeLists.txt
+++ b/test/unit/context/CMakeLists.txt
@@ -11,10 +11,10 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(cdlist_black context)
-cvc4_add_unit_test_black(cdmap_black context)
-cvc4_add_unit_test_white(cdmap_white context)
-cvc4_add_unit_test_black(cdo_black context)
-cvc4_add_unit_test_black(context_black context)
-cvc4_add_unit_test_black(context_mm_black context)
-cvc4_add_unit_test_white(context_white context)
+cvc4_add_cxx_unit_test_black(cdlist_black context)
+cvc4_add_cxx_unit_test_black(cdmap_black context)
+cvc4_add_cxx_unit_test_white(cdmap_white context)
+cvc4_add_cxx_unit_test_black(cdo_black context)
+cvc4_add_cxx_unit_test_black(context_black context)
+cvc4_add_cxx_unit_test_black(context_mm_black context)
+cvc4_add_cxx_unit_test_white(context_white context)
diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt
index c10648c03..6c0abc4ab 100644
--- a/test/unit/expr/CMakeLists.txt
+++ b/test/unit/expr/CMakeLists.txt
@@ -11,20 +11,20 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(attribute_black expr)
-cvc4_add_unit_test_white(attribute_white expr)
-cvc4_add_unit_test_black(expr_manager_public expr)
-cvc4_add_unit_test_black(expr_public expr)
-cvc4_add_unit_test_black(kind_black expr)
-cvc4_add_unit_test_black(kind_map_black expr)
-cvc4_add_unit_test_black(node_black expr)
-cvc4_add_unit_test_black(node_algorithm_black expr)
-cvc4_add_unit_test_black(node_builder_black expr)
-cvc4_add_unit_test_black(node_manager_black expr)
-cvc4_add_unit_test_white(node_manager_white expr)
-cvc4_add_unit_test_black(node_self_iterator_black expr)
-cvc4_add_unit_test_black(node_traversal_black expr)
-cvc4_add_unit_test_white(node_white expr)
-cvc4_add_unit_test_black(symbol_table_black expr)
-cvc4_add_unit_test_black(type_cardinality_public expr)
-cvc4_add_unit_test_white(type_node_white expr)
+cvc4_add_cxx_unit_test_black(attribute_black expr)
+cvc4_add_cxx_unit_test_white(attribute_white expr)
+cvc4_add_cxx_unit_test_black(expr_manager_public expr)
+cvc4_add_cxx_unit_test_black(expr_public expr)
+cvc4_add_cxx_unit_test_black(kind_black expr)
+cvc4_add_cxx_unit_test_black(kind_map_black expr)
+cvc4_add_cxx_unit_test_black(node_black expr)
+cvc4_add_cxx_unit_test_black(node_algorithm_black expr)
+cvc4_add_cxx_unit_test_black(node_builder_black expr)
+cvc4_add_cxx_unit_test_black(node_manager_black expr)
+cvc4_add_cxx_unit_test_white(node_manager_white expr)
+cvc4_add_cxx_unit_test_black(node_self_iterator_black expr)
+cvc4_add_cxx_unit_test_black(node_traversal_black expr)
+cvc4_add_cxx_unit_test_white(node_white expr)
+cvc4_add_cxx_unit_test_black(symbol_table_black expr)
+cvc4_add_cxx_unit_test_black(type_cardinality_public expr)
+cvc4_add_cxx_unit_test_white(type_node_white expr)
diff --git a/test/unit/main/CMakeLists.txt b/test/unit/main/CMakeLists.txt
index 55307db95..59c197f04 100644
--- a/test/unit/main/CMakeLists.txt
+++ b/test/unit/main/CMakeLists.txt
@@ -11,4 +11,4 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(interactive_shell_black main)
+cvc4_add_cxx_unit_test_black(interactive_shell_black main)
diff --git a/test/unit/parser/CMakeLists.txt b/test/unit/parser/CMakeLists.txt
index 1bdcbd5f5..4202ea0c9 100644
--- a/test/unit/parser/CMakeLists.txt
+++ b/test/unit/parser/CMakeLists.txt
@@ -11,5 +11,5 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(parser_black parser)
-cvc4_add_unit_test_black(parser_builder_black parser)
+cvc4_add_cxx_unit_test_black(parser_black parser)
+cvc4_add_cxx_unit_test_black(parser_builder_black parser)
diff --git a/test/unit/preprocessing/CMakeLists.txt b/test/unit/preprocessing/CMakeLists.txt
index 7e142f404..a2381ba90 100644
--- a/test/unit/preprocessing/CMakeLists.txt
+++ b/test/unit/preprocessing/CMakeLists.txt
@@ -11,4 +11,4 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_white(pass_bv_gauss_white preprocessing)
+cvc4_add_cxx_unit_test_white(pass_bv_gauss_white preprocessing)
diff --git a/test/unit/printer/CMakeLists.txt b/test/unit/printer/CMakeLists.txt
index 3b040d1fc..93c241af9 100644
--- a/test/unit/printer/CMakeLists.txt
+++ b/test/unit/printer/CMakeLists.txt
@@ -11,4 +11,4 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(smt2_printer_black printer)
+cvc4_add_cxx_unit_test_black(smt2_printer_black printer)
diff --git a/test/unit/prop/CMakeLists.txt b/test/unit/prop/CMakeLists.txt
index bed0575c6..f866e5ffa 100644
--- a/test/unit/prop/CMakeLists.txt
+++ b/test/unit/prop/CMakeLists.txt
@@ -11,4 +11,4 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_white(cnf_stream_white prop)
+cvc4_add_cxx_unit_test_white(cnf_stream_white prop)
diff --git a/test/unit/test_api.h b/test/unit/test_api.h
new file mode 100644
index 000000000..72d0658a7
--- /dev/null
+++ b/test/unit/test_api.h
@@ -0,0 +1,27 @@
+/*********************                                                        */
+/*! \file datatype_api_black.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Common header for API unit test.
+ **/
+
+#ifndef CVC4__TEST__UNIT__TEST_API_H
+#define CVC4__TEST__UNIT__TEST_API_H
+
+#include "api/cvc4cpp.h"
+#include "gtest/gtest.h"
+
+class TestApi : public ::testing::Test
+{
+ protected:
+  CVC4::api::Solver d_solver;
+};
+
+#endif
diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index 0eccbf436..334ded2d1 100644
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -8,24 +8,24 @@
 ## All rights reserved.  See the file COPYING in the top-level source
 ## directory for licensing information.
 ##
-cvc4_add_unit_test_black(regexp_operation_black theory)
-cvc4_add_unit_test_black(theory_black theory)
-cvc4_add_unit_test_white(evaluator_white theory)
-cvc4_add_unit_test_white(logic_info_white theory)
-cvc4_add_unit_test_white(sequences_rewriter_white theory)
-cvc4_add_unit_test_white(strings_rewriter_white theory)
-cvc4_add_unit_test_white(theory_arith_white theory)
-cvc4_add_unit_test_white(theory_bags_normal_form_white theory)
-cvc4_add_unit_test_white(theory_bags_rewriter_white theory)
-cvc4_add_unit_test_white(theory_bags_type_rules_white theory)
-cvc4_add_unit_test_white(theory_bv_rewriter_white theory)
-cvc4_add_unit_test_white(theory_bv_white theory)
-cvc4_add_unit_test_white(theory_engine_white theory)
-cvc4_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory)
-cvc4_add_unit_test_white(theory_quantifiers_bv_inverter_white theory)
-cvc4_add_unit_test_white(theory_sets_type_enumerator_white theory)
-cvc4_add_unit_test_white(theory_sets_type_rules_white theory)
-cvc4_add_unit_test_white(theory_strings_skolem_cache_black theory)
-cvc4_add_unit_test_white(theory_strings_word_white theory)
-cvc4_add_unit_test_white(theory_white theory)
-cvc4_add_unit_test_white(type_enumerator_white theory)
+cvc4_add_cxx_unit_test_black(regexp_operation_black theory)
+cvc4_add_cxx_unit_test_black(theory_black theory)
+cvc4_add_cxx_unit_test_white(evaluator_white theory)
+cvc4_add_cxx_unit_test_white(logic_info_white theory)
+cvc4_add_cxx_unit_test_white(sequences_rewriter_white theory)
+cvc4_add_cxx_unit_test_white(strings_rewriter_white theory)
+cvc4_add_cxx_unit_test_white(theory_arith_white theory)
+cvc4_add_cxx_unit_test_white(theory_bags_normal_form_white theory)
+cvc4_add_cxx_unit_test_white(theory_bags_rewriter_white theory)
+cvc4_add_cxx_unit_test_white(theory_bags_type_rules_white theory)
+cvc4_add_cxx_unit_test_white(theory_bv_rewriter_white theory)
+cvc4_add_cxx_unit_test_white(theory_bv_white theory)
+cvc4_add_cxx_unit_test_white(theory_engine_white theory)
+cvc4_add_cxx_unit_test_white(theory_quantifiers_bv_instantiator_white theory)
+cvc4_add_cxx_unit_test_white(theory_quantifiers_bv_inverter_white theory)
+cvc4_add_cxx_unit_test_white(theory_sets_type_enumerator_white theory)
+cvc4_add_cxx_unit_test_white(theory_sets_type_rules_white theory)
+cvc4_add_cxx_unit_test_white(theory_strings_skolem_cache_black theory)
+cvc4_add_cxx_unit_test_white(theory_strings_word_white theory)
+cvc4_add_cxx_unit_test_white(theory_white theory)
+cvc4_add_cxx_unit_test_white(type_enumerator_white theory)
diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt
index 0fd7894fe..148ae9910 100644
--- a/test/unit/util/CMakeLists.txt
+++ b/test/unit/util/CMakeLists.txt
@@ -11,25 +11,25 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_white(array_store_all_white util)
-cvc4_add_unit_test_white(assert_white util)
-cvc4_add_unit_test_black(binary_heap_black util)
-cvc4_add_unit_test_black(bitvector_black util)
-cvc4_add_unit_test_black(boolean_simplification_black util)
-cvc4_add_unit_test_black(cardinality_public util)
-cvc4_add_unit_test_white(check_white util)
-cvc4_add_unit_test_black(configuration_black util)
-cvc4_add_unit_test_black(datatype_black util)
-cvc4_add_unit_test_black(exception_black util)
+cvc4_add_cxx_unit_test_white(array_store_all_white util)
+cvc4_add_cxx_unit_test_white(assert_white util)
+cvc4_add_cxx_unit_test_black(binary_heap_black util)
+cvc4_add_cxx_unit_test_black(bitvector_black util)
+cvc4_add_cxx_unit_test_black(boolean_simplification_black util)
+cvc4_add_cxx_unit_test_black(cardinality_public util)
+cvc4_add_cxx_unit_test_white(check_white util)
+cvc4_add_cxx_unit_test_black(configuration_black util)
+cvc4_add_cxx_unit_test_black(datatype_black util)
+cvc4_add_cxx_unit_test_black(exception_black util)
 if(CVC4_USE_SYMFPU)
-cvc4_add_unit_test_black(floatingpoint_black util)
+cvc4_add_cxx_unit_test_black(floatingpoint_black util)
 endif()
-cvc4_add_unit_test_black(integer_black util)
-cvc4_add_unit_test_white(integer_white util)
-cvc4_add_unit_test_black(output_black util)
-cvc4_add_unit_test_black(rational_black util)
-cvc4_add_unit_test_white(rational_white util)
+cvc4_add_cxx_unit_test_black(integer_black util)
+cvc4_add_cxx_unit_test_white(integer_white util)
+cvc4_add_cxx_unit_test_black(output_black util)
+cvc4_add_cxx_unit_test_black(rational_black util)
+cvc4_add_cxx_unit_test_white(rational_white util)
 if(CVC4_USE_POLY_IMP)
-cvc4_add_unit_test_black(real_algebraic_number_black util)
+cvc4_add_cxx_unit_test_black(real_algebraic_number_black util)
 endif()
-cvc4_add_unit_test_black(stats_black util)
+cvc4_add_cxx_unit_test_black(stats_black util)