removing v1l20009.cvc, a datatypes benchmark where the TCC fails (CVC3 and CVC4 diffe...

diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index d226799171095d62b8ff57c6a183f5438ce1aa0a..377450c3ec2258cab603701d98189dc7d22ee024 100644 (file)
--- 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 (file)
index 64469cb..0000000
--- 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))))))))));