From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 10 Jan 2022 22:19:00 +0000 (-0600)
Subject: Check arity in Sort::instantiate (#7897)
X-Git-Tag: cvc5-1.0.0~574
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7e30c1cb975d5c071dface28be38fbe815f695f0;p=cvc5.git

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 e2f645340..1c795431d 100644
--- 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 7a04566dd..ff7c7cb42 100644
--- 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