From 030cea7270b61225d24c0768613dd73317b8e21d Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 15 Mar 2022 13:47:36 -0500
Subject: [PATCH] Properly guard sort instantiate (#8247)

Fixes cvc5/cvc5-projects#387.

Adds a prefix of that unit test before the first exception.
---
 src/api/cpp/cvc5.cpp                          |  5 +-
 test/unit/api/cpp/CMakeLists.txt              |  1 +
 .../api/cpp/parametric_datatype_black.cpp     | 47 +++++++++++++++++++
 3 files changed, 52 insertions(+), 1 deletion(-)
 create mode 100644 test/unit/api/cpp/parametric_datatype_black.cpp

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index d1e0dc12e..d16dbfa5a 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -1373,9 +1373,12 @@ Sort Sort::instantiate(const std::vector<Sort>& params) const
   CVC5_API_CHECK_DOMAIN_SORTS(params);
   CVC5_API_CHECK(isParametricDatatype() || isSortConstructor())
       << "Expected parametric datatype or sort constructor sort.";
-  CVC5_API_CHECK(isSortConstructor()
+  CVC5_API_CHECK(!isParametricDatatype()
                  || d_type->getNumChildren() == params.size() + 1)
       << "Arity mismatch for instantiated parametric datatype";
+  CVC5_API_CHECK(!isSortConstructor()
+                 || d_type->getSortConstructorArity() == params.size())
+      << "Arity mismatch for instantiated sort constructor";
   //////// all checks before this line
   std::vector<cvc5::TypeNode> tparams = sortVectorToTypeNodes(params);
   if (d_type->isDatatype())
diff --git a/test/unit/api/cpp/CMakeLists.txt b/test/unit/api/cpp/CMakeLists.txt
index c10214803..0125d6962 100644
--- a/test/unit/api/cpp/CMakeLists.txt
+++ b/test/unit/api/cpp/CMakeLists.txt
@@ -16,6 +16,7 @@ cvc5_add_unit_test_black(datatype_api_black api)
 cvc5_add_unit_test_black(grammar_black api)
 cvc5_add_unit_test_black(op_black api)
 cvc5_add_unit_test_white(op_white api)
+cvc5_add_unit_test_black(parametric_datatype_black api)
 cvc5_add_unit_test_black(result_black api)
 cvc5_add_unit_test_black(solver_black api)
 cvc5_add_unit_test_white(solver_white api)
diff --git a/test/unit/api/cpp/parametric_datatype_black.cpp b/test/unit/api/cpp/parametric_datatype_black.cpp
new file mode 100644
index 000000000..6c4bb80e9
--- /dev/null
+++ b/test/unit/api/cpp/parametric_datatype_black.cpp
@@ -0,0 +1,47 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Blackbox tests involving parametric datatypes.
+ */
+
+#include "test_api.h"
+#include "base/configuration.h"
+
+namespace cvc5 {
+
+using namespace api;
+
+namespace test {
+
+class TestApiBlackParametricDatatype : public TestApi
+{
+};
+
+TEST_F(TestApiBlackParametricDatatype, proj_issue387)
+{
+  Sort s1 = d_solver.getBooleanSort();
+
+  Sort u1 = d_solver.mkSortConstructorSort("_x0", 1);
+  Sort u2 = d_solver.mkSortConstructorSort("_x1", 1);
+  Sort p1 = d_solver.mkParamSort("_x4");
+  Sort p2 = d_solver.mkParamSort("_x27");
+  Sort p3 = d_solver.mkParamSort("_x3");
+
+  DatatypeDecl dtdecl1 = d_solver.mkDatatypeDecl("_x0", p1);
+  DatatypeConstructorDecl ctordecl1 =
+      d_solver.mkDatatypeConstructorDecl("_x18");
+  ASSERT_THROW(ctordecl1.addSelector("_x17", u2.instantiate({p1, p1})),
+               CVC5ApiException);
+}
+
+}  // namespace test
+}  // namespace cvc5
-- 
2.30.2