diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/api/term_black.h | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h index a3cbd028f..56d13fc63 100644 --- a/test/unit/api/term_black.h +++ b/test/unit/api/term_black.h @@ -43,6 +43,7 @@ class TermBlack : public CxxTest::TestSuite void testTermChildren(); void testSubstitute(); void testIsConst(); + void testConstArray(); private: Solver d_solver; @@ -752,3 +753,19 @@ void TermBlack::testIsConst() Term tnull; TS_ASSERT_THROWS(tnull.isConst(), CVC4ApiException&); } + +void TermBlack::testConstArray() +{ + Sort intsort = d_solver.getIntegerSort(); + Sort arrsort = d_solver.mkArraySort(intsort, intsort); + Term a = d_solver.mkConst(arrsort, "a"); + Term one = d_solver.mkReal(1); + Term constarr = d_solver.mkConstArray(arrsort, one); + + TS_ASSERT(!a.isConst()); + TS_ASSERT(constarr.isConst()); + + TS_ASSERT_EQUALS(constarr.getKind(), CONST_ARRAY); + TS_ASSERT_EQUALS(constarr.getConstArrayBase(), one); + TS_ASSERT_THROWS(a.getConstArrayBase(), CVC4ApiException&); +} |