From 12f88ad664c24ee522643073dcddf144854ca1ef Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 12 Dec 2018 23:19:30 +0000
Subject: [PATCH] API: Add simple empty/sigma regexp unit tests (#2746)

---
 test/unit/api/solver_black.h | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

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()));
+}
-- 
2.30.2