1 files changed, 19 insertions, 0 deletions
diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 66a35a1af..0f6e2759c 100644
--- 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");