1 files changed, 23 insertions, 0 deletions
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index ddff63352..4a7b74c8e 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -46,6 +46,7 @@ class SolverBlack : public CxxTest::TestSuite
   void testMkPredicateSort();
   void testMkRecordSort();
   void testMkSetSort();
+  void testMkSequenceSort();
   void testMkSortConstructorSort();
   void testMkTupleSort();
   void testMkUninterpretedSort();
@@ -56,6 +57,7 @@ class SolverBlack : public CxxTest::TestSuite
   void testMkConst();
   void testMkConstArray();
   void testMkEmptySet();
+  void testMkEmptySequence();
   void testMkFalse();
   void testMkFloatingPoint();
   void testMkNaN();
@@ -388,6 +390,17 @@ void SolverBlack::testMkSetSort()
                    CVC4ApiException&);
 }
 
+void SolverBlack::testMkSequenceSort()
+{
+  TS_ASSERT_THROWS_NOTHING(
+      d_solver->mkSequenceSort(d_solver->getBooleanSort()));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkSequenceSort(
+      d_solver->mkSequenceSort(d_solver->getIntegerSort())));
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkSequenceSort(d_solver->getIntegerSort()),
+                   CVC4ApiException&);
+}
+
 void SolverBlack::testMkUninterpretedSort()
 {
   TS_ASSERT_THROWS_NOTHING(d_solver->mkUninterpretedSort("u"));
@@ -540,6 +553,16 @@ void SolverBlack::testMkEmptySet()
   TS_ASSERT_THROWS(slv.mkEmptySet(s), CVC4ApiException&);
 }
 
+void SolverBlack::testMkEmptySequence()
+{
+  Solver slv;
+  Sort s = d_solver->mkSequenceSort(d_solver->getBooleanSort());
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptySequence(s));
+  TS_ASSERT_THROWS_NOTHING(
+      d_solver->mkEmptySequence(d_solver->getBooleanSort()));
+  TS_ASSERT_THROWS(slv.mkEmptySequence(s), CVC4ApiException&);
+}
+
 void SolverBlack::testMkFalse()
 {
   TS_ASSERT_THROWS_NOTHING(d_solver->mkFalse());