Bug fixes and refactoring of parametric datatypes, add some regressions.

3 files changed, 28 insertions, 1 deletions

diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 8631a4f32..a8a637377 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -69,7 +69,9 @@ TESTS =	\
 	sc-cdt1.smt2  \
 	conqueue-dt-enum-iloop.smt2 \
 	coda_simp_model.smt2 \
-	Test1-tup-mp.cvc
+	Test1-tup-mp.cvc \
+	dt-param-card4-unsat.smt2 \
+	dt-param-card4-bool-sat.smt2
 
 FAILING_TESTS = \
 	datatype-dump.cvc
diff --git a/test/regress/regress0/datatypes/dt-param-card4-bool-sat.smt2 b/test/regress/regress0/datatypes/dt-param-card4-bool-sat.smt2
new file mode 100644
index 000000000..ca5791ce2
--- /dev/null
+++ b/test/regress/regress0/datatypes/dt-param-card4-bool-sat.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status sat)
+(declare-datatypes (T S) ( (Pair (pair (first T) (second S)) ) ) )
+
+(declare-fun p1 () (Pair Bool Bool))
+(declare-fun p2 () (Pair Bool Bool))
+(declare-fun p3 () (Pair Bool Bool))
+(declare-fun p4 () (Pair Bool Bool))
+
+(assert (distinct p1 p2 p3 p4))
+(check-sat)
diff --git a/test/regress/regress0/datatypes/dt-param-card4-unsat.smt2 b/test/regress/regress0/datatypes/dt-param-card4-unsat.smt2
new file mode 100644
index 000000000..9676745b4
--- /dev/null
+++ b/test/regress/regress0/datatypes/dt-param-card4-unsat.smt2
@@ -0,0 +1,14 @@
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-datatypes (T S) ( (Pair (pair (first T) (second S)) ) ) )
+
+(declare-datatypes () ((Color (red) (blue))))
+
+(declare-fun p1 () (Pair Color Color))
+(declare-fun p2 () (Pair Color Color))
+(declare-fun p3 () (Pair Color Color))
+(declare-fun p4 () (Pair Color Color))
+(declare-fun p5 () (Pair Color Color))
+
+(assert (distinct p1 p2 p3 p4 p5))
+(check-sat)