From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 20 Aug 2012 21:12:00 +0000 (+0000)
Subject: removing v1l20009.cvc, a datatypes benchmark where the TCC fails (CVC3 and CVC4 diffe... 
X-Git-Tag: cvc5-1.0.0~7859
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bd45444319c0baa11b530184e3065df3a2d926a2;p=cvc5.git

removing v1l20009.cvc, a datatypes benchmark where the TCC fails (CVC3 and CVC4 differ in the answer), so it doesn't really test anything
---

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