From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 30 Nov 2012 15:29:36 +0000 (+0000)
Subject: Add some regressions for bug 438.
X-Git-Tag: cvc5-1.0.0~7521
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a0cce22b009afac40122c01a57404c94db241ea6;p=cvc5.git

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 a3392f0f3..58bd6711d 100644
--- 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
index 000000000..a10940928
--- /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;