1; On a production build (as of 2014-05-16), takes several minutes
2; to finish (2967466 decisions).
3
4(set-logic QF_BVFS)
5(set-info :status unsat)
6
7(define-sort myset () (Set (Set (_ BitVec 1))))
8(declare-fun S () myset)
9
10; 0 elements
11(assert (not (= S (as emptyset myset))))
12
13; 1 element is S
14(assert (not (= S (singleton (as emptyset (Set (_ BitVec 1)))))))
15(assert (not (= S (singleton (singleton (_ bv0 1)) ))))
16(assert (not (= S (singleton (singleton (_ bv1 1)) ))))
17(assert (not (= S (singleton (union (singleton (_ bv0 1))
18                                  (singleton (_ bv1 1)))))))
19
20; 2 elements in S
21(assert (not (= S (union (singleton (as emptyset (Set (_ BitVec 1))))
22                         (singleton (singleton (_ bv0 1)))) )))
23(assert (not (= S (union (singleton (as emptyset (Set (_ BitVec 1))))
24                         (singleton (singleton (_ bv1 1)))))))
25(assert (not (= S (union (singleton (as emptyset (Set (_ BitVec 1))))
26                         (singleton (union (singleton (_ bv0 1))
27                                         (singleton (_ bv1 1))))))))
28(assert (not (= S (union (singleton (union (singleton (_ bv0 1))
29                                         (singleton (_ bv1 1))))
30                         (singleton (singleton (_ bv0 1)))) )))
31(assert (not (= S (union (singleton (singleton (_ bv0 1)))
32                         (singleton (singleton (_ bv1 1))))   )))
33(assert (not (= S (union (singleton (union (singleton (_ bv0 1))
34                                         (singleton (_ bv1 1))))
35                         (singleton (singleton (_ bv1 1)))))))
36
37; 3 elements in S
38(assert (not (= S (union (singleton (singleton (_ bv1 1)))
39                         (union (singleton (as emptyset (Set (_ BitVec 1))))
40                                (singleton (singleton (_ bv0 1)))))  )))
41(assert (not (= S (union (singleton (union (singleton (_ bv0 1))
42                                         (singleton (_ bv1 1))))
43                         (union (singleton (as emptyset (Set (_ BitVec 1))))
44                                (singleton (singleton (_ bv1 1)))))  )))
45(assert (not (= S (union (singleton (union (singleton (_ bv0 1))
46                                         (singleton (_ bv1 1))))
47                         (union (singleton (singleton (_ bv0 1)))
48                                (singleton (singleton (_ bv1 1)))))  )))
49(assert (not (= S (union (singleton (union (singleton (_ bv0 1))
50                                         (singleton (_ bv1 1))))
51                         (union (singleton (as emptyset (Set (_ BitVec 1))))
52                                (singleton (singleton (_ bv0 1)))))  )))
53
54; 4 elements in S
55(assert (not (= S (union (singleton (union (singleton (_ bv0 1))
56                                         (singleton (_ bv1 1))))
57                         (union (singleton (singleton (_ bv1 1)))
58                                (union (singleton (as emptyset (Set (_ BitVec 1))))
59                                       (singleton (singleton (_ bv0 1))))))  )))
60
61(check-sat)
62
63; if you delete any of the above assertions, you should get sat
64; (get-model)
65