API: Add simple empty/sigma regexp unit tests (#2746)

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 538899a0f836e6265f461e14c21e9097ed363202..7527a5c55573414ef2c3f5dc0bf8f1cecfa398e7 100644 (file)
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -36,6 +36,8 @@ class SolverBlack : public CxxTest::TestSuite
   void testDefineFun();
   void testDefineFunRec();
   void testDefineFunsRec();
+  void testMkRegexpEmpty();
+  void testMkRegexpSigma();
 
  private:
   Solver d_solver;
@@ -228,3 +230,19 @@ void SolverBlack::testDefineFunsRec()
       d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}),
       CVC4ApiException&);
 }
+
+void SolverBlack::testMkRegexpEmpty()
+{
+  Sort strSort = d_solver.getStringSort();
+  Term s = d_solver.mkVar("s", strSort);
+  TS_ASSERT_THROWS_NOTHING(
+      d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpEmpty()));
+}
+
+void SolverBlack::testMkRegexpSigma()
+{
+  Sort strSort = d_solver.getStringSort();
+  Term s = d_solver.mkVar("s", strSort);
+  TS_ASSERT_THROWS_NOTHING(
+      d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma()));
+}