blob: 448022a2e82152d0bead0fa7268d8fb56fb0033a (
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
65
66
67
68
69
70
71
72
73
74
75
|
(set-logic QF_ALL)
(set-info :status unsat)
(define-sort Elt () Int)
(define-sort mySet () (Set Elt ))
(define-fun smt_set_emp () mySet (as emptyset mySet))
(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (member x s))
(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (singleton x)))
(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2))
(declare-fun z3v58 () Int)
(declare-fun z3v59 () Int)
(assert (distinct z3v58 z3v59))
(declare-fun z3f60 (Int) Bool)
(declare-fun z3v61 () Int)
(declare-fun z3f62 (Int) Int)
(declare-fun z3v63 () Int)
(declare-fun z3v64 () Int)
(declare-fun z3v65 () Int)
(declare-fun z3v66 () Int)
(declare-fun z3f67 (Int) mySet)
(declare-fun z3v69 () Int)
(declare-fun z3f70 (Int) Int)
(declare-fun z3v76 () Int)
(declare-fun z3v77 () Int)
(declare-fun z3v78 () Int)
(declare-fun z3v79 () Int)
(declare-fun z3v80 () Int)
(declare-fun z3v81 () Int)
(declare-fun z3v82 () Int)
(declare-fun z3f83 (Int) Int)
(declare-fun z3f84 (Int) Int)
(declare-fun z3v85 () Int)
(declare-fun z3f86 (Int) Int)
(declare-fun z3f87 (Int Int) Int)
(declare-fun z3v88 () Int)
(declare-fun z3v89 () Int)
(declare-fun z3f90 (Int) mySet)
(declare-fun z3f91 (Int) Bool)
(declare-fun z3f92 (Int Int) Int)
(declare-fun z3v93 () Int)
(declare-fun z3v94 () Int)
(declare-fun z3v95 () Int)
(declare-fun z3v96 () Int)
(declare-fun z3v97 () Int)
(declare-fun z3v99 () Int)
(assert (= z3v99 z3v89))
(assert (>= (z3f70 z3v99) 0))
(assert (and (not (z3f60 z3v79))
(not (z3f60 z3v79))
(= z3v79 z3v80)
(= (z3f60 z3v79)
(= z3v76 z3v81))
(= (z3f60 z3v80)
(= z3v76 z3v81))
(= (z3f83 z3v82) z3v81)
(= (z3f91 z3v78) false)
(= z3v78 (z3f92 z3v88 z3v89))
(= z3v82 z3v88)
(= (z3f67 z3v78)
(smt_set_cup (smt_set_add smt_set_emp (z3f83 z3v88))
(z3f67 z3v89)))
(= (z3f62 z3v64) z3v64)))
(assert (smt_set_mem z3v76 (z3f67 z3v78)))
(assert (<= z3v95 z3v93))
(assert (>= z3v95 z3v93))
(assert (not (smt_set_mem z3v76 (z3f67 z3v99))))
(check-sat)
|
