Fix parametric datatype instantiation (#4493)

A bug was introduced when adding the Node-level datatype implementation in d803e7f. The code did not probably get the arity of a sort constructor. This adds TypeNode::getSortConstructorArity and uses it during parametric datatype type resolution.

2 files changed, 14 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 6f948b02b..d5174af5e 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -416,6 +416,7 @@ set(regress_0_tests
   regress0/datatypes/mutually-recursive.cvc
   regress0/datatypes/pair-bool-bool.cvc
   regress0/datatypes/pair-real-bool.smt2
+  regress0/datatypes/parametric-alt-list.cvc
   regress0/datatypes/rec1.cvc
   regress0/datatypes/rec2.cvc
   regress0/datatypes/rec4.cvc
diff --git a/test/regress/regress0/datatypes/parametric-alt-list.cvc b/test/regress/regress0/datatypes/parametric-alt-list.cvc
new file mode 100644
index 000000000..f523272ae
--- /dev/null
+++ b/test/regress/regress0/datatypes/parametric-alt-list.cvc
@@ -0,0 +1,13 @@
+% EXPECT: sat
+DATATYPE
+List[X,Y] = nil | cons (head: X, tail: List[Y,X])
+END;
+
+x : List[INT,STRING]; % = cons(1, nil::List[STRING,INT]);
+y : List[INT,STRING];
+
+ASSERT NOT( x = y );
+
+ASSERT NOT ( x = tail(tail(x)) );
+
+CHECKSAT;