using namespace CVC4::api;
-TEST_F(TestApi, mkDatatypeSort)
+class TestApiDatatypeBlack : public TestApi
+{
+};
+
+TEST_F(TestApiDatatypeBlack, mkDatatypeSort)
{
DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
ASSERT_NO_THROW(nilConstr.getConstructorTerm());
}
-TEST_F(TestApi, mkDatatypeSorts)
+TEST_F(TestApiDatatypeBlack, mkDatatypeSorts)
{
/* Create two mutual datatypes corresponding to this definition
* block:
EXPECT_THROW(d_solver.mkDatatypeSorts(dtdeclsBad), CVC4ApiException);
}
-TEST_F(TestApi, datatypeStructs)
+TEST_F(TestApiDatatypeBlack, datatypeStructs)
{
Sort intSort = d_solver.getIntegerSort();
Sort boolSort = d_solver.getBooleanSort();
EXPECT_TRUE(dtRecord.isWellFounded());
}
-TEST_F(TestApi, datatypeNames)
+TEST_F(TestApiDatatypeBlack, datatypeNames)
{
Sort intSort = d_solver.getIntegerSort();
ASSERT_THROW(DatatypeDecl().getName(), CVC4ApiException);
}
-TEST_F(TestApi, parametricDatatype)
+TEST_F(TestApiDatatypeBlack, parametricDatatype)
{
std::vector<Sort> v;
Sort t1 = d_solver.mkParamSort("T1");
EXPECT_TRUE(pairIntInt.isSubsortOf(pairIntInt));
}
-TEST_F(TestApi, datatypeSimplyRec)
+TEST_F(TestApiDatatypeBlack, datatypeSimplyRec)
{
/* Create mutual datatypes corresponding to this definition block:
*
EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
}
-TEST_F(TestApi, datatypeSpecializedCons)
+TEST_F(TestApiDatatypeBlack, datatypeSpecializedCons)
{
/* Create mutual datatypes corresponding to this definition block:
* DATATYPE