Add a method for retrieving base of a constant array through API (#4494)

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