Check constructor is used in APPLY_CONSTRUCTOR (#7737)

Fixes cvc5/cvc5-projects#373.

diff --git a/src/theory/datatypes/theory_datatypes_type_rules.cpp b/src/theory/datatypes/theory_datatypes_type_rules.cpp
index 86a11357bfbda66f18da4d4a66c6ad85a9020df4..d3c06d1f3635e6340e1742d7296c975a8387c976 100644 (file)
--- a/src/theory/datatypes/theory_datatypes_type_rules.cpp
+++ b/src/theory/datatypes/theory_datatypes_type_rules.cpp
@@ -36,6 +36,10 @@ TypeNode DatatypeConstructorTypeRule::computeType(NodeManager* nodeManager,
 {
   Assert(n.getKind() == kind::APPLY_CONSTRUCTOR);
   TypeNode consType = n.getOperator().getType(check);
+  if (!consType.isConstructor())
+  {
+    throw TypeCheckingExceptionPrivate(n, "expected constructor to apply");
+  }
   TypeNode t = consType.getConstructorRangeType();
   Assert(t.isDatatype());
   TNode::iterator child_it = n.begin();

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 66a35a1afe1ae4a2fccb153c7f8dcc34b5d0d5cd..0f6e2759cfd77a82a5c8e90ee7bb3d75370cd80e 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -2642,6 +2642,25 @@ TEST_F(TestApiBlackSolver, issue5893)
   ASSERT_NO_FATAL_FAILURE(distinct.getOp());
 }
 
+TEST_F(TestApiBlackSolver, proj_issue373)
+{
+  Sort s1 = d_solver.getRealSort();
+
+  DatatypeConstructorDecl ctor13 = d_solver.mkDatatypeConstructorDecl("_x115");
+  ctor13.addSelector("_x109", s1);
+  Sort s4 = d_solver.declareDatatype("_x86", {ctor13});
+
+  Term t452 = d_solver.mkVar(s1, "_x281");
+  Term bvl = d_solver.mkTerm(d_solver.mkOp(VARIABLE_LIST), {t452});
+  Term acons =
+      d_solver.mkTerm(d_solver.mkOp(APPLY_CONSTRUCTOR),
+                      {s4.getDatatype().getConstructorTerm("_x115"), t452});
+  // type exception
+  ASSERT_THROW(
+      d_solver.mkTerm(d_solver.mkOp(APPLY_CONSTRUCTOR), {bvl, acons, t452}),
+      CVC5ApiException);
+}
+
 TEST_F(TestApiBlackSolver, doubleUseCons)
 {
   DatatypeConstructorDecl ctor1 = d_solver.mkDatatypeConstructorDecl("_x21");