diff options
| -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; |