Fix quantifiers dynamic split module for parametric datatypes (#7085)

Fixes #6838.

1 files changed, 7 insertions, 5 deletions

diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index cc2525b78..941b94d23 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -17,9 +17,10 @@
 
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/first_order_model.h"
 #include "options/quantifiers_options.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/term_database.h"
 
 using namespace cvc5::kind;
 
@@ -164,17 +165,18 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e)
       for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
       {
         std::vector<Node> vars;
+        TypeNode dtjtn = dt[j].getSpecializedConstructorType(tn);
+        Assert(dtjtn.getNumChildren() == dt[j].getNumArgs() + 1);
         for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++)
         {
-          TypeNode tns = dt[j][k].getRangeType();
+          TypeNode tns = dtjtn[k];
           Node v = nm->mkBoundVar(tns);
           vars.push_back(v);
         }
         std::vector<Node> bvs_cmb;
         bvs_cmb.insert(bvs_cmb.end(), bvs.begin(), bvs.end());
         bvs_cmb.insert(bvs_cmb.end(), vars.begin(), vars.end());
-        vars.insert(vars.begin(), dt[j].getConstructor());
-        Node c = nm->mkNode(kind::APPLY_CONSTRUCTOR, vars);
+        Node c = datatypes::utils::mkApplyCons(tn, dt, j, vars);
         TNode ct = c;
         Node body = q[1].substitute(svar, ct);
         if (!bvs_cmb.empty())