diff options
Diffstat (limited to 'test/regress/regress0/quantifiers/set8.smt2')
| -rw-r--r-- | test/regress/regress0/quantifiers/set8.smt2 | 26 |
1 files changed, 0 insertions, 26 deletions
diff --git a/test/regress/regress0/quantifiers/set8.smt2 b/test/regress/regress0/quantifiers/set8.smt2 deleted file mode 100644 index 684d94b7a..000000000 --- a/test/regress/regress0/quantifiers/set8.smt2 +++ /dev/null @@ -1,26 +0,0 @@ -(set-logic AUFLIA) -(set-info :source | Set theory. |) -(set-info :smt-lib-version 2.0) -(set-info :category "crafted") -(set-info :status unsat) -(declare-sort Set 0) -(declare-sort Elem 0) -(declare-fun member (Elem Set) Bool) -(declare-fun subset (Set Set) Bool) -(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (=> (and (member ?x ?s1) (subset ?s1 ?s2)) (member ?x ?s2)))) -(assert (forall ((?s1 Set) (?s2 Set)) (=> (not (subset ?s1 ?s2)) (exists ((?x Elem)) (and (member ?x ?s1) (not (member ?x ?s2))))))) -(assert (forall ((?s1 Set) (?s2 Set)) (=> (forall ((?x Elem)) (=> (member ?x ?s1) (member ?x ?s2))) (subset ?s1 ?s2)))) -(declare-fun seteq (Set Set) Bool) -(assert (forall ((?s1 Set) (?s2 Set)) (= (seteq ?s1 ?s2) (= ?s1 ?s2)))) -(assert (forall ((?s1 Set) (?s2 Set)) (= (seteq ?s1 ?s2) (and (subset ?s1 ?s2) (subset ?s2 ?s1))))) -(declare-fun union (Set Set) Set) -(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (member ?x (union ?s1 ?s2)) (or (member ?x ?s1) (member ?x ?s2))))) -(declare-fun intersection (Set Set) Set) -(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (member ?x (intersection ?s1 ?s2)) (and (member ?x ?s1) (member ?x ?s2))))) -(declare-fun difference (Set Set) Set) -(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (member ?x (difference ?s1 ?s2)) (and (member ?x ?s1) (not (member ?x ?s2)))))) -(declare-fun a () Set) -(declare-fun b () Set) -(assert (not (seteq (intersection a b) (intersection b a)))) -(check-sat) -(exit) |