blob: cb1dfc842bbca1d4c4cf12a3b24082a1709bd0d3 (
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
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
|
(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_com ((s mySet)) mySet ((_ map not) s))
(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2))
(declare-fun z3v66 () Int)
(declare-fun z3v67 () Int)
(assert (distinct z3v66 z3v67))
(declare-fun z3v68 () Int)
(declare-fun z3f69 (Int) Int)
(declare-fun z3f70 (Int) mySet)
(declare-fun z3v71 () Int)
(declare-fun z3f72 (Int) mySet)
(declare-fun z3v73 () Int)
(declare-fun z3v74 () Int)
(declare-fun z3v75 () Int)
(declare-fun z3f76 (Int) Bool)
(declare-fun z3f77 (Int Int) Int)
(declare-fun z3v78 () Int)
(declare-fun z3f79 (Int) Bool)
(declare-fun z3v80 () Int)
(declare-fun z3f81 (Int) Int)
(declare-fun z3v82 () Int)
(declare-fun z3v83 () Int)
(declare-fun z3v85 () Int)
(declare-fun z3v86 () Int)
(declare-fun z3v87 () Int)
(declare-fun z3f88 () Int)
(declare-fun z3v89 () Int)
(declare-fun z3v90 () Int)
(declare-fun z3v91 () Int)
(declare-fun z3v92 () Int)
(declare-fun z3v93 () Int)
(declare-fun z3f94 (Int) Int)
(declare-fun z3f95 (Int) Int)
(declare-fun z3f96 (Int Int Int) Int)
(declare-fun z3v97 () Int)
(declare-fun z3v98 () Int)
(declare-fun z3v99 () Int)
(declare-fun z3v100 () Int)
(declare-fun z3v101 () Int)
(declare-fun z3v102 () Int)
(declare-fun z3v103 () Int)
(declare-fun z3v104 () Int)
(declare-fun z3v105 () Int)
(declare-fun z3v106 () Int)
(declare-fun z3v107 () Int)
(declare-fun z3v108 () Int)
(declare-fun z3v109 () Int)
(declare-fun z3v110 () Int)
(declare-fun z3v113 () Int)
(declare-fun z3v114 () Int)
(declare-fun z3v115 () Int)
(declare-fun z3v116 () Int)
(declare-fun z3v117 () Int)
(declare-fun z3v118 () Int)
(declare-fun z3v120 () Int)
(declare-fun z3v121 () Int)
(declare-fun z3v122 () Int)
(declare-fun z3v124 () Int)
(declare-fun z3v125 () Int)
(declare-fun z3v126 () Int)
(declare-fun z3v127 () Int)
(declare-fun z3v128 () Int)
(declare-fun z3v129 () Int)
(declare-fun z3v131 () Int)
(declare-fun z3v132 () Int)
(declare-fun z3v133 () Int)
(declare-fun z3v134 () Int)
(declare-fun z3v135 () Int)
(declare-fun z3v136 () Int)
(declare-fun z3v137 () Int)
(declare-fun z3v138 () Int)
(declare-fun z3v139 () Int)
(declare-fun z3v140 () Int)
(declare-fun z3v141 () Int)
(declare-fun z3v142 () Int)
(declare-fun z3v144 () Int)
(declare-fun z3v145 () Int)
(declare-fun z3v146 () Int)
(declare-fun z3v149 () Int)
(declare-fun z3v151 () Int)
(declare-fun z3v154 () Int)
(declare-fun z3v155 () Int)
(declare-fun z3v156 () Int)
(declare-fun z3v157 () Int)
(declare-fun z3v158 () Int)
(declare-fun z3v159 () Int)
(declare-fun z3v161 () Int)
(declare-fun z3v163 () Int)
(declare-fun z3v164 () Int)
(declare-fun z3v165 () Int)
(declare-fun z3v167 () Int)
(declare-fun z3v170 () Int)
(declare-fun z3v174 () Int)
(declare-fun z3v175 () Int)
(declare-fun z3v176 () Int)
(declare-fun z3v179 () Int)
(declare-fun z3v181 () Int)
(declare-fun z3v182 () Int)
(declare-fun z3v183 () Int)
(declare-fun z3v184 () Int)
(declare-fun z3v187 () Int)
(declare-fun z3v188 () Int)
(declare-fun z3v189 () Int)
(declare-fun z3v190 () Int)
(declare-fun z3f191 (Int) Int)
(declare-fun z3f192 (Int) Int)
(declare-fun z3v195 () Int)
(declare-fun z3v196 () Int)
(declare-fun z3v199 () Int)
(declare-fun z3v200 () Int)
(declare-fun z3v201 () Int)
(declare-fun z3v202 () Int)
(declare-fun z3v203 () Int)
(declare-fun z3v206 () Int)
(declare-fun z3v207 () Int)
(declare-fun z3v208 () Int)
(declare-fun z3v210 () Int)
(declare-fun z3v211 () Int)
(declare-fun z3v212 () Int)
(declare-fun z3f213 (Int) Bool)
(declare-fun z3f214 (Int) Int)
(declare-fun z3v215 () Int)
(declare-fun z3v216 () Int)
(declare-fun z3v218 () Int)
(declare-fun z3v220 () Int)
(declare-fun z3v221 () Int)
(declare-fun z3v222 () Int)
(declare-fun z3v223 () Int)
(declare-fun z3v224 () Int)
(declare-fun z3v225 () Int)
(declare-fun z3v226 () Int)
(declare-fun z3v227 () Int)
(declare-fun z3v228 () Int)
(declare-fun z3v229 () Int)
(declare-fun z3v230 () Int)
(declare-fun z3v231 () Int)
(declare-fun z3v233 () Int)
(declare-fun z3v236 () Int)
(declare-fun z3v242 () Int)
(declare-fun z3v243 () Int)
(declare-fun z3v244 () Int)
(declare-fun z3v245 () Int)
(declare-fun z3v247 () Int)
(declare-fun z3v248 () Int)
(declare-fun z3v249 () Int)
(declare-fun z3v250 () Int)
(declare-fun z3v251 () Int)
(declare-fun z3v252 () Int)
(declare-fun z3v253 () Int)
(declare-fun z3v255 () Int)
(declare-fun z3v256 () Int)
(declare-fun z3v258 () Int)
(declare-fun z3v259 () Int)
(declare-fun z3v261 () Int)
(declare-fun z3v262 () Int)
(declare-fun z3v263 () Int)
(declare-fun z3v264 () Int)
(declare-fun z3v266 () Int)
(declare-fun z3v268 () Int)
(declare-fun z3v270 () Int)
(declare-fun z3v271 () Int)
(declare-fun z3v272 () Int)
(declare-fun z3v274 () Int)
(declare-fun z3v275 () Int)
(declare-fun z3v276 () Int)
(declare-fun z3v278 () Int)
(declare-fun z3v279 () Int)
(declare-fun z3v281 () Int)
(declare-fun z3v282 () Int)
(declare-fun z3v283 () Int)
(declare-fun z3v284 () Int)
(declare-fun z3v285 () Int)
(declare-fun z3v287 () Int)
(declare-fun z3v289 () Int)
(declare-fun z3v290 () Int)
(declare-fun z3v291 () Int)
(declare-fun z3v292 () Int)
(declare-fun z3v293 () Int)
(declare-fun z3v296 () Int)
(declare-fun z3v298 () Int)
(declare-fun z3v299 () Int)
(declare-fun z3f300 (Int Int) Int)
(declare-fun z3v301 () Int)
(declare-fun z3v302 () Int)
(declare-fun z3v303 () Int)
(declare-fun z3v304 () Int)
(declare-fun z3v308 () Int)
(declare-fun z3v309 () Int)
(declare-fun z3v310 () Int)
(declare-fun z3v314 () Int)
(declare-fun z3v315 () Int)
(declare-fun z3v316 () Int)
(declare-fun z3v317 () Int)
(declare-fun z3v318 () Int)
(declare-fun z3v319 () Int)
(declare-fun z3v320 () Int)
(declare-fun z3v324 () Int)
(declare-fun z3v325 () Int)
(declare-fun z3v326 () Int)
(declare-fun z3v327 () Int)
(declare-fun z3v328 () Int)
(declare-fun z3v330 () Int)
(declare-fun z3v332 () Int)
(declare-fun z3v333 () Int)
(declare-fun z3v334 () Int)
(declare-fun z3v335 () Int)
(declare-fun z3v336 () Int)
(declare-fun z3v337 () Int)
(declare-fun z3v339 () Int)
(declare-fun z3v340 () Int)
(declare-fun z3v341 () Int)
(declare-fun z3v342 () Int)
(assert (= z3v342 z3v113))
(assert (>= (z3f69 z3v342) 0))
(assert (and (>= (z3f69 z3v113) 0) (>= (z3f69 z3v114) 0) (= (z3f72 z3v114) smt_set_emp) (= (z3f70 z3v114) smt_set_emp) (= (z3f69 z3v114) 0) (= (z3f76 z3v114) true) (>= (z3f69 z3v115) 0) (= (z3f72 z3v115) (ite (smt_set_mem z3v116 (z3f70 z3v113)) (smt_set_cup (smt_set_add smt_set_emp z3v116) (z3f72 z3v113)) (z3f72 z3v113))) (= (z3f70 z3v115) (smt_set_cup (smt_set_add smt_set_emp z3v116) (z3f70 z3v113))) (= (z3f69 z3v115) (+ 1 (z3f69 z3v113))) (= (z3f76 z3v115) false) (= z3v115 (z3f77 z3v116 z3v113)) (>= (z3f69 z3v115) 0) (= z3v115 z3v117) (>= (z3f69 z3v115) 0) (= (z3f72 z3v115) smt_set_emp) (>= (z3f69 z3v117) 0) (= (z3f72 z3v117) smt_set_emp) (z3f79 z3v66) (= (z3f81 z3v80) z3v80) (= (z3f81 z3v82) z3v82) (not (z3f79 z3v67)) (= (z3f81 z3v83) z3v83)))
(assert (not (and (= (z3f72 z3v342) smt_set_emp) (not (smt_set_mem z3v116 (z3f70 z3v342))))))
(check-sat)
|
