diff options
| -rw-r--r-- | test/unit/api/solver_black.h | 18 |
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())); +} |