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

1 files changed, 18 insertions, 0 deletions

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 538899a0f..7527a5c55 100644
--- 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()));
+}