diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-11-30 15:29:36 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-11-30 15:29:36 +0000 |
commit | a0cce22b009afac40122c01a57404c94db241ea6 (patch) | |
tree | c8601ddbe53a4d48aae12d1b276337a8568b3b49 /test | |
parent | 03b766ec1f86976d602988581e5e47dbed31952c (diff) |
Add some regressions for bug 438.
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/datatypes/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/datatypes/bug438b.cvc | 7 |
2 files changed, 9 insertions, 1 deletions
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; |