summaryrefslogtreecommitdiff
path: root/test/regress/regress0/trim.cvc
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/trim.cvc')
-rw-r--r--test/regress/regress0/trim.cvc36
1 files changed, 0 insertions, 36 deletions
diff --git a/test/regress/regress0/trim.cvc b/test/regress/regress0/trim.cvc
deleted file mode 100644
index 8bdbde79a..000000000
--- a/test/regress/regress0/trim.cvc
+++ /dev/null
@@ -1,36 +0,0 @@
-% COMMAND-LINE: --finite-model-find
-% EXPECT: sat
-DATATYPE
- myType = A | B
-END;
-%%% structured datatypes
-myTypeSet: TYPE = SET OF myType;
-myTypeGammaSet: TYPE = [# pos: myTypeSet, neg: myTypeSet #];
-delta: TYPE = ARRAY myType OF myTypeGammaSet;
-labels: TYPE = ARRAY myType OF SET OF STRING;
-
-%%% the empty myTypes set
-emptymyTypeSet : SET OF myType;
-ASSERT emptymyTypeSet = {} :: SET OF myType;
-
-d: delta;
-l: labels;
-
-ASSERT (l[A] = {"L","H"});
-ASSERT (l[B] = {"L"});
-
-ic0_i : myTypeSet;
-ic0_c : myTypeSet;
-ASSERT FORALL (r:myType):
- (r IS_IN ic0_i) => FORALL (r2: myType): (r2 IS_IN d[r].neg) => r2 IS_IN ic0_c;
-ASSERT {A} <= ic0_i;
-ASSERT ((EXISTS (e0 : myType): (e0 IS_IN ic0_i) => (l[A] <= l[e0]))) OR ((ic0_i & ic0_c) <= emptymyTypeSet);
-
-ic1_i : myTypeSet;
-ic1_c : myTypeSet;
-ASSERT FORALL (r:myType):
- (r IS_IN d[B].pos) => r IS_IN ic1_i;
-ASSERT ((EXISTS (e1 : myType): (e1 IS_IN ic1_i) => (l[B] <= l[e1]))) OR ((ic1_i & ic1_c) <= emptymyTypeSet);
-
-CHECKSAT;
-%COUNTEREXAMPLE;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback