Add some regressions for bug 438.

(this commit was certified error- and warning-free by the test-and-commit script.)

diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index a3392f0f34343c193d28d2c27bc07ba3e59120b5..58bd6711df72b967920047a32c8476970e33d859 100644 (file)
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -42,10 +42,11 @@ TESTS =     \
        v3l60006.cvc \
        v5l30058.cvc \
        bug286.cvc \
+       bug438.cvc \
+       bug438b.cvc \
        wrong-sel-simp.cvc
 
 FAILING_TESTS = \
-       bug438.cvc \
        datatype-dump.cvc
 
 EXTRA_DIST = $(TESTS)

diff --git a/test/regress/regress0/datatypes/bug438b.cvc b/test/regress/regress0/datatypes/bug438b.cvc
new file mode 100644 (file)
index 0000000..a109409
--- /dev/null
+++ b/test/regress/regress0/datatypes/bug438b.cvc
@@ -0,0 +1,7 @@
+% EXPECT: sat
+% EXIT: 10
+DATATYPE list[T] = cons(car:T, cdr:list[T]) | nil END;
+x : list[REAL];
+ASSERT x = cons(1.0,nil::list[REAL]);
+ASSERT x = cons(1.0,nil::list[REAL])::list[REAL];
+CHECKSAT;