1; EXPECT: unsat
2(set-logic QF_UFLIAFS)
3(declare-fun x () Int)
4(declare-fun c () (Set Int))
5(declare-fun alloc0 () (Set Int))
6(declare-fun alloc1 () (Set Int))
7(declare-fun alloc2 () (Set Int))
8(assert
9(and (member x c)
10      (<= (card (setminus alloc1 alloc0)) 1)
11      (<= (card (setminus alloc2 alloc1))
12          (card (setminus c (singleton x))))
13      (> (card (setminus alloc2 alloc0)) (card c))
14))
15(check-sat)
16