test/regress/regress0/sets/card-4.smt2

   1 (set-logic QF_UFLIAFS)
   2 (declare-sort E 0)
   3 (declare-fun s () (Set E))
   4 (declare-fun t () (Set E))
   5 (declare-fun u () (Set E))
   6 (assert (>= (card (union s t)) 8))
   7 (assert (>= (card (union s u)) 8))
   8 ;(assert (<= (card (union t u)) 5))
   9 (assert (<= (card s) 5))
  10 (assert (= (as emptyset (Set E)) (intersection t u)))
  11 (declare-fun x1 () E)
  12 (declare-fun x2 () E)
  13 (declare-fun x3 () E)
  14 (declare-fun x4 () E)
  15 (declare-fun x5 () E)
  16 (declare-fun x6 () E)
  17 (assert (member x1 s))
  18 (assert (member x2 s))
  19 (assert (member x3 s))
  20 (assert (member x4 s))
  21 (assert (member x5 s))
  22 (assert (member x6 s))
  23 (check-sat)