Use consistent names for fixtures in unit tests. (#5863)

diff --git a/test/unit/api/datatype_api_black.cpp b/test/unit/api/datatype_api_black.cpp
index 85831697149f26e20e8eb6615ef0b566f3d1bd06..f72bcd1c38908667bf43fa6861333ad41a267d97 100644 (file)
--- a/test/unit/api/datatype_api_black.cpp
+++ b/test/unit/api/datatype_api_black.cpp
@@ -22,11 +22,11 @@ using namespace api;
 
 namespace test {
 
-class TestApiDatatypeBlack : public TestApi
+class TestApiBlackDatatype : public TestApi
 {
 };
 
-TEST_F(TestApiDatatypeBlack, mkDatatypeSort)
+TEST_F(TestApiBlackDatatype, mkDatatypeSort)
 {
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
   DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
@@ -43,7 +43,7 @@ TEST_F(TestApiDatatypeBlack, mkDatatypeSort)
   ASSERT_NO_THROW(nilConstr.getConstructorTerm());
 }
 
-TEST_F(TestApiDatatypeBlack, mkDatatypeSorts)
+TEST_F(TestApiBlackDatatype, mkDatatypeSorts)
 {
   /* Create two mutual datatypes corresponding to this definition
    * block:
@@ -108,7 +108,7 @@ TEST_F(TestApiDatatypeBlack, mkDatatypeSorts)
   ASSERT_THROW(d_solver.mkDatatypeSorts(dtdeclsBad), CVC4ApiException);
 }
 
-TEST_F(TestApiDatatypeBlack, datatypeStructs)
+TEST_F(TestApiBlackDatatype, datatypeStructs)
 {
   Sort intSort = d_solver.getIntegerSort();
   Sort boolSort = d_solver.getBooleanSort();
@@ -182,7 +182,7 @@ TEST_F(TestApiDatatypeBlack, datatypeStructs)
   ASSERT_TRUE(dtRecord.isWellFounded());
 }
 
-TEST_F(TestApiDatatypeBlack, datatypeNames)
+TEST_F(TestApiBlackDatatype, datatypeNames)
 {
   Sort intSort = d_solver.getIntegerSort();
 
@@ -219,7 +219,7 @@ TEST_F(TestApiDatatypeBlack, datatypeNames)
   ASSERT_THROW(DatatypeDecl().getName(), CVC4ApiException);
 }
 
-TEST_F(TestApiDatatypeBlack, parametricDatatype)
+TEST_F(TestApiBlackDatatype, parametricDatatype)
 {
   std::vector<Sort> v;
   Sort t1 = d_solver.mkParamSort("T1");
@@ -297,7 +297,7 @@ TEST_F(TestApiDatatypeBlack, parametricDatatype)
   ASSERT_TRUE(pairIntInt.isSubsortOf(pairIntInt));
 }
 
-TEST_F(TestApiDatatypeBlack, datatypeSimplyRec)
+TEST_F(TestApiBlackDatatype, datatypeSimplyRec)
 {
   /* Create mutual datatypes corresponding to this definition block:
    *
@@ -496,7 +496,7 @@ TEST_F(TestApiDatatypeBlack, datatypeSimplyRec)
   ASSERT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
 }
 
-TEST_F(TestApiDatatypeBlack, datatypeSpecializedCons)
+TEST_F(TestApiBlackDatatype, datatypeSpecializedCons)
 {
   /* Create mutual datatypes corresponding to this definition block:
    *   DATATYPE

diff --git a/test/unit/api/grammar_black.cpp b/test/unit/api/grammar_black.cpp
index c87406a87768574c24cf861a9b7c46abebc33b2b..406d145ab20013aadc22023f3750539b755d6d37 100644 (file)
--- a/test/unit/api/grammar_black.cpp
+++ b/test/unit/api/grammar_black.cpp
@@ -22,11 +22,11 @@ using namespace api;
 
 namespace test {
 
-class TestApiGrammarBlack : public TestApi
+class TestApiBlackGrammar : public TestApi
 {
 };
 
-TEST_F(TestApiGrammarBlack, addRule)
+TEST_F(TestApiBlackGrammar, addRule)
 {
   Sort boolean = d_solver.getBooleanSort();
   Sort integer = d_solver.getIntegerSort();
@@ -50,7 +50,7 @@ TEST_F(TestApiGrammarBlack, addRule)
   ASSERT_THROW(g.addRule(start, d_solver.mkBoolean(false)), CVC4ApiException);
 }
 
-TEST_F(TestApiGrammarBlack, addRules)
+TEST_F(TestApiBlackGrammar, addRules)
 {
   Sort boolean = d_solver.getBooleanSort();
   Sort integer = d_solver.getIntegerSort();
@@ -75,7 +75,7 @@ TEST_F(TestApiGrammarBlack, addRules)
                CVC4ApiException);
 }
 
-TEST_F(TestApiGrammarBlack, addAnyConstant)
+TEST_F(TestApiBlackGrammar, addAnyConstant)
 {
   Sort boolean = d_solver.getBooleanSort();
 
@@ -96,7 +96,7 @@ TEST_F(TestApiGrammarBlack, addAnyConstant)
   ASSERT_THROW(g.addAnyConstant(start), CVC4ApiException);
 }
 
-TEST_F(TestApiGrammarBlack, addAnyVariable)
+TEST_F(TestApiBlackGrammar, addAnyVariable)
 {
   Sort boolean = d_solver.getBooleanSort();
 

diff --git a/test/unit/api/op_black.cpp b/test/unit/api/op_black.cpp
index 817662d67353fb67a95d2545ac91cded21abb4e0..19bd4bb03e900c2d3b03e22c6437d3a19d77cd24 100644 (file)
--- a/test/unit/api/op_black.cpp
+++ b/test/unit/api/op_black.cpp
@@ -20,18 +20,18 @@ using namespace api;
 
 namespace test {
 
-class TestApiOpBlack : public TestApi
+class TestApiBlackOp : public TestApi
 {
 };
 
-TEST_F(TestApiOpBlack, getKind)
+TEST_F(TestApiBlackOp, getKind)
 {
   Op x;
   x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1);
   ASSERT_NO_THROW(x.getKind());
 }
 
-TEST_F(TestApiOpBlack, isNull)
+TEST_F(TestApiBlackOp, isNull)
 {
   Op x;
   ASSERT_TRUE(x.isNull());
@@ -39,7 +39,7 @@ TEST_F(TestApiOpBlack, isNull)
   ASSERT_FALSE(x.isNull());
 }
 
-TEST_F(TestApiOpBlack, opFromKind)
+TEST_F(TestApiBlackOp, opFromKind)
 {
   Op plus(&d_solver, PLUS);
   ASSERT_FALSE(plus.isIndexed());
@@ -50,7 +50,7 @@ TEST_F(TestApiOpBlack, opFromKind)
   ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT), CVC4ApiException);
 }
 
-TEST_F(TestApiOpBlack, getIndicesString)
+TEST_F(TestApiBlackOp, getIndicesString)
 {
   Op x;
   ASSERT_THROW(x.getIndices<std::string>(), CVC4ApiException);
@@ -66,7 +66,7 @@ TEST_F(TestApiOpBlack, getIndicesString)
   ASSERT_THROW(record_update_ot.getIndices<uint32_t>(), CVC4ApiException);
 }
 
-TEST_F(TestApiOpBlack, getIndicesUint)
+TEST_F(TestApiBlackOp, getIndicesUint)
 {
   Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5);
   ASSERT_TRUE(bitvector_repeat_ot.isIndexed());
@@ -116,7 +116,7 @@ TEST_F(TestApiOpBlack, getIndicesUint)
   ASSERT_THROW(tuple_update_ot.getIndices<std::string>(), CVC4ApiException);
 }
 
-TEST_F(TestApiOpBlack, getIndicesPairUint)
+TEST_F(TestApiBlackOp, getIndicesPairUint)
 {
   Op bitvector_extract_ot = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0);
   ASSERT_TRUE(bitvector_extract_ot.isIndexed());
@@ -175,7 +175,7 @@ TEST_F(TestApiOpBlack, getIndicesPairUint)
                CVC4ApiException);
 }
 
-TEST_F(TestApiOpBlack, opScopingToString)
+TEST_F(TestApiBlackOp, opScopingToString)
 {
   Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5);
   std::string op_repr = bitvector_repeat_ot.toString();

diff --git a/test/unit/api/result_black.cpp b/test/unit/api/result_black.cpp
index 52cb68b253a45368dbb6ae2ba829aa8219b142df..887be8fe0e3ad30c5be536b964b388ce08bbea08 100644 (file)
--- a/test/unit/api/result_black.cpp
+++ b/test/unit/api/result_black.cpp
@@ -20,11 +20,11 @@ using namespace api;
 
 namespace test {
 
-class TestApiResultBlack : public TestApi
+class TestApiBlackResult : public TestApi
 {
 };
 
-TEST_F(TestApiResultBlack, isNull)
+TEST_F(TestApiBlackResult, isNull)
 {
   CVC4::api::Result res_null;
   ASSERT_TRUE(res_null.isNull());
@@ -41,7 +41,7 @@ TEST_F(TestApiResultBlack, isNull)
   ASSERT_FALSE(res.isNull());
 }
 
-TEST_F(TestApiResultBlack, eq)
+TEST_F(TestApiBlackResult, eq)
 {
   Sort u_sort = d_solver.mkUninterpretedSort("u");
   Term x = d_solver.mkVar(u_sort, "x");
@@ -54,7 +54,7 @@ TEST_F(TestApiResultBlack, eq)
   ASSERT_EQ(res3, res2);
 }
 
-TEST_F(TestApiResultBlack, isSat)
+TEST_F(TestApiBlackResult, isSat)
 {
   Sort u_sort = d_solver.mkUninterpretedSort("u");
   Term x = d_solver.mkVar(u_sort, "x");
@@ -64,7 +64,7 @@ TEST_F(TestApiResultBlack, isSat)
   ASSERT_FALSE(res.isSatUnknown());
 }
 
-TEST_F(TestApiResultBlack, isUnsat)
+TEST_F(TestApiBlackResult, isUnsat)
 {
   Sort u_sort = d_solver.mkUninterpretedSort("u");
   Term x = d_solver.mkVar(u_sort, "x");
@@ -74,7 +74,7 @@ TEST_F(TestApiResultBlack, isUnsat)
   ASSERT_FALSE(res.isSatUnknown());
 }
 
-TEST_F(TestApiResultBlack, isSatUnknown)
+TEST_F(TestApiBlackResult, isSatUnknown)
 {
   d_solver.setLogic("QF_NIA");
   d_solver.setOption("incremental", "false");
@@ -87,7 +87,7 @@ TEST_F(TestApiResultBlack, isSatUnknown)
   ASSERT_TRUE(res.isSatUnknown());
 }
 
-TEST_F(TestApiResultBlack, isEntailed)
+TEST_F(TestApiBlackResult, isEntailed)
 {
   d_solver.setOption("incremental", "true");
   Sort u_sort = d_solver.mkUninterpretedSort("u");
@@ -104,7 +104,7 @@ TEST_F(TestApiResultBlack, isEntailed)
   ASSERT_FALSE(not_entailed.isEntailmentUnknown());
 }
 
-TEST_F(TestApiResultBlack, isEntailmentUnknown)
+TEST_F(TestApiBlackResult, isEntailmentUnknown)
 {
   d_solver.setLogic("QF_NIA");
   d_solver.setOption("incremental", "false");

diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 82a176498f1daca31f21f0804b8976b2e862e985..2e285fcc7fca6e3e88835b7a5137a27dbb24da05 100644 (file)
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -23,11 +23,11 @@ using namespace api;
 
 namespace test {
 
-class TestApiSolverBlack : public TestApi
+class TestApiBlackSolver : public TestApi
 {
 };
 
-TEST_F(TestApiSolverBlack, recoverableException)
+TEST_F(TestApiBlackSolver, recoverableException)
 {
   d_solver.setOption("produce-models", "true");
   Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
@@ -35,7 +35,7 @@ TEST_F(TestApiSolverBlack, recoverableException)
   ASSERT_THROW(d_solver.getValue(x), CVC4ApiRecoverableException);
 }
 
-TEST_F(TestApiSolverBlack, supportsFloatingPoint)
+TEST_F(TestApiBlackSolver, supportsFloatingPoint)
 {
   if (d_solver.supportsFloatingPoint())
   {
@@ -48,37 +48,37 @@ TEST_F(TestApiSolverBlack, supportsFloatingPoint)
   }
 }
 
-TEST_F(TestApiSolverBlack, getBooleanSort)
+TEST_F(TestApiBlackSolver, getBooleanSort)
 {
   ASSERT_NO_THROW(d_solver.getBooleanSort());
 }
 
-TEST_F(TestApiSolverBlack, getIntegerSort)
+TEST_F(TestApiBlackSolver, getIntegerSort)
 {
   ASSERT_NO_THROW(d_solver.getIntegerSort());
 }
 
-TEST_F(TestApiSolverBlack, getNullSort)
+TEST_F(TestApiBlackSolver, getNullSort)
 {
   ASSERT_NO_THROW(d_solver.getNullSort());
 }
 
-TEST_F(TestApiSolverBlack, getRealSort)
+TEST_F(TestApiBlackSolver, getRealSort)
 {
   ASSERT_NO_THROW(d_solver.getRealSort());
 }
 
-TEST_F(TestApiSolverBlack, getRegExpSort)
+TEST_F(TestApiBlackSolver, getRegExpSort)
 {
   ASSERT_NO_THROW(d_solver.getRegExpSort());
 }
 
-TEST_F(TestApiSolverBlack, getStringSort)
+TEST_F(TestApiBlackSolver, getStringSort)
 {
   ASSERT_NO_THROW(d_solver.getStringSort());
 }
 
-TEST_F(TestApiSolverBlack, getRoundingModeSort)
+TEST_F(TestApiBlackSolver, getRoundingModeSort)
 {
   if (d_solver.supportsFloatingPoint())
   {
@@ -90,7 +90,7 @@ TEST_F(TestApiSolverBlack, getRoundingModeSort)
   }
 }
 
-TEST_F(TestApiSolverBlack, mkArraySort)
+TEST_F(TestApiBlackSolver, mkArraySort)
 {
   Sort boolSort = d_solver.getBooleanSort();
   Sort intSort = d_solver.getIntegerSort();
@@ -114,13 +114,13 @@ TEST_F(TestApiSolverBlack, mkArraySort)
   ASSERT_THROW(slv.mkArraySort(boolSort, boolSort), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, mkBitVectorSort)
+TEST_F(TestApiBlackSolver, mkBitVectorSort)
 {
   ASSERT_NO_THROW(d_solver.mkBitVectorSort(32));
   ASSERT_THROW(d_solver.mkBitVectorSort(0), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, mkFloatingPointSort)
+TEST_F(TestApiBlackSolver, mkFloatingPointSort)
 {
   if (d_solver.supportsFloatingPoint())
   {
@@ -134,7 +134,7 @@ TEST_F(TestApiSolverBlack, mkFloatingPointSort)
   }
 }
 
-TEST_F(TestApiSolverBlack, mkDatatypeSort)
+TEST_F(TestApiBlackSolver, mkDatatypeSort)
 {
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
   DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
@@ -151,7 +151,7 @@ TEST_F(TestApiSolverBlack, mkDatatypeSort)
   ASSERT_THROW(d_solver.mkDatatypeSort(throwsDtypeSpec), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, mkDatatypeSorts)
+TEST_F(TestApiBlackSolver, mkDatatypeSorts)
 {
   Solver slv;
 
@@ -194,7 +194,7 @@ TEST_F(TestApiSolverBlack, mkDatatypeSorts)
   /* Note: More tests are in datatype_api_black. */
 }
 
-TEST_F(TestApiSolverBlack, mkFunctionSort)
+TEST_F(TestApiBlackSolver, mkFunctionSort)
 {
   ASSERT_NO_THROW(d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
                                           d_solver.getIntegerSort()));
@@ -236,13 +236,13 @@ TEST_F(TestApiSolverBlack, mkFunctionSort)
                CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, mkParamSort)
+TEST_F(TestApiBlackSolver, mkParamSort)
 {
   ASSERT_NO_THROW(d_solver.mkParamSort("T"));
   ASSERT_NO_THROW(d_solver.mkParamSort(""));
 }
 
-TEST_F(TestApiSolverBlack, mkPredicateSort)
+TEST_F(TestApiBlackSolver, mkPredicateSort)
 {
   ASSERT_NO_THROW(d_solver.mkPredicateSort({d_solver.getIntegerSort()}));
   ASSERT_THROW(d_solver.mkPredicateSort({}), CVC4ApiException);
@@ -256,7 +256,7 @@ TEST_F(TestApiSolverBlack, mkPredicateSort)
                CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, mkRecordSort)
+TEST_F(TestApiBlackSolver, mkRecordSort)
 {
   std::vector<std::pair<std::string, Sort>> fields = {
       std::make_pair("b", d_solver.getBooleanSort()),
@@ -272,7 +272,7 @@ TEST_F(TestApiSolverBlack, mkRecordSort)
   ASSERT_THROW(slv.mkRecordSort(fields), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, mkSetSort)
+TEST_F(TestApiBlackSolver, mkSetSort)
 {
   ASSERT_NO_THROW(d_solver.mkSetSort(d_solver.getBooleanSort()));
   ASSERT_NO_THROW(d_solver.mkSetSort(d_solver.getIntegerSort()));
@@ -281,7 +281,7 @@ TEST_F(TestApiSolverBlack, mkSetSort)
   ASSERT_THROW(slv.mkSetSort(d_solver.mkBitVectorSort(4)), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, mkBagSort)
+TEST_F(TestApiBlackSolver, mkBagSort)
 {
   ASSERT_NO_THROW(d_solver.mkBagSort(d_solver.getBooleanSort()));
   ASSERT_NO_THROW(d_solver.mkBagSort(d_solver.getIntegerSort()));
@@ -290,7 +290,7 @@ TEST_F(TestApiSolverBlack, mkBagSort)
   ASSERT_THROW(slv.mkBagSort(d_solver.mkBitVectorSort(4)), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, mkSequenceSort)
+TEST_F(TestApiBlackSolver, mkSequenceSort)
 {
   ASSERT_NO_THROW(d_solver.mkSequenceSort(d_solver.getBooleanSort()));
   ASSERT_NO_THROW(d_solver.mkSequenceSort(
@@ -299,20 +299,20 @@ TEST_F(TestApiSolverBlack, mkSequenceSort)
   ASSERT_THROW(slv.mkSequenceSort(d_solver.getIntegerSort()), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, mkUninterpretedSort)
+TEST_F(TestApiBlackSolver, mkUninterpretedSort)
 {
   ASSERT_NO_THROW(d_solver.mkUninterpretedSort("u"));
   ASSERT_NO_THROW(d_solver.mkUninterpretedSort(""));
 }
 
-TEST_F(TestApiSolverBlack, mkSortConstructorSort)
+TEST_F(TestApiBlackSolver, mkSortConstructorSort)
 {
   ASSERT_NO_THROW(d_solver.mkSortConstructorSort("s", 2));
   ASSERT_NO_THROW(d_solver.mkSortConstructorSort("", 2));
   ASSERT_THROW(d_solver.mkSortConstructorSort("", 0), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, mkTupleSort)
+TEST_F(TestApiBlackSolver, mkTupleSort)
 {
   ASSERT_NO_THROW(d_solver.mkTupleSort({d_solver.getIntegerSort()}));
   Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
@@ -324,7 +324,7 @@ TEST_F(TestApiSolverBlack, mkTupleSort)
   ASSERT_THROW(slv.mkTupleSort({d_solver.getIntegerSort()}), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, mkBitVector)
+TEST_F(TestApiBlackSolver, mkBitVector)
 {
   uint32_t size0 = 0, size1 = 8, size2 = 32, val1 = 2;
   uint64_t val2 = 2;
@@ -351,7 +351,7 @@ TEST_F(TestApiSolverBlack, mkBitVector)
             d_solver.mkBitVector(8, "FF", 16));
 }
 
-TEST_F(TestApiSolverBlack, mkVar)
+TEST_F(TestApiBlackSolver, mkVar)
 {
   Sort boolSort = d_solver.getBooleanSort();
   Sort intSort = d_solver.getIntegerSort();
@@ -366,13 +366,13 @@ TEST_F(TestApiSolverBlack, mkVar)
   ASSERT_THROW(slv.mkVar(boolSort, "x"), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, mkBoolean)
+TEST_F(TestApiBlackSolver, mkBoolean)
 {
   ASSERT_NO_THROW(d_solver.mkBoolean(true));
   ASSERT_NO_THROW(d_solver.mkBoolean(false));
 }
 
-TEST_F(TestApiSolverBlack, mkRoundingMode)
+TEST_F(TestApiBlackSolver, mkRoundingMode)
 {
   if (CVC4::Configuration::isBuiltWithSymFPU())
   {
@@ -385,7 +385,7 @@ TEST_F(TestApiSolverBlack, mkRoundingMode)
   }
 }
 
-TEST_F(TestApiSolverBlack, mkUninterpretedConst)
+TEST_F(TestApiBlackSolver, mkUninterpretedConst)
 {
   ASSERT_NO_THROW(d_solver.mkUninterpretedConst(d_solver.getBooleanSort(), 1));
   ASSERT_THROW(d_solver.mkUninterpretedConst(Sort(), 1), CVC4ApiException);
@@ -394,7 +394,7 @@ TEST_F(TestApiSolverBlack, mkUninterpretedConst)
                CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, mkAbstractValue)
+TEST_F(TestApiBlackSolver, mkAbstractValue)
 {
   ASSERT_NO_THROW(d_solver.mkAbstractValue(std::string("1")));
   ASSERT_THROW(d_solver.mkAbstractValue(std::string("0")), CVC4ApiException);
@@ -412,7 +412,7 @@ TEST_F(TestApiSolverBlack, mkAbstractValue)
   ASSERT_THROW(d_solver.mkAbstractValue(0), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, mkFloatingPoint)
+TEST_F(TestApiBlackSolver, mkFloatingPoint)
 {
   Term t1 = d_solver.mkBitVector(8);
   Term t2 = d_solver.mkBitVector(4);
@@ -438,7 +438,7 @@ TEST_F(TestApiSolverBlack, mkFloatingPoint)
   }
 }
 
-TEST_F(TestApiSolverBlack, mkEmptySet)
+TEST_F(TestApiBlackSolver, mkEmptySet)
 {
   Solver slv;
   Sort s = d_solver.mkSetSort(d_solver.getBooleanSort());
@@ -449,7 +449,7 @@ TEST_F(TestApiSolverBlack, mkEmptySet)
   ASSERT_THROW(slv.mkEmptySet(s), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, mkEmptyBag)
+TEST_F(TestApiBlackSolver, mkEmptyBag)
 {
   Solver slv;
   Sort s = d_solver.mkBagSort(d_solver.getBooleanSort());
@@ -460,7 +460,7 @@ TEST_F(TestApiSolverBlack, mkEmptyBag)
   ASSERT_THROW(slv.mkEmptyBag(s), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, mkEmptySequence)
+TEST_F(TestApiBlackSolver, mkEmptySequence)
 {
   Solver slv;
   Sort s = d_solver.mkSequenceSort(d_solver.getBooleanSort());
@@ -469,13 +469,13 @@ TEST_F(TestApiSolverBlack, mkEmptySequence)
   ASSERT_THROW(slv.mkEmptySequence(s), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, mkFalse)
+TEST_F(TestApiBlackSolver, mkFalse)
 {
   ASSERT_NO_THROW(d_solver.mkFalse());
   ASSERT_NO_THROW(d_solver.mkFalse());
 }
 
-TEST_F(TestApiSolverBlack, mkNaN)
+TEST_F(TestApiBlackSolver, mkNaN)
 {
   if (CVC4::Configuration::isBuiltWithSymFPU())
   {
@@ -487,7 +487,7 @@ TEST_F(TestApiSolverBlack, mkNaN)
   }
 }
 
-TEST_F(TestApiSolverBlack, mkNegZero)
+TEST_F(TestApiBlackSolver, mkNegZero)
 {
   if (CVC4::Configuration::isBuiltWithSymFPU())
   {
@@ -499,7 +499,7 @@ TEST_F(TestApiSolverBlack, mkNegZero)
   }
 }
 
-TEST_F(TestApiSolverBlack, mkNegInf)
+TEST_F(TestApiBlackSolver, mkNegInf)
 {
   if (CVC4::Configuration::isBuiltWithSymFPU())
   {
@@ -511,7 +511,7 @@ TEST_F(TestApiSolverBlack, mkNegInf)
   }
 }
 
-TEST_F(TestApiSolverBlack, mkPosInf)
+TEST_F(TestApiBlackSolver, mkPosInf)
 {
   if (CVC4::Configuration::isBuiltWithSymFPU())
   {
@@ -523,7 +523,7 @@ TEST_F(TestApiSolverBlack, mkPosInf)
   }
 }
 
-TEST_F(TestApiSolverBlack, mkPosZero)
+TEST_F(TestApiBlackSolver, mkPosZero)
 {
   if (CVC4::Configuration::isBuiltWithSymFPU())
   {
@@ -535,7 +535,7 @@ TEST_F(TestApiSolverBlack, mkPosZero)
   }
 }
 
-TEST_F(TestApiSolverBlack, mkOp)
+TEST_F(TestApiBlackSolver, mkOp)
 {
   // mkOp(Kind kind, Kind k)
   ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, EQUAL), CVC4ApiException);
@@ -556,9 +556,9 @@ TEST_F(TestApiSolverBlack, mkOp)
   ASSERT_THROW(d_solver.mkOp(DIVISIBLE, 1, 2), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, mkPi) { ASSERT_NO_THROW(d_solver.mkPi()); }
+TEST_F(TestApiBlackSolver, mkPi) { ASSERT_NO_THROW(d_solver.mkPi()); }
 
-TEST_F(TestApiSolverBlack, mkInteger)
+TEST_F(TestApiBlackSolver, mkInteger)
 {
   ASSERT_NO_THROW(d_solver.mkInteger("123"));
   ASSERT_THROW(d_solver.mkInteger("1.23"), CVC4ApiException);
@@ -599,7 +599,7 @@ TEST_F(TestApiSolverBlack, mkInteger)
   ASSERT_NO_THROW(d_solver.mkInteger(val4));
 }
 
-TEST_F(TestApiSolverBlack, mkReal)
+TEST_F(TestApiBlackSolver, mkReal)
 {
   ASSERT_NO_THROW(d_solver.mkReal("123"));
   ASSERT_NO_THROW(d_solver.mkReal("1.23"));
@@ -644,7 +644,7 @@ TEST_F(TestApiSolverBlack, mkReal)
   ASSERT_NO_THROW(d_solver.mkReal(val4, val4));
 }
 
-TEST_F(TestApiSolverBlack, mkRegexpEmpty)
+TEST_F(TestApiBlackSolver, mkRegexpEmpty)
 {
   Sort strSort = d_solver.getStringSort();
   Term s = d_solver.mkConst(strSort, "s");
@@ -652,7 +652,7 @@ TEST_F(TestApiSolverBlack, mkRegexpEmpty)
       d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpEmpty()));
 }
 
-TEST_F(TestApiSolverBlack, mkRegexpSigma)
+TEST_F(TestApiBlackSolver, mkRegexpSigma)
 {
   Sort strSort = d_solver.getStringSort();
   Term s = d_solver.mkConst(strSort, "s");
@@ -660,7 +660,7 @@ TEST_F(TestApiSolverBlack, mkRegexpSigma)
       d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma()));
 }
 
-TEST_F(TestApiSolverBlack, mkSepNil)
+TEST_F(TestApiBlackSolver, mkSepNil)
 {
   ASSERT_NO_THROW(d_solver.mkSepNil(d_solver.getBooleanSort()));
   ASSERT_THROW(d_solver.mkSepNil(Sort()), CVC4ApiException);
@@ -668,7 +668,7 @@ TEST_F(TestApiSolverBlack, mkSepNil)
   ASSERT_THROW(slv.mkSepNil(d_solver.getIntegerSort()), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, mkString)
+TEST_F(TestApiBlackSolver, mkString)
 {
   ASSERT_NO_THROW(d_solver.mkString(""));
   ASSERT_NO_THROW(d_solver.mkString("asdfasdf"));
@@ -678,7 +678,7 @@ TEST_F(TestApiSolverBlack, mkString)
             "\"asdf\\u{5c}nasdf\"");
 }
 
-TEST_F(TestApiSolverBlack, mkChar)
+TEST_F(TestApiBlackSolver, mkChar)
 {
   ASSERT_NO_THROW(d_solver.mkChar(std::string("0123")));
   ASSERT_NO_THROW(d_solver.mkChar("aA"));
@@ -688,7 +688,7 @@ TEST_F(TestApiSolverBlack, mkChar)
   ASSERT_EQ(d_solver.mkChar("abc"), d_solver.mkChar("ABC"));
 }
 
-TEST_F(TestApiSolverBlack, mkTerm)
+TEST_F(TestApiBlackSolver, mkTerm)
 {
   Sort bv32 = d_solver.mkBitVectorSort(32);
   Term a = d_solver.mkConst(bv32, "a");
@@ -745,7 +745,7 @@ TEST_F(TestApiSolverBlack, mkTerm)
   ASSERT_THROW(d_solver.mkTerm(DISTINCT, v6), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, mkTermFromOp)
+TEST_F(TestApiBlackSolver, mkTermFromOp)
 {
   Sort bv32 = d_solver.mkBitVectorSort(32);
   Term a = d_solver.mkConst(bv32, "a");
@@ -843,13 +843,13 @@ TEST_F(TestApiSolverBlack, mkTermFromOp)
   ASSERT_THROW(slv.mkTerm(opterm2, v4), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, mkTrue)
+TEST_F(TestApiBlackSolver, mkTrue)
 {
   ASSERT_NO_THROW(d_solver.mkTrue());
   ASSERT_NO_THROW(d_solver.mkTrue());
 }
 
-TEST_F(TestApiSolverBlack, mkTuple)
+TEST_F(TestApiBlackSolver, mkTuple)
 {
   ASSERT_NO_THROW(d_solver.mkTuple({d_solver.mkBitVectorSort(3)},
                                    {d_solver.mkBitVector("101", 2)}));
@@ -873,7 +873,7 @@ TEST_F(TestApiSolverBlack, mkTuple)
       CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, mkUniverseSet)
+TEST_F(TestApiBlackSolver, mkUniverseSet)
 {
   ASSERT_NO_THROW(d_solver.mkUniverseSet(d_solver.getBooleanSort()));
   ASSERT_THROW(d_solver.mkUniverseSet(Sort()), CVC4ApiException);
@@ -881,7 +881,7 @@ TEST_F(TestApiSolverBlack, mkUniverseSet)
   ASSERT_THROW(slv.mkUniverseSet(d_solver.getBooleanSort()), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, mkConst)
+TEST_F(TestApiBlackSolver, mkConst)
 {
   Sort boolSort = d_solver.getBooleanSort();
   Sort intSort = d_solver.getIntegerSort();
@@ -899,7 +899,7 @@ TEST_F(TestApiSolverBlack, mkConst)
   ASSERT_THROW(slv.mkConst(boolSort), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, mkConstArray)
+TEST_F(TestApiBlackSolver, mkConstArray)
 {
   Sort intSort = d_solver.getIntegerSort();
   Sort arrSort = d_solver.mkArraySort(intSort, intSort);
@@ -919,7 +919,7 @@ TEST_F(TestApiSolverBlack, mkConstArray)
   ASSERT_THROW(slv.mkConstArray(arrSort, zero2), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, declareDatatype)
+TEST_F(TestApiBlackSolver, declareDatatype)
 {
   DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   std::vector<DatatypeConstructorDecl> ctors1 = {nil};
@@ -941,7 +941,7 @@ TEST_F(TestApiSolverBlack, declareDatatype)
   ASSERT_THROW(slv.declareDatatype(std::string("a"), ctors1), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, declareFun)
+TEST_F(TestApiBlackSolver, declareFun)
 {
   Sort bvSort = d_solver.mkBitVectorSort(32);
   Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
@@ -958,14 +958,14 @@ TEST_F(TestApiSolverBlack, declareFun)
   ASSERT_THROW(slv.declareFun("f1", {}, bvSort), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, declareSort)
+TEST_F(TestApiBlackSolver, declareSort)
 {
   ASSERT_NO_THROW(d_solver.declareSort("s", 0));
   ASSERT_NO_THROW(d_solver.declareSort("s", 2));
   ASSERT_NO_THROW(d_solver.declareSort("", 2));
 }
 
-TEST_F(TestApiSolverBlack, defineSort)
+TEST_F(TestApiBlackSolver, defineSort)
 {
   Sort sortVar0 = d_solver.mkParamSort("T0");
   Sort sortVar1 = d_solver.mkParamSort("T1");
@@ -978,7 +978,7 @@ TEST_F(TestApiSolverBlack, defineSort)
   ASSERT_NO_THROW(arraySort1.substitute({sortVar0, sortVar1}, {intSort, realSort}));
 }
 
-TEST_F(TestApiSolverBlack, defineFun)
+TEST_F(TestApiBlackSolver, defineFun)
 {
   Sort bvSort = d_solver.mkBitVectorSort(32);
   Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
@@ -1024,7 +1024,7 @@ TEST_F(TestApiSolverBlack, defineFun)
   ASSERT_THROW(slv.defineFun("ff", {b12, b22}, bvSort2, v1), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, defineFunGlobal)
+TEST_F(TestApiBlackSolver, defineFunGlobal)
 {
   Sort bSort = d_solver.getBooleanSort();
   Sort fSort = d_solver.mkFunctionSort(bSort, bSort);
@@ -1048,7 +1048,7 @@ TEST_F(TestApiSolverBlack, defineFunGlobal)
   ASSERT_TRUE(d_solver.checkSat().isUnsat());
 }
 
-TEST_F(TestApiSolverBlack, defineFunRec)
+TEST_F(TestApiBlackSolver, defineFunRec)
 {
   Sort bvSort = d_solver.mkBitVectorSort(32);
   Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
@@ -1100,7 +1100,7 @@ TEST_F(TestApiSolverBlack, defineFunRec)
                CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, defineFunRecWrongLogic)
+TEST_F(TestApiBlackSolver, defineFunRecWrongLogic)
 {
   d_solver.setLogic("QF_BV");
   Sort bvSort = d_solver.mkBitVectorSort(32);
@@ -1112,7 +1112,7 @@ TEST_F(TestApiSolverBlack, defineFunRecWrongLogic)
   ASSERT_THROW(d_solver.defineFunRec(f, {b, b}, v), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, defineFunRecGlobal)
+TEST_F(TestApiBlackSolver, defineFunRecGlobal)
 {
   Sort bSort = d_solver.getBooleanSort();
   Sort fSort = d_solver.mkFunctionSort(bSort, bSort);
@@ -1137,7 +1137,7 @@ TEST_F(TestApiSolverBlack, defineFunRecGlobal)
   ASSERT_TRUE(d_solver.checkSat().isUnsat());
 }
 
-TEST_F(TestApiSolverBlack, defineFunsRec)
+TEST_F(TestApiBlackSolver, defineFunsRec)
 {
   Sort uSort = d_solver.mkUninterpretedSort("u");
   Sort bvSort = d_solver.mkBitVectorSort(32);
@@ -1198,7 +1198,7 @@ TEST_F(TestApiSolverBlack, defineFunsRec)
                CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, defineFunsRecWrongLogic)
+TEST_F(TestApiBlackSolver, defineFunsRecWrongLogic)
 {
   d_solver.setLogic("QF_BV");
   Sort uSort = d_solver.mkUninterpretedSort("u");
@@ -1215,7 +1215,7 @@ TEST_F(TestApiSolverBlack, defineFunsRecWrongLogic)
                CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, defineFunsRecGlobal)
+TEST_F(TestApiBlackSolver, defineFunsRecGlobal)
 {
   Sort bSort = d_solver.getBooleanSort();
   Sort fSort = d_solver.mkFunctionSort(bSort, bSort);
@@ -1236,7 +1236,7 @@ TEST_F(TestApiSolverBlack, defineFunsRecGlobal)
   ASSERT_TRUE(d_solver.checkSat().isUnsat());
 }
 
-TEST_F(TestApiSolverBlack, uFIteration)
+TEST_F(TestApiBlackSolver, uFIteration)
 {
   Sort intSort = d_solver.getIntegerSort();
   Sort funSort = d_solver.mkFunctionSort({intSort, intSort}, intSort);
@@ -1256,13 +1256,13 @@ TEST_F(TestApiSolverBlack, uFIteration)
   }
 }
 
-TEST_F(TestApiSolverBlack, getInfo)
+TEST_F(TestApiBlackSolver, getInfo)
 {
   ASSERT_NO_THROW(d_solver.getInfo("name"));
   ASSERT_THROW(d_solver.getInfo("asdf"), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, getInterpolant)
+TEST_F(TestApiBlackSolver, getInterpolant)
 {
   d_solver.setOption("produce-interpols", "default");
   d_solver.setOption("incremental", "false");
@@ -1290,7 +1290,7 @@ TEST_F(TestApiSolverBlack, getInterpolant)
   ASSERT_TRUE(output.getSort().isBoolean());
 }
 
-TEST_F(TestApiSolverBlack, getOp)
+TEST_F(TestApiBlackSolver, getOp)
 {
   Sort bv32 = d_solver.mkBitVectorSort(32);
   Term a = d_solver.mkConst(bv32, "a");
@@ -1332,13 +1332,13 @@ TEST_F(TestApiSolverBlack, getOp)
   ASSERT_EQ(listhead.getOp(), Op(&d_solver, APPLY_SELECTOR));
 }
 
-TEST_F(TestApiSolverBlack, getOption)
+TEST_F(TestApiBlackSolver, getOption)
 {
   ASSERT_NO_THROW(d_solver.getOption("incremental"));
   ASSERT_THROW(d_solver.getOption("asdf"), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, getUnsatAssumptions1)
+TEST_F(TestApiBlackSolver, getUnsatAssumptions1)
 {
 #if IS_PROOFS_BUILD
   d_solver.setOption("incremental", "false");
@@ -1347,7 +1347,7 @@ TEST_F(TestApiSolverBlack, getUnsatAssumptions1)
 #endif
 }
 
-TEST_F(TestApiSolverBlack, getUnsatAssumptions2)
+TEST_F(TestApiBlackSolver, getUnsatAssumptions2)
 {
 #if IS_PROOFS_BUILD
   d_solver.setOption("incremental", "true");
@@ -1357,7 +1357,7 @@ TEST_F(TestApiSolverBlack, getUnsatAssumptions2)
 #endif
 }
 
-TEST_F(TestApiSolverBlack, getUnsatAssumptions3)
+TEST_F(TestApiBlackSolver, getUnsatAssumptions3)
 {
 #if IS_PROOFS_BUILD
   d_solver.setOption("incremental", "true");
@@ -1369,7 +1369,7 @@ TEST_F(TestApiSolverBlack, getUnsatAssumptions3)
 #endif
 }
 
-TEST_F(TestApiSolverBlack, getUnsatCore1)
+TEST_F(TestApiBlackSolver, getUnsatCore1)
 {
 #if IS_PROOFS_BUILD
   d_solver.setOption("incremental", "false");
@@ -1379,7 +1379,7 @@ TEST_F(TestApiSolverBlack, getUnsatCore1)
 #endif
 }
 
-TEST_F(TestApiSolverBlack, getUnsatCore2)
+TEST_F(TestApiBlackSolver, getUnsatCore2)
 {
 #if IS_PROOFS_BUILD
   d_solver.setOption("incremental", "false");
@@ -1390,7 +1390,7 @@ TEST_F(TestApiSolverBlack, getUnsatCore2)
 #endif
 }
 
-TEST_F(TestApiSolverBlack, getUnsatCore3)
+TEST_F(TestApiBlackSolver, getUnsatCore3)
 {
 #if IS_PROOFS_BUILD
   d_solver.setOption("incremental", "true");
@@ -1433,7 +1433,7 @@ TEST_F(TestApiSolverBlack, getUnsatCore3)
 #endif
 }
 
-TEST_F(TestApiSolverBlack, getValue1)
+TEST_F(TestApiBlackSolver, getValue1)
 {
   d_solver.setOption("produce-models", "false");
   Term t = d_solver.mkTrue();
@@ -1442,7 +1442,7 @@ TEST_F(TestApiSolverBlack, getValue1)
   ASSERT_THROW(d_solver.getValue(t), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, getValue2)
+TEST_F(TestApiBlackSolver, getValue2)
 {
   d_solver.setOption("produce-models", "true");
   Term t = d_solver.mkFalse();
@@ -1451,7 +1451,7 @@ TEST_F(TestApiSolverBlack, getValue2)
   ASSERT_THROW(d_solver.getValue(t), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, getValue3)
+TEST_F(TestApiBlackSolver, getValue3)
 {
   d_solver.setOption("produce-models", "true");
   Sort uSort = d_solver.mkUninterpretedSort("u");
@@ -1490,7 +1490,7 @@ TEST_F(TestApiSolverBlack, getValue3)
   ASSERT_THROW(slv.getValue(x), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, getQuantifierElimination)
+TEST_F(TestApiBlackSolver, getQuantifierElimination)
 {
   Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x");
   Term forall =
@@ -1503,7 +1503,7 @@ TEST_F(TestApiSolverBlack, getQuantifierElimination)
   ASSERT_NO_THROW(d_solver.getQuantifierElimination(forall));
 }
 
-TEST_F(TestApiSolverBlack, getQuantifierEliminationDisjunct)
+TEST_F(TestApiBlackSolver, getQuantifierEliminationDisjunct)
 {
   Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x");
   Term forall =
@@ -1518,7 +1518,7 @@ TEST_F(TestApiSolverBlack, getQuantifierEliminationDisjunct)
   ASSERT_NO_THROW(d_solver.getQuantifierEliminationDisjunct(forall));
 }
 
-TEST_F(TestApiSolverBlack, declareSeparationHeap)
+TEST_F(TestApiBlackSolver, declareSeparationHeap)
 {
   d_solver.setLogic("ALL_SUPPORTED");
   Sort integer = d_solver.getIntegerSort();
@@ -1548,7 +1548,7 @@ void checkSimpleSeparationConstraints(Solver* solver)
 }
 }  // namespace
 
-TEST_F(TestApiSolverBlack, getSeparationHeapTerm1)
+TEST_F(TestApiBlackSolver, getSeparationHeapTerm1)
 {
   d_solver.setLogic("QF_BV");
   d_solver.setOption("incremental", "false");
@@ -1558,7 +1558,7 @@ TEST_F(TestApiSolverBlack, getSeparationHeapTerm1)
   ASSERT_THROW(d_solver.getSeparationHeap(), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, getSeparationHeapTerm2)
+TEST_F(TestApiBlackSolver, getSeparationHeapTerm2)
 {
   d_solver.setLogic("ALL_SUPPORTED");
   d_solver.setOption("incremental", "false");
@@ -1567,7 +1567,7 @@ TEST_F(TestApiSolverBlack, getSeparationHeapTerm2)
   ASSERT_THROW(d_solver.getSeparationHeap(), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, getSeparationHeapTerm3)
+TEST_F(TestApiBlackSolver, getSeparationHeapTerm3)
 {
   d_solver.setLogic("ALL_SUPPORTED");
   d_solver.setOption("incremental", "false");
@@ -1578,7 +1578,7 @@ TEST_F(TestApiSolverBlack, getSeparationHeapTerm3)
   ASSERT_THROW(d_solver.getSeparationHeap(), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, getSeparationHeapTerm4)
+TEST_F(TestApiBlackSolver, getSeparationHeapTerm4)
 {
   d_solver.setLogic("ALL_SUPPORTED");
   d_solver.setOption("incremental", "false");
@@ -1589,7 +1589,7 @@ TEST_F(TestApiSolverBlack, getSeparationHeapTerm4)
   ASSERT_THROW(d_solver.getSeparationHeap(), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, getSeparationHeapTerm5)
+TEST_F(TestApiBlackSolver, getSeparationHeapTerm5)
 {
   d_solver.setLogic("ALL_SUPPORTED");
   d_solver.setOption("incremental", "false");
@@ -1598,7 +1598,7 @@ TEST_F(TestApiSolverBlack, getSeparationHeapTerm5)
   ASSERT_NO_THROW(d_solver.getSeparationHeap());
 }
 
-TEST_F(TestApiSolverBlack, getSeparationNilTerm1)
+TEST_F(TestApiBlackSolver, getSeparationNilTerm1)
 {
   d_solver.setLogic("QF_BV");
   d_solver.setOption("incremental", "false");
@@ -1608,7 +1608,7 @@ TEST_F(TestApiSolverBlack, getSeparationNilTerm1)
   ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, getSeparationNilTerm2)
+TEST_F(TestApiBlackSolver, getSeparationNilTerm2)
 {
   d_solver.setLogic("ALL_SUPPORTED");
   d_solver.setOption("incremental", "false");
@@ -1617,7 +1617,7 @@ TEST_F(TestApiSolverBlack, getSeparationNilTerm2)
   ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, getSeparationNilTerm3)
+TEST_F(TestApiBlackSolver, getSeparationNilTerm3)
 {
   d_solver.setLogic("ALL_SUPPORTED");
   d_solver.setOption("incremental", "false");
@@ -1628,7 +1628,7 @@ TEST_F(TestApiSolverBlack, getSeparationNilTerm3)
   ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, getSeparationNilTerm4)
+TEST_F(TestApiBlackSolver, getSeparationNilTerm4)
 {
   d_solver.setLogic("ALL_SUPPORTED");
   d_solver.setOption("incremental", "false");
@@ -1639,7 +1639,7 @@ TEST_F(TestApiSolverBlack, getSeparationNilTerm4)
   ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, getSeparationNilTerm5)
+TEST_F(TestApiBlackSolver, getSeparationNilTerm5)
 {
   d_solver.setLogic("ALL_SUPPORTED");
   d_solver.setOption("incremental", "false");
@@ -1648,7 +1648,7 @@ TEST_F(TestApiSolverBlack, getSeparationNilTerm5)
   ASSERT_NO_THROW(d_solver.getSeparationNilTerm());
 }
 
-TEST_F(TestApiSolverBlack, push1)
+TEST_F(TestApiBlackSolver, push1)
 {
   d_solver.setOption("incremental", "true");
   ASSERT_NO_THROW(d_solver.push(1));
@@ -1656,25 +1656,25 @@ TEST_F(TestApiSolverBlack, push1)
   ASSERT_THROW(d_solver.setOption("incremental", "true"), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, push2)
+TEST_F(TestApiBlackSolver, push2)
 {
   d_solver.setOption("incremental", "false");
   ASSERT_THROW(d_solver.push(1), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, pop1)
+TEST_F(TestApiBlackSolver, pop1)
 {
   d_solver.setOption("incremental", "false");
   ASSERT_THROW(d_solver.pop(1), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, pop2)
+TEST_F(TestApiBlackSolver, pop2)
 {
   d_solver.setOption("incremental", "true");
   ASSERT_THROW(d_solver.pop(1), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, pop3)
+TEST_F(TestApiBlackSolver, pop3)
 {
   d_solver.setOption("incremental", "true");
   ASSERT_NO_THROW(d_solver.push(1));
@@ -1682,7 +1682,7 @@ TEST_F(TestApiSolverBlack, pop3)
   ASSERT_THROW(d_solver.pop(1), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, blockModel1)
+TEST_F(TestApiBlackSolver, blockModel1)
 {
   d_solver.setOption("produce-models", "true");
   Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
@@ -1691,7 +1691,7 @@ TEST_F(TestApiSolverBlack, blockModel1)
   ASSERT_THROW(d_solver.blockModel(), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, blockModel2)
+TEST_F(TestApiBlackSolver, blockModel2)
 {
   d_solver.setOption("block-models", "literals");
   Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
@@ -1700,7 +1700,7 @@ TEST_F(TestApiSolverBlack, blockModel2)
   ASSERT_THROW(d_solver.blockModel(), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, blockModel3)
+TEST_F(TestApiBlackSolver, blockModel3)
 {
   d_solver.setOption("produce-models", "true");
   d_solver.setOption("block-models", "literals");
@@ -1709,7 +1709,7 @@ TEST_F(TestApiSolverBlack, blockModel3)
   ASSERT_THROW(d_solver.blockModel(), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, blockModel4)
+TEST_F(TestApiBlackSolver, blockModel4)
 {
   d_solver.setOption("produce-models", "true");
   d_solver.setOption("block-models", "literals");
@@ -1719,7 +1719,7 @@ TEST_F(TestApiSolverBlack, blockModel4)
   ASSERT_NO_THROW(d_solver.blockModel());
 }
 
-TEST_F(TestApiSolverBlack, blockModelValues1)
+TEST_F(TestApiBlackSolver, blockModelValues1)
 {
   d_solver.setOption("produce-models", "true");
   d_solver.setOption("block-models", "literals");
@@ -1732,7 +1732,7 @@ TEST_F(TestApiSolverBlack, blockModelValues1)
                CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, blockModelValues2)
+TEST_F(TestApiBlackSolver, blockModelValues2)
 {
   d_solver.setOption("produce-models", "true");
   Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
@@ -1741,7 +1741,7 @@ TEST_F(TestApiSolverBlack, blockModelValues2)
   ASSERT_THROW(d_solver.blockModelValues({x}), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, blockModelValues3)
+TEST_F(TestApiBlackSolver, blockModelValues3)
 {
   d_solver.setOption("block-models", "literals");
   Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
@@ -1750,7 +1750,7 @@ TEST_F(TestApiSolverBlack, blockModelValues3)
   ASSERT_THROW(d_solver.blockModelValues({x}), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, blockModelValues4)
+TEST_F(TestApiBlackSolver, blockModelValues4)
 {
   d_solver.setOption("produce-models", "true");
   d_solver.setOption("block-models", "literals");
@@ -1759,7 +1759,7 @@ TEST_F(TestApiSolverBlack, blockModelValues4)
   ASSERT_THROW(d_solver.blockModelValues({x}), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, blockModelValues5)
+TEST_F(TestApiBlackSolver, blockModelValues5)
 {
   d_solver.setOption("produce-models", "true");
   d_solver.setOption("block-models", "literals");
@@ -1769,7 +1769,7 @@ TEST_F(TestApiSolverBlack, blockModelValues5)
   ASSERT_NO_THROW(d_solver.blockModelValues({x}));
 }
 
-TEST_F(TestApiSolverBlack, setInfo)
+TEST_F(TestApiBlackSolver, setInfo)
 {
   ASSERT_THROW(d_solver.setInfo("cvc4-lagic", "QF_BV"), CVC4ApiException);
   ASSERT_THROW(d_solver.setInfo("cvc2-logic", "QF_BV"), CVC4ApiException);
@@ -1795,7 +1795,7 @@ TEST_F(TestApiSolverBlack, setInfo)
   ASSERT_THROW(d_solver.setInfo("status", "asdf"), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, simplify)
+TEST_F(TestApiBlackSolver, simplify)
 {
   ASSERT_THROW(d_solver.simplify(Term()), CVC4ApiException);
 
@@ -1870,7 +1870,7 @@ TEST_F(TestApiSolverBlack, simplify)
   ASSERT_NO_THROW(d_solver.simplify(f2));
 }
 
-TEST_F(TestApiSolverBlack, assertFormula)
+TEST_F(TestApiBlackSolver, assertFormula)
 {
   ASSERT_NO_THROW(d_solver.assertFormula(d_solver.mkTrue()));
   ASSERT_THROW(d_solver.assertFormula(Term()), CVC4ApiException);
@@ -1878,7 +1878,7 @@ TEST_F(TestApiSolverBlack, assertFormula)
   ASSERT_THROW(slv.assertFormula(d_solver.mkTrue()), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, checkEntailed)
+TEST_F(TestApiBlackSolver, checkEntailed)
 {
   d_solver.setOption("incremental", "false");
   ASSERT_NO_THROW(d_solver.checkEntailed(d_solver.mkTrue()));
@@ -1887,7 +1887,7 @@ TEST_F(TestApiSolverBlack, checkEntailed)
   ASSERT_THROW(slv.checkEntailed(d_solver.mkTrue()), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, checkEntailed1)
+TEST_F(TestApiBlackSolver, checkEntailed1)
 {
   Sort boolSort = d_solver.getBooleanSort();
   Term x = d_solver.mkConst(boolSort, "x");
@@ -1902,7 +1902,7 @@ TEST_F(TestApiSolverBlack, checkEntailed1)
   ASSERT_THROW(slv.checkEntailed(d_solver.mkTrue()), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, checkEntailed2)
+TEST_F(TestApiBlackSolver, checkEntailed2)
 {
   d_solver.setOption("incremental", "true");
 
@@ -1951,14 +1951,14 @@ TEST_F(TestApiSolverBlack, checkEntailed2)
   ASSERT_THROW(slv.checkEntailed(d_solver.mkTrue()), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, checkSat)
+TEST_F(TestApiBlackSolver, checkSat)
 {
   d_solver.setOption("incremental", "false");
   ASSERT_NO_THROW(d_solver.checkSat());
   ASSERT_THROW(d_solver.checkSat(), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, checkSatAssuming)
+TEST_F(TestApiBlackSolver, checkSatAssuming)
 {
   d_solver.setOption("incremental", "false");
   ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTrue()));
@@ -1967,7 +1967,7 @@ TEST_F(TestApiSolverBlack, checkSatAssuming)
   ASSERT_THROW(slv.checkSatAssuming(d_solver.mkTrue()), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, checkSatAssuming1)
+TEST_F(TestApiBlackSolver, checkSatAssuming1)
 {
   Sort boolSort = d_solver.getBooleanSort();
   Term x = d_solver.mkConst(boolSort, "x");
@@ -1982,7 +1982,7 @@ TEST_F(TestApiSolverBlack, checkSatAssuming1)
   ASSERT_THROW(slv.checkSatAssuming(d_solver.mkTrue()), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, checkSatAssuming2)
+TEST_F(TestApiBlackSolver, checkSatAssuming2)
 {
   d_solver.setOption("incremental", "true");
 
@@ -2031,7 +2031,7 @@ TEST_F(TestApiSolverBlack, checkSatAssuming2)
   ASSERT_THROW(slv.checkSatAssuming(d_solver.mkTrue()), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, setLogic)
+TEST_F(TestApiBlackSolver, setLogic)
 {
   ASSERT_NO_THROW(d_solver.setLogic("AUFLIRA"));
   ASSERT_THROW(d_solver.setLogic("AF_BV"), CVC4ApiException);
@@ -2039,7 +2039,7 @@ TEST_F(TestApiSolverBlack, setLogic)
   ASSERT_THROW(d_solver.setLogic("AUFLIRA"), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, setOption)
+TEST_F(TestApiBlackSolver, setOption)
 {
   ASSERT_NO_THROW(d_solver.setOption("bv-sat-solver", "minisat"));
   ASSERT_THROW(d_solver.setOption("bv-sat-solver", "1"), CVC4ApiException);
@@ -2048,7 +2048,7 @@ TEST_F(TestApiSolverBlack, setOption)
                CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, resetAssertions)
+TEST_F(TestApiBlackSolver, resetAssertions)
 {
   d_solver.setOption("incremental", "true");
 
@@ -2063,7 +2063,7 @@ TEST_F(TestApiSolverBlack, resetAssertions)
   d_solver.checkSatAssuming({slt, ule});
 }
 
-TEST_F(TestApiSolverBlack, mkSygusVar)
+TEST_F(TestApiBlackSolver, mkSygusVar)
 {
   Sort boolSort = d_solver.getBooleanSort();
   Sort intSort = d_solver.getIntegerSort();
@@ -2080,7 +2080,7 @@ TEST_F(TestApiSolverBlack, mkSygusVar)
   ASSERT_THROW(slv.mkSygusVar(boolSort), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, mkSygusGrammar)
+TEST_F(TestApiBlackSolver, mkSygusGrammar)
 {
   Term nullTerm;
   Term boolTerm = d_solver.mkBoolean(true);
@@ -2101,7 +2101,7 @@ TEST_F(TestApiSolverBlack, mkSygusGrammar)
   ASSERT_THROW(slv.mkSygusGrammar({boolVar2}, {intVar}), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, synthFun)
+TEST_F(TestApiBlackSolver, synthFun)
 {
   Sort null = d_solver.getNullSort();
   Sort boolean = d_solver.getBooleanSort();
@@ -2135,7 +2135,7 @@ TEST_F(TestApiSolverBlack, synthFun)
                CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, synthInv)
+TEST_F(TestApiBlackSolver, synthInv)
 {
   Sort boolean = d_solver.getBooleanSort();
   Sort integer = d_solver.getIntegerSort();
@@ -2160,7 +2160,7 @@ TEST_F(TestApiSolverBlack, synthInv)
   ASSERT_THROW(d_solver.synthInv("i4", {x}, g2), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, addSygusConstraint)
+TEST_F(TestApiBlackSolver, addSygusConstraint)
 {
   Term nullTerm;
   Term boolTerm = d_solver.mkBoolean(true);
@@ -2174,7 +2174,7 @@ TEST_F(TestApiSolverBlack, addSygusConstraint)
   ASSERT_THROW(slv.addSygusConstraint(boolTerm), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, addSygusInvConstraint)
+TEST_F(TestApiBlackSolver, addSygusInvConstraint)
 {
   Sort boolean = d_solver.getBooleanSort();
   Sort real = d_solver.getRealSort();
@@ -2244,7 +2244,7 @@ TEST_F(TestApiSolverBlack, addSygusInvConstraint)
                CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, getSynthSolution)
+TEST_F(TestApiBlackSolver, getSynthSolution)
 {
   d_solver.setOption("lang", "sygus2");
   d_solver.setOption("incremental", "false");
@@ -2267,7 +2267,7 @@ TEST_F(TestApiSolverBlack, getSynthSolution)
   ASSERT_THROW(slv.getSynthSolution(f), CVC4ApiException);
 }
 
-TEST_F(TestApiSolverBlack, getSynthSolutions)
+TEST_F(TestApiBlackSolver, getSynthSolutions)
 {
   d_solver.setOption("lang", "sygus2");
   d_solver.setOption("incremental", "false");

diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp
index 16190b76d5a18bd772cdf0cbc03f8cba351220be..747ddb92dac59215974e1228c66f4b9d5a47dbf1 100644 (file)
--- a/test/unit/api/sort_black.cpp
+++ b/test/unit/api/sort_black.cpp
@@ -23,11 +23,11 @@ using namespace api;
 
 namespace test {
 
-class TestApiSortBlack : public TestApi
+class TestApiBlackSort : public TestApi
 {
 };
 
-TEST_F(TestApiSortBlack, getDatatype)
+TEST_F(TestApiBlackSort, getDatatype)
 {
   // create datatype sort, check should not fail
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
@@ -43,7 +43,7 @@ TEST_F(TestApiSortBlack, getDatatype)
   ASSERT_THROW(bvSort.getDatatype(), CVC4ApiException);
 }
 
-TEST_F(TestApiSortBlack, datatypeSorts)
+TEST_F(TestApiBlackSort, datatypeSorts)
 {
   Sort intSort = d_solver.getIntegerSort();
   // create datatype sort to test
@@ -93,7 +93,7 @@ TEST_F(TestApiSortBlack, datatypeSorts)
   ASSERT_THROW(booleanSort.getSelectorCodomainSort(), CVC4ApiException);
 }
 
-TEST_F(TestApiSortBlack, instantiate)
+TEST_F(TestApiBlackSort, instantiate)
 {
   // instantiate parametric datatype, check should not fail
   Sort sort = d_solver.mkParamSort("T");
@@ -120,7 +120,7 @@ TEST_F(TestApiSortBlack, instantiate)
       CVC4ApiException);
 }
 
-TEST_F(TestApiSortBlack, getFunctionArity)
+TEST_F(TestApiBlackSort, getFunctionArity)
 {
   Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
                                          d_solver.getIntegerSort());
@@ -129,7 +129,7 @@ TEST_F(TestApiSortBlack, getFunctionArity)
   ASSERT_THROW(bvSort.getFunctionArity(), CVC4ApiException);
 }
 
-TEST_F(TestApiSortBlack, getFunctionDomainSorts)
+TEST_F(TestApiBlackSort, getFunctionDomainSorts)
 {
   Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
                                          d_solver.getIntegerSort());
@@ -138,7 +138,7 @@ TEST_F(TestApiSortBlack, getFunctionDomainSorts)
   ASSERT_THROW(bvSort.getFunctionDomainSorts(), CVC4ApiException);
 }
 
-TEST_F(TestApiSortBlack, getFunctionCodomainSort)
+TEST_F(TestApiBlackSort, getFunctionCodomainSort)
 {
   Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
                                          d_solver.getIntegerSort());
@@ -147,7 +147,7 @@ TEST_F(TestApiSortBlack, getFunctionCodomainSort)
   ASSERT_THROW(bvSort.getFunctionCodomainSort(), CVC4ApiException);
 }
 
-TEST_F(TestApiSortBlack, getArrayIndexSort)
+TEST_F(TestApiBlackSort, getArrayIndexSort)
 {
   Sort elementSort = d_solver.mkBitVectorSort(32);
   Sort indexSort = d_solver.mkBitVectorSort(32);
@@ -156,7 +156,7 @@ TEST_F(TestApiSortBlack, getArrayIndexSort)
   ASSERT_THROW(indexSort.getArrayIndexSort(), CVC4ApiException);
 }
 
-TEST_F(TestApiSortBlack, getArrayElementSort)
+TEST_F(TestApiBlackSort, getArrayElementSort)
 {
   Sort elementSort = d_solver.mkBitVectorSort(32);
   Sort indexSort = d_solver.mkBitVectorSort(32);
@@ -165,7 +165,7 @@ TEST_F(TestApiSortBlack, getArrayElementSort)
   ASSERT_THROW(indexSort.getArrayElementSort(), CVC4ApiException);
 }
 
-TEST_F(TestApiSortBlack, getSetElementSort)
+TEST_F(TestApiBlackSort, getSetElementSort)
 {
   Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
   ASSERT_NO_THROW(setSort.getSetElementSort());
@@ -175,7 +175,7 @@ TEST_F(TestApiSortBlack, getSetElementSort)
   ASSERT_THROW(bvSort.getSetElementSort(), CVC4ApiException);
 }
 
-TEST_F(TestApiSortBlack, getBagElementSort)
+TEST_F(TestApiBlackSort, getBagElementSort)
 {
   Sort bagSort = d_solver.mkBagSort(d_solver.getIntegerSort());
   ASSERT_NO_THROW(bagSort.getBagElementSort());
@@ -185,7 +185,7 @@ TEST_F(TestApiSortBlack, getBagElementSort)
   ASSERT_THROW(bvSort.getBagElementSort(), CVC4ApiException);
 }
 
-TEST_F(TestApiSortBlack, getSequenceElementSort)
+TEST_F(TestApiBlackSort, getSequenceElementSort)
 {
   Sort seqSort = d_solver.mkSequenceSort(d_solver.getIntegerSort());
   ASSERT_TRUE(seqSort.isSequence());
@@ -195,7 +195,7 @@ TEST_F(TestApiSortBlack, getSequenceElementSort)
   ASSERT_THROW(bvSort.getSequenceElementSort(), CVC4ApiException);
 }
 
-TEST_F(TestApiSortBlack, getUninterpretedSortName)
+TEST_F(TestApiBlackSort, getUninterpretedSortName)
 {
   Sort uSort = d_solver.mkUninterpretedSort("u");
   ASSERT_NO_THROW(uSort.getUninterpretedSortName());
@@ -203,7 +203,7 @@ TEST_F(TestApiSortBlack, getUninterpretedSortName)
   ASSERT_THROW(bvSort.getUninterpretedSortName(), CVC4ApiException);
 }
 
-TEST_F(TestApiSortBlack, isUninterpretedSortParameterized)
+TEST_F(TestApiBlackSort, isUninterpretedSortParameterized)
 {
   Sort uSort = d_solver.mkUninterpretedSort("u");
   ASSERT_FALSE(uSort.isUninterpretedSortParameterized());
@@ -214,7 +214,7 @@ TEST_F(TestApiSortBlack, isUninterpretedSortParameterized)
   ASSERT_THROW(bvSort.isUninterpretedSortParameterized(), CVC4ApiException);
 }
 
-TEST_F(TestApiSortBlack, getUninterpretedSortParamSorts)
+TEST_F(TestApiBlackSort, getUninterpretedSortParamSorts)
 {
   Sort uSort = d_solver.mkUninterpretedSort("u");
   ASSERT_NO_THROW(uSort.getUninterpretedSortParamSorts());
@@ -225,7 +225,7 @@ TEST_F(TestApiSortBlack, getUninterpretedSortParamSorts)
   ASSERT_THROW(bvSort.getUninterpretedSortParamSorts(), CVC4ApiException);
 }
 
-TEST_F(TestApiSortBlack, getUninterpretedSortConstructorName)
+TEST_F(TestApiBlackSort, getUninterpretedSortConstructorName)
 {
   Sort sSort = d_solver.mkSortConstructorSort("s", 2);
   ASSERT_NO_THROW(sSort.getSortConstructorName());
@@ -233,7 +233,7 @@ TEST_F(TestApiSortBlack, getUninterpretedSortConstructorName)
   ASSERT_THROW(bvSort.getSortConstructorName(), CVC4ApiException);
 }
 
-TEST_F(TestApiSortBlack, getUninterpretedSortConstructorArity)
+TEST_F(TestApiBlackSort, getUninterpretedSortConstructorArity)
 {
   Sort sSort = d_solver.mkSortConstructorSort("s", 2);
   ASSERT_NO_THROW(sSort.getSortConstructorArity());
@@ -241,7 +241,7 @@ TEST_F(TestApiSortBlack, getUninterpretedSortConstructorArity)
   ASSERT_THROW(bvSort.getSortConstructorArity(), CVC4ApiException);
 }
 
-TEST_F(TestApiSortBlack, getBVSize)
+TEST_F(TestApiBlackSort, getBVSize)
 {
   Sort bvSort = d_solver.mkBitVectorSort(32);
   ASSERT_NO_THROW(bvSort.getBVSize());
@@ -249,7 +249,7 @@ TEST_F(TestApiSortBlack, getBVSize)
   ASSERT_THROW(setSort.getBVSize(), CVC4ApiException);
 }
 
-TEST_F(TestApiSortBlack, getFPExponentSize)
+TEST_F(TestApiBlackSort, getFPExponentSize)
 {
   if (CVC4::Configuration::isBuiltWithSymFPU())
   {
@@ -260,7 +260,7 @@ TEST_F(TestApiSortBlack, getFPExponentSize)
   }
 }
 
-TEST_F(TestApiSortBlack, getFPSignificandSize)
+TEST_F(TestApiBlackSort, getFPSignificandSize)
 {
   if (CVC4::Configuration::isBuiltWithSymFPU())
   {
@@ -271,7 +271,7 @@ TEST_F(TestApiSortBlack, getFPSignificandSize)
   }
 }
 
-TEST_F(TestApiSortBlack, getDatatypeParamSorts)
+TEST_F(TestApiBlackSort, getDatatypeParamSorts)
 {
   // create parametric datatype, check should not fail
   Sort sort = d_solver.mkParamSort("T");
@@ -295,7 +295,7 @@ TEST_F(TestApiSortBlack, getDatatypeParamSorts)
   ASSERT_THROW(dtypeSort.getDatatypeParamSorts(), CVC4ApiException);
 }
 
-TEST_F(TestApiSortBlack, getDatatypeArity)
+TEST_F(TestApiBlackSort, getDatatypeArity)
 {
   // create datatype sort, check should not fail
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
@@ -311,7 +311,7 @@ TEST_F(TestApiSortBlack, getDatatypeArity)
   ASSERT_THROW(bvSort.getDatatypeArity(), CVC4ApiException);
 }
 
-TEST_F(TestApiSortBlack, getTupleLength)
+TEST_F(TestApiBlackSort, getTupleLength)
 {
   Sort tupleSort = d_solver.mkTupleSort(
       {d_solver.getIntegerSort(), d_solver.getIntegerSort()});
@@ -320,7 +320,7 @@ TEST_F(TestApiSortBlack, getTupleLength)
   ASSERT_THROW(bvSort.getTupleLength(), CVC4ApiException);
 }
 
-TEST_F(TestApiSortBlack, getTupleSorts)
+TEST_F(TestApiBlackSort, getTupleSorts)
 {
   Sort tupleSort = d_solver.mkTupleSort(
       {d_solver.getIntegerSort(), d_solver.getIntegerSort()});
@@ -329,7 +329,7 @@ TEST_F(TestApiSortBlack, getTupleSorts)
   ASSERT_THROW(bvSort.getTupleSorts(), CVC4ApiException);
 }
 
-TEST_F(TestApiSortBlack, sortCompare)
+TEST_F(TestApiBlackSort, sortCompare)
 {
   Sort boolSort = d_solver.getBooleanSort();
   Sort intSort = d_solver.getIntegerSort();
@@ -341,7 +341,7 @@ TEST_F(TestApiSortBlack, sortCompare)
   ASSERT_TRUE((intSort > bvSort || intSort == bvSort) == (intSort >= bvSort));
 }
 
-TEST_F(TestApiSortBlack, sortSubtyping)
+TEST_F(TestApiBlackSort, sortSubtyping)
 {
   Sort intSort = d_solver.getIntegerSort();
   Sort realSort = d_solver.getRealSort();
@@ -365,7 +365,7 @@ TEST_F(TestApiSortBlack, sortSubtyping)
   ASSERT_FALSE(setSortR.isSubsortOf(setSortI));
 }
 
-TEST_F(TestApiSortBlack, sortScopedToString)
+TEST_F(TestApiBlackSort, sortScopedToString)
 {
   std::string name = "uninterp-sort";
   Sort bvsort8 = d_solver.mkBitVectorSort(8);

diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp
index b6f8fc4ed7f779ec846fe50396911b118bfbc991..d437342957638a019657b86b2c2593e5e40cbd0c 100644 (file)
--- a/test/unit/api/term_black.cpp
+++ b/test/unit/api/term_black.cpp
@@ -20,11 +20,11 @@ using namespace api;
 
 namespace test {
 
-class TestApiTermBlack : public TestApi
+class TestApiBlackTerm : public TestApi
 {
 };
 
-TEST_F(TestApiTermBlack, eq)
+TEST_F(TestApiBlackTerm, eq)
 {
   Sort uSort = d_solver.mkUninterpretedSort("u");
   Term x = d_solver.mkVar(uSort, "x");
@@ -39,7 +39,7 @@ TEST_F(TestApiTermBlack, eq)
   ASSERT_TRUE(x != z);
 }
 
-TEST_F(TestApiTermBlack, getId)
+TEST_F(TestApiBlackTerm, getId)
 {
   Term n;
   ASSERT_THROW(n.getId(), CVC4ApiException);
@@ -52,7 +52,7 @@ TEST_F(TestApiTermBlack, getId)
   ASSERT_NE(x.getId(), z.getId());
 }
 
-TEST_F(TestApiTermBlack, getKind)
+TEST_F(TestApiBlackTerm, getKind)
 {
   Sort uSort = d_solver.mkUninterpretedSort("u");
   Sort intSort = d_solver.getIntegerSort();
@@ -94,7 +94,7 @@ TEST_F(TestApiTermBlack, getKind)
   ASSERT_EQ(ss.getKind(), SEQ_CONCAT);
 }
 
-TEST_F(TestApiTermBlack, getSort)
+TEST_F(TestApiBlackTerm, getSort)
 {
   Sort bvSort = d_solver.mkBitVectorSort(8);
   Sort intSort = d_solver.getIntegerSort();
@@ -139,7 +139,7 @@ TEST_F(TestApiTermBlack, getSort)
   ASSERT_EQ(p_f_y.getSort(), boolSort);
 }
 
-TEST_F(TestApiTermBlack, getOp)
+TEST_F(TestApiBlackTerm, getOp)
 {
   Sort intsort = d_solver.getIntegerSort();
   Sort bvsort = d_solver.mkBitVectorSort(8);
@@ -219,7 +219,7 @@ TEST_F(TestApiTermBlack, getOp)
   ASSERT_EQ(headTerm, d_solver.mkTerm(headTerm.getOp(), children));
 }
 
-TEST_F(TestApiTermBlack, isNull)
+TEST_F(TestApiBlackTerm, isNull)
 {
   Term x;
   ASSERT_TRUE(x.isNull());
@@ -227,7 +227,7 @@ TEST_F(TestApiTermBlack, isNull)
   ASSERT_FALSE(x.isNull());
 }
 
-TEST_F(TestApiTermBlack, notTerm)
+TEST_F(TestApiBlackTerm, notTerm)
 {
   Sort bvSort = d_solver.mkBitVectorSort(8);
   Sort intSort = d_solver.getIntegerSort();
@@ -256,7 +256,7 @@ TEST_F(TestApiTermBlack, notTerm)
   ASSERT_NO_THROW(p_f_x.notTerm());
 }
 
-TEST_F(TestApiTermBlack, andTerm)
+TEST_F(TestApiBlackTerm, andTerm)
 {
   Sort bvSort = d_solver.mkBitVectorSort(8);
   Sort intSort = d_solver.getIntegerSort();
@@ -322,7 +322,7 @@ TEST_F(TestApiTermBlack, andTerm)
   ASSERT_NO_THROW(p_f_x.andTerm(p_f_x));
 }
 
-TEST_F(TestApiTermBlack, orTerm)
+TEST_F(TestApiBlackTerm, orTerm)
 {
   Sort bvSort = d_solver.mkBitVectorSort(8);
   Sort intSort = d_solver.getIntegerSort();
@@ -388,7 +388,7 @@ TEST_F(TestApiTermBlack, orTerm)
   ASSERT_NO_THROW(p_f_x.orTerm(p_f_x));
 }
 
-TEST_F(TestApiTermBlack, xorTerm)
+TEST_F(TestApiBlackTerm, xorTerm)
 {
   Sort bvSort = d_solver.mkBitVectorSort(8);
   Sort intSort = d_solver.getIntegerSort();
@@ -454,7 +454,7 @@ TEST_F(TestApiTermBlack, xorTerm)
   ASSERT_NO_THROW(p_f_x.xorTerm(p_f_x));
 }
 
-TEST_F(TestApiTermBlack, eqTerm)
+TEST_F(TestApiBlackTerm, eqTerm)
 {
   Sort bvSort = d_solver.mkBitVectorSort(8);
   Sort intSort = d_solver.getIntegerSort();
@@ -520,7 +520,7 @@ TEST_F(TestApiTermBlack, eqTerm)
   ASSERT_NO_THROW(p_f_x.eqTerm(p_f_x));
 }
 
-TEST_F(TestApiTermBlack, impTerm)
+TEST_F(TestApiBlackTerm, impTerm)
 {
   Sort bvSort = d_solver.mkBitVectorSort(8);
   Sort intSort = d_solver.getIntegerSort();
@@ -586,7 +586,7 @@ TEST_F(TestApiTermBlack, impTerm)
   ASSERT_NO_THROW(p_f_x.impTerm(p_f_x));
 }
 
-TEST_F(TestApiTermBlack, iteTerm)
+TEST_F(TestApiBlackTerm, iteTerm)
 {
   Sort bvSort = d_solver.mkBitVectorSort(8);
   Sort intSort = d_solver.getIntegerSort();
@@ -630,7 +630,7 @@ TEST_F(TestApiTermBlack, iteTerm)
   ASSERT_THROW(p_f_x.iteTerm(x, b), CVC4ApiException);
 }
 
-TEST_F(TestApiTermBlack, termAssignment)
+TEST_F(TestApiBlackTerm, termAssignment)
 {
   Term t1 = d_solver.mkInteger(1);
   Term t2 = t1;
@@ -638,7 +638,7 @@ TEST_F(TestApiTermBlack, termAssignment)
   ASSERT_EQ(t1, d_solver.mkInteger(1));
 }
 
-TEST_F(TestApiTermBlack, termCompare)
+TEST_F(TestApiBlackTerm, termCompare)
 {
   Term t1 = d_solver.mkInteger(1);
   Term t2 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2));
@@ -649,7 +649,7 @@ TEST_F(TestApiTermBlack, termCompare)
   ASSERT_TRUE((t1 > t2 || t1 == t2) == (t1 >= t2));
 }
 
-TEST_F(TestApiTermBlack, termChildren)
+TEST_F(TestApiBlackTerm, termChildren)
 {
   // simple term 2+3
   Term two = d_solver.mkInteger(2);
@@ -671,7 +671,7 @@ TEST_F(TestApiTermBlack, termChildren)
   ASSERT_THROW(tnull[0], CVC4ApiException);
 }
 
-TEST_F(TestApiTermBlack, getInteger)
+TEST_F(TestApiBlackTerm, getInteger)
 {
   Term int1 = d_solver.mkInteger("-18446744073709551616");
   Term int2 = d_solver.mkInteger("-18446744073709551615");
@@ -749,14 +749,14 @@ TEST_F(TestApiTermBlack, getInteger)
   ASSERT_EQ(int11.getInteger(), "18446744073709551616");
 }
 
-TEST_F(TestApiTermBlack, getString)
+TEST_F(TestApiBlackTerm, getString)
 {
   Term s1 = d_solver.mkString("abcde");
   ASSERT_TRUE(s1.isString());
   ASSERT_EQ(s1.getString(), L"abcde");
 }
 
-TEST_F(TestApiTermBlack, substitute)
+TEST_F(TestApiBlackTerm, substitute)
 {
   Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
   Term one = d_solver.mkInteger(1);
@@ -807,7 +807,7 @@ TEST_F(TestApiTermBlack, substitute)
   ASSERT_THROW(xpx.substitute(es, rs), CVC4ApiException);
 }
 
-TEST_F(TestApiTermBlack, constArray)
+TEST_F(TestApiBlackTerm, constArray)
 {
   Sort intsort = d_solver.getIntegerSort();
   Sort arrsort = d_solver.mkArraySort(intsort, intsort);
@@ -830,7 +830,7 @@ TEST_F(TestApiTermBlack, constArray)
       d_solver.mkTerm(STORE, stores, d_solver.mkReal(4), d_solver.mkReal(5));
 }
 
-TEST_F(TestApiTermBlack, constSequenceElements)
+TEST_F(TestApiBlackTerm, constSequenceElements)
 {
   Sort realsort = d_solver.getRealSort();
   Sort seqsort = d_solver.mkSequenceSort(realsort);
@@ -847,7 +847,7 @@ TEST_F(TestApiTermBlack, constSequenceElements)
   ASSERT_THROW(su.getConstSequenceElements(), CVC4ApiException);
 }
 
-TEST_F(TestApiTermBlack, termScopedToString)
+TEST_F(TestApiBlackTerm, termScopedToString)
 {
   Sort intsort = d_solver.getIntegerSort();
   Term x = d_solver.mkConst(intsort, "x");

diff --git a/test/unit/expr/node_black.cpp b/test/unit/expr/node_black.cpp
index 88406f6bc95cc7d7af8e5a0070f8c5b6ae034c32..33576b2cce030e71f0880d0f0bc9ef0ab4678f63 100644 (file)
--- a/test/unit/expr/node_black.cpp
+++ b/test/unit/expr/node_black.cpp
@@ -32,7 +32,7 @@
 
 namespace CVC4 {
 
-using namespace CVC4::kind;
+using namespace kind;
 
 namespace test {
 

diff --git a/test/unit/expr/node_builder_black.cpp b/test/unit/expr/node_builder_black.cpp
index 3ba78950b0e8800bab22702fffd0af4daa99f875..20f907e18a8b592689f56fe365a6a5d34d748186 100644 (file)
--- a/test/unit/expr/node_builder_black.cpp
+++ b/test/unit/expr/node_builder_black.cpp
@@ -32,11 +32,11 @@
 
 namespace CVC4 {
 
-using namespace CVC4::kind;
+using namespace kind;
 
 namespace test {
 
-class TestNodeBuilderBlackNode : public TestNodeBlack
+class TestNodeBlackNodeBuilder : public TestNodeBlack
 {
  protected:
   template <unsigned N>
@@ -51,7 +51,7 @@ class TestNodeBuilderBlackNode : public TestNodeBlack
 };
 
 /** Tests just constructors. No modification is done to the node. */
-TEST_F(TestNodeBuilderBlackNode, ctors)
+TEST_F(TestNodeBlackNodeBuilder, ctors)
 {
   /* Default size tests. */
   NodeBuilder<> def;
@@ -153,13 +153,13 @@ TEST_F(TestNodeBuilderBlackNode, ctors)
 #endif
 }
 
-TEST_F(TestNodeBuilderBlackNode, dtor)
+TEST_F(TestNodeBlackNodeBuilder, dtor)
 {
   NodeBuilder<K>* nb = new NodeBuilder<K>();
   delete nb;
 }
 
-TEST_F(TestNodeBuilderBlackNode, begin_end)
+TEST_F(TestNodeBlackNodeBuilder, begin_end)
 {
   /* Test begin() and end() without resizing. */
   NodeBuilder<K> ws(d_specKind);
@@ -208,7 +208,7 @@ TEST_F(TestNodeBuilderBlackNode, begin_end)
   ASSERT_EQ(smaller_citer, smaller.end());
 }
 
-TEST_F(TestNodeBuilderBlackNode, iterator)
+TEST_F(TestNodeBlackNodeBuilder, iterator)
 {
   NodeBuilder<> b;
   Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode);
@@ -234,7 +234,7 @@ TEST_F(TestNodeBuilderBlackNode, iterator)
   }
 }
 
-TEST_F(TestNodeBuilderBlackNode, getKind)
+TEST_F(TestNodeBlackNodeBuilder, getKind)
 {
   NodeBuilder<> noKind;
   ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND);
@@ -259,7 +259,7 @@ TEST_F(TestNodeBuilderBlackNode, getKind)
   ASSERT_EQ(spec.getKind(), PLUS);
 }
 
-TEST_F(TestNodeBuilderBlackNode, getNumChildren)
+TEST_F(TestNodeBlackNodeBuilder, getNumChildren)
 {
   Node x(d_nodeManager->mkSkolem("x", *d_intTypeNode));
 
@@ -294,7 +294,7 @@ TEST_F(TestNodeBuilderBlackNode, getNumChildren)
 #endif
 }
 
-TEST_F(TestNodeBuilderBlackNode, operator_square)
+TEST_F(TestNodeBlackNodeBuilder, operator_square)
 {
   NodeBuilder<> arr(d_specKind);
 
@@ -343,7 +343,7 @@ TEST_F(TestNodeBuilderBlackNode, operator_square)
 #endif
 }
 
-TEST_F(TestNodeBuilderBlackNode, clear)
+TEST_F(TestNodeBlackNodeBuilder, clear)
 {
   NodeBuilder<> nb;
 
@@ -394,7 +394,7 @@ TEST_F(TestNodeBuilderBlackNode, clear)
 #endif
 }
 
-TEST_F(TestNodeBuilderBlackNode, operator_stream_insertion_kind)
+TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_kind)
 {
 #ifdef CVC4_ASSERTIONS
   NodeBuilder<> spec(d_specKind);
@@ -443,7 +443,7 @@ TEST_F(TestNodeBuilderBlackNode, operator_stream_insertion_kind)
       d_specKind);
 }
 
-TEST_F(TestNodeBuilderBlackNode, operator_stream_insertion_node)
+TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_node)
 {
   NodeBuilder<K> nb(d_specKind);
   ASSERT_EQ(nb.getKind(), d_specKind);
@@ -471,7 +471,7 @@ TEST_F(TestNodeBuilderBlackNode, operator_stream_insertion_node)
   ASSERT_NE(overflow.begin(), overflow.end());
 }
 
-TEST_F(TestNodeBuilderBlackNode, append)
+TEST_F(TestNodeBlackNodeBuilder, append)
 {
   Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode);
   Node y = d_nodeManager->mkSkolem("y", *d_boolTypeNode);
@@ -536,7 +536,7 @@ TEST_F(TestNodeBuilderBlackNode, append)
   ASSERT_EQ(b[8], m);
 }
 
-TEST_F(TestNodeBuilderBlackNode, operator_node_cast)
+TEST_F(TestNodeBlackNodeBuilder, operator_node_cast)
 {
   NodeBuilder<K> implicit(d_specKind);
   NodeBuilder<K> explic(d_specKind);
@@ -558,7 +558,7 @@ TEST_F(TestNodeBuilderBlackNode, operator_node_cast)
 #endif
 }
 
-TEST_F(TestNodeBuilderBlackNode, leftist_building)
+TEST_F(TestNodeBlackNodeBuilder, leftist_building)
 {
   NodeBuilder<> nb;