From bd45444319c0baa11b530184e3065df3a2d926a2 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 20 Aug 2012 21:12:00 +0000
Subject: [PATCH] removing v1l20009.cvc, a datatypes benchmark where the TCC
 fails (CVC3 and CVC4 differ in the answer), so it doesn't really test
 anything

---
 test/regress/regress0/datatypes/Makefile.am  |  1 -
 test/regress/regress0/datatypes/v1l20009.cvc | 16 ----------------
 2 files changed, 17 deletions(-)
 delete mode 100644 test/regress/regress0/datatypes/v1l20009.cvc

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))))))))));
-- 
2.30.2