Check arity in Sort::instantiate (#7897)

Fixes cvc5/cvc5-projects#386.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index e2f645340c2f3d6c059445ea36ebb717a496afab..1c795431d8cd3400ce88af5338daaf08d8e63f04 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -1409,6 +1409,9 @@ Sort Sort::instantiate(const std::vector<Sort>& params) const
   CVC5_API_CHECK_SORTS(params);
   CVC5_API_CHECK(isParametricDatatype() || isSortConstructor())
       << "Expected parametric datatype or sort constructor sort.";
+  CVC5_API_CHECK(isSortConstructor()
+                 || d_type->getNumChildren() == params.size() + 1)
+      << "Arity mismatch for instantiated parametric datatype";
   //////// all checks before this line
   std::vector<cvc5::TypeNode> tparams = sortVectorToTypeNodes(params);
   if (d_type->isDatatype())

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 7a04566ddd04120dcfc9d9a22f8b1587fbb9f364..ff7c7cb4223e9031867c54b7bce728bed6fdbd40 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -2996,5 +2996,18 @@ TEST_F(TestApiBlackSolver, proj_issue383)
   ASSERT_THROW(d_solver.getValue(t3), CVC5ApiException);
 }
 
+TEST_F(TestApiBlackSolver, proj_issue386)
+{
+  Sort s1 = d_solver.getBooleanSort();
+  Sort p1 = d_solver.mkParamSort("_p1");
+  Sort p2 = d_solver.mkParamSort("_p2");
+  DatatypeDecl dtdecl = d_solver.mkDatatypeDecl("_x0", {p1, p2});
+  DatatypeConstructorDecl ctordecl = d_solver.mkDatatypeConstructorDecl("_x1");
+  ctordecl.addSelector("_x2", p1);
+  dtdecl.addConstructor(ctordecl);
+  Sort s2 = d_solver.mkDatatypeSort(dtdecl);
+  ASSERT_THROW(s2.instantiate({s1}), CVC5ApiException);
+}
+
 }  // namespace test
 }  // namespace cvc5