From 7e30c1cb975d5c071dface28be38fbe815f695f0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 10 Jan 2022 16:19:00 -0600 Subject: [PATCH] Check arity in Sort::instantiate (#7897) Fixes cvc5/cvc5-projects#386. --- src/api/cpp/cvc5.cpp | 3 +++ test/unit/api/cpp/solver_black.cpp | 13 +++++++++++++ 2 files changed, 16 insertions(+) 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& 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 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 -- 2.30.2