From a0cce22b009afac40122c01a57404c94db241ea6 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 30 Nov 2012 15:29:36 +0000 Subject: [PATCH] Add some regressions for bug 438. (this commit was certified error- and warning-free by the test-and-commit script.) --- test/regress/regress0/datatypes/Makefile.am | 3 ++- test/regress/regress0/datatypes/bug438b.cvc | 7 +++++++ 2 files changed, 9 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/datatypes/bug438b.cvc 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; -- 2.30.2