1 files changed, 0 insertions, 112 deletions
diff --git a/test/regress/regress0/quantifiers/refcount24.cvc b/test/regress/regress0/quantifiers/refcount24.cvc
deleted file mode 100644
index 21c9a3cfe..000000000
--- a/test/regress/regress0/quantifiers/refcount24.cvc
+++ /dev/null
@@ -1,112 +0,0 @@
-% Preamble  --------------
-DATATYPE UNIT = Unit END;
-DATATYPE BOOL = Truth | Falsity END;
-
-% Decls     --------------
-resource$type: TYPE;
-process$type: TYPE;
-null: resource$type;
-S$elem$type: TYPE = process$type;
-S$t$type: TYPE;
-S$empty: S$t$type;
-S$mem:(S$elem$type, S$t$type) -> BOOL;
-S$add:(S$elem$type, S$t$type) -> S$t$type;
-S$remove:(S$elem$type, S$t$type) -> S$t$type;
-S$cardinality:(S$t$type) -> INT;
-S$mem_empty: BOOLEAN = (FORALL (e: S$elem$type): (NOT ((S$mem((e), (S$empty))) = 
-                                                      (Truth))));
-ASSERT S$mem_empty;
-S$mem_add: BOOLEAN = (FORALL (x: S$elem$type, y: S$elem$type, s: S$t$type): 
-                     ((S$mem((x), (S$add((y), (s))))) = (IF (((x) = (y)) OR 
-                                                            ((S$mem((x), (s))) = 
-                                                            (Truth))) THEN 
-                                                        (Truth) ELSE 
-                                                        (Falsity) ENDIF)));
-ASSERT S$mem_add;
-S$mem_remove: BOOLEAN = (FORALL (x: S$elem$type, y: S$elem$type, s: S$t$type): 
-                        ((S$mem((x), (S$remove((y), (s))))) = (IF ((NOT 
-                                                                   ((x) = 
-                                                                   (y))) AND 
-                                                                  ((S$mem(
-                                                                   (x), (s))) = 
-                                                                  (Truth))) THEN 
-                                                              (Truth) ELSE 
-                                                              (Falsity) ENDIF)));
-ASSERT S$mem_remove;
-S$card_empty: BOOLEAN = ((S$cardinality((S$empty))) = (0));
-ASSERT S$card_empty;
-S$card_zero: BOOLEAN = (FORALL (s: S$t$type): (((S$cardinality((s))) = (0)) => 
-                                              ((s) = (S$empty))));
-ASSERT S$card_zero;
-S$card_non_negative: BOOLEAN = (FORALL (s: S$t$type): ((S$cardinality((s))) >= 
-                               (0)));
-ASSERT S$card_non_negative;
-S$card_add: BOOLEAN = (FORALL (x: S$elem$type, s: S$t$type): ((S$cardinality(
-                                                              (S$add(
-                                                              (x), (s))))) = 
-                                                             (IF ((S$mem(
-                                                                  (x), (s))) = 
-                                                                 (Truth)) THEN 
-                                                             (S$cardinality(
-                                                             (s))) ELSE (
-                                                             (S$cardinality(
-                                                             (s))) + 
-                                                             (1)) ENDIF)));
-ASSERT S$card_add;
-S$card_remove: BOOLEAN = (FORALL (x: S$elem$type, s: S$t$type): ((S$cardinality(
-                                                                 (S$remove(
-                                                                 (x), (s))))) = 
-                                                                (IF (
-                                                                    (S$mem(
-                                                                    (x), (s))) = 
-                                                                    (Truth)) THEN (
-                                                                (S$cardinality(
-                                                                (s))) - 
-                                                                (1)) ELSE 
-                                                                (S$cardinality(
-                                                                (s))) ENDIF)));
-ASSERT S$card_remove;
-
-% Var Decls --------------
-count: ARRAY resource$type OF INT;
-ref: ARRAY process$type OF resource$type;
-valid: ARRAY resource$type OF BOOL;
-destroy$r: resource$type;
-valid$1: ARRAY resource$type OF BOOL;
-
-% Asserts   --------------
-ASSERT (NOT ((FORALL (p: process$type): ((NOT 
-                                                                    (
-                                                                    (
-                                                                    (ref)[
-                                                                    (p)]) = 
-                                                                    (null))) => 
-                                                                   ((
-                                                                    (valid)[
-                                                                    (
-                                                                    (ref)[
-                                                                    (p)])]) = 
-                                                                   (Truth)))) => 
-                                       ((NOT ((destroy$r) = (null))) => 
-                                       ((((valid)[(destroy$r)]) = (Truth)) => 
-                                       ((((count)[(destroy$r)]) = (0)) => 
-                                       (((valid$1) = ((valid) WITH [(destroy$r)] := 
-                                                     (Falsity))) => (FORALL 
-                                                                    (
-                                                                    p: process$type): 
-                                                                    (
-                                                                    (NOT 
-                                                                    (
-                                                                    (
-                                                                    (ref)[
-                                                                    (p)]) = 
-                                                                    (null))) => 
-                                                                    (
-                                                                    (
-                                                                    (valid$1)[
-                                                                    (
-                                                                    (ref)[
-                                                                    (p)])]) = 
-                                                                    (Truth))))))))));
-                           
-CHECKSAT;