summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sets/card-5.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/sets/card-5.smt2')
-rw-r--r--test/regress/regress0/sets/card-5.smt225
1 files changed, 0 insertions, 25 deletions
diff --git a/test/regress/regress0/sets/card-5.smt2 b/test/regress/regress0/sets/card-5.smt2
deleted file mode 100644
index 4135a0c16..000000000
--- a/test/regress/regress0/sets/card-5.smt2
+++ /dev/null
@@ -1,25 +0,0 @@
-(set-logic QF_UFLIAFS)
-(set-info :status unsat)
-(declare-sort E 0)
-(declare-fun s () (Set E))
-(declare-fun t () (Set E))
-(declare-fun u () (Set E))
-(assert (>= (card (union s t)) 8))
-(assert (>= (card (union s u)) 8))
-;(assert (<= (card (union t u)) 5))
-(assert (<= (card s) 5))
-(assert (= (as emptyset (Set E)) (intersection t u)))
-(declare-fun x1 () E)
-(declare-fun x2 () E)
-(declare-fun x3 () E)
-(declare-fun x4 () E)
-(declare-fun x5 () E)
-(declare-fun x6 () E)
-(assert (member x1 s))
-(assert (member x2 s))
-(assert (member x3 s))
-(assert (member x4 s))
-(assert (member x5 s))
-(assert (member x6 s))
-(assert (distinct x1 x2 x3 x4 x5 x6))
-(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback