diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-08-20 21:12:00 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-08-20 21:12:00 +0000 |
| commit | bd45444319c0baa11b530184e3065df3a2d926a2 (patch) | |
| tree | 70d5d0fa224167d9bee1b000eeb27cc43aa56962 | |
| parent | c38e9c2acd9ba85db68f6b52697cac6ddc0595b5 (diff) | |
removing v1l20009.cvc, a datatypes benchmark where the TCC fails (CVC3 and CVC4 differ in the answer), so it doesn't really test anything
| -rw-r--r-- | test/regress/regress0/datatypes/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/v1l20009.cvc | 16 |
2 files changed, 0 insertions, 17 deletions
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index d22679917..377450c3e 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -32,7 +32,6 @@ TESTS = \ typed_v3l20092.cvc \ typed_v5l30069.cvc \ v10l40099.cvc \ - v1l20009.cvc \ v2l40025.cvc \ v3l60006.cvc \ v5l30058.cvc \ diff --git a/test/regress/regress0/datatypes/v1l20009.cvc b/test/regress/regress0/datatypes/v1l20009.cvc deleted file mode 100644 index 64469cbd6..000000000 --- a/test/regress/regress0/datatypes/v1l20009.cvc +++ /dev/null @@ -1,16 +0,0 @@ -% EXPECT: invalid -% EXIT: 10 -DATATYPE - nat = succ(pred : nat) | zero, - list = cons(car : tree, cdr : list) | null, - tree = node(children : list) | leaf(data : nat) -END; - -x1 : nat ; -x2 : list ; -x3 : tree ; - -QUERY - -(NOT ((NOT is_zero(pred(succ(pred(zero))))) - AND (data(x3) = succ(pred(data(leaf(succ(data(car(null)))))))))); |