diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-10-20 16:12:55 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-10-20 23:12:55 +0000 |
commit | bef33ceaf0a6b69d76b4fd61cb03c990e86bc41c (patch) | |
tree | 8dac5c6e500c4a6379270de70c3c547b5b0b18d8 /test/unit/api | |
parent | 80cdf28298c9190506f37721492680f432ef635d (diff) |
api: Add Solver::mkSepEmp(). (#7432)
@alex-ozdemir
Diffstat (limited to 'test/unit/api')
-rw-r--r-- | test/unit/api/java/cvc5/SolverTest.java | 7 | ||||
-rw-r--r-- | test/unit/api/solver_black.cpp | 2 |
2 files changed, 8 insertions, 1 deletions
diff --git a/test/unit/api/java/cvc5/SolverTest.java b/test/unit/api/java/cvc5/SolverTest.java index d153b8a91..6f9d8206d 100644 --- a/test/unit/api/java/cvc5/SolverTest.java +++ b/test/unit/api/java/cvc5/SolverTest.java @@ -623,6 +623,11 @@ class SolverTest assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma())); } + @Test void mkSepEmp() + { + assertDoesNotThrow(() -> d_solver.mkSepEmp()); + } + @Test void mkSepNil() { assertDoesNotThrow(() -> d_solver.mkSepNil(d_solver.getBooleanSort())); @@ -2342,4 +2347,4 @@ class SolverTest + "\"Z\")))", projection.toString()); } -}
\ No newline at end of file +} diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index a294ad6ca..c9527c2d4 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -597,6 +597,8 @@ TEST_F(TestApiBlackSolver, mkRegexpSigma) d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma())); } +TEST_F(TestApiBlackSolver, mkSepEmp) { ASSERT_NO_THROW(d_solver.mkSepEmp()); } + TEST_F(TestApiBlackSolver, mkSepNil) { ASSERT_NO_THROW(d_solver.mkSepNil(d_solver.getBooleanSort())); |