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