-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathsquare.smt2
251 lines (250 loc) · 14 KB
/
square.smt2
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
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
; RUN: %solver %s | %OutputCheck %s
; CHECK-NEXT: ^unsat
(set-logic QF_BV)
(set-info :source |
Generated by Alberto Griggio. For more details see the following paper.
Leopold Haller, Alberto Griggio, Martin Brain, Daniel Kroening: Deciding floating-point logic with systematic abstraction. FMCAD 2012: 131-140
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun fp.f1 () (_ BitVec 64))
(declare-fun fp.i4 () (_ BitVec 1))
(declare-fun fp.f2 () (_ BitVec 64))
(declare-fun fp.i1 () (_ BitVec 13))
(declare-fun fp.f3 () (_ BitVec 64))
(declare-fun fp.i2 () (_ BitVec 106))
(declare-fun fp.i3 () (_ BitVec 106))
(define-fun def_401 () Bool (= fp.f3 (_ bv0 64)))
(define-fun def_412 () Bool (not def_401))
(define-fun def_347 () (_ BitVec 63) ((_ extract 62 0) fp.f3))
(define-fun def_348 () (_ BitVec 1) (bvcomp def_347 (_ bv0 63)))
(define-fun def_399 () Bool (= def_348 (_ bv1 1)))
(define-fun def_410 () Bool (not def_399))
(define-fun def_337 () (_ BitVec 11) ((_ extract 62 52) fp.f3))
(define-fun def_341 () (_ BitVec 1) (bvcomp def_337 (_ bv2047 11)))
(define-fun def_338 () (_ BitVec 52) ((_ extract 51 0) fp.f3))
(define-fun def_339 () (_ BitVec 1) (bvcomp def_338 (_ bv0 52)))
(define-fun def_340 () (_ BitVec 1) (bvnot def_339))
(define-fun def_343 () (_ BitVec 1) (bvand def_340 def_341))
(define-fun def_396 () Bool (= def_343 (_ bv1 1)))
(define-fun def_409 () Bool (not def_396))
(define-fun def_411 () Bool (and def_409 def_410))
(define-fun def_413 () Bool (and def_411 def_412))
(define-fun def_354 () (_ BitVec 1) ((_ extract 63 63) fp.f3))
(define-fun def_402 () Bool (= def_354 (_ bv0 1)))
(define-fun def_377 () Bool (= def_354 (_ bv1 1)))
(define-fun def_407 () Bool (or def_377 def_402))
(define-fun def_403 () Bool (not def_402))
(define-fun def_408 () Bool (and def_403 def_407))
(define-fun def_414 () Bool (and def_408 def_413))
(define-fun def_389 () Bool (= fp.f1 fp.f2))
(define-fun def_73 () (_ BitVec 63) ((_ extract 62 0) fp.f1))
(define-fun def_74 () (_ BitVec 1) (bvcomp def_73 (_ bv0 63)))
(define-fun def_70 () (_ BitVec 63) ((_ extract 62 0) fp.f2))
(define-fun def_72 () (_ BitVec 1) (bvcomp def_70 (_ bv0 63)))
(define-fun def_385 () (_ BitVec 1) (bvand def_72 def_74))
(define-fun def_386 () Bool (= def_385 (_ bv1 1)))
(define-fun def_391 () Bool (or def_386 def_389))
(define-fun def_54 () (_ BitVec 52) ((_ extract 51 0) fp.f1))
(define-fun def_64 () (_ BitVec 1) (bvcomp def_54 (_ bv0 52)))
(define-fun def_68 () (_ BitVec 1) (bvnot def_64))
(define-fun def_35 () (_ BitVec 11) ((_ extract 62 52) fp.f1))
(define-fun def_55 () (_ BitVec 1) (bvcomp def_35 (_ bv2047 11)))
(define-fun def_69 () (_ BitVec 1) (bvand def_55 def_68))
(define-fun def_46 () (_ BitVec 52) ((_ extract 51 0) fp.f2))
(define-fun def_62 () (_ BitVec 1) (bvcomp def_46 (_ bv0 52)))
(define-fun def_66 () (_ BitVec 1) (bvnot def_62))
(define-fun def_23 () (_ BitVec 11) ((_ extract 62 52) fp.f2))
(define-fun def_48 () (_ BitVec 1) (bvcomp def_23 (_ bv2047 11)))
(define-fun def_67 () (_ BitVec 1) (bvand def_48 def_66))
(define-fun def_383 () (_ BitVec 1) (bvor def_67 def_69))
(define-fun def_384 () Bool (= def_383 (_ bv1 1)))
(define-fun def_390 () Bool (not def_384))
(define-fun def_392 () Bool (and def_390 def_391))
(define-fun def_65 () (_ BitVec 1) (bvand def_55 def_64))
(define-fun def_63 () (_ BitVec 1) (bvand def_48 def_62))
(define-fun def_86 () (_ BitVec 1) (bvor def_63 def_65))
(define-fun def_280 () (_ BitVec 1) (bvor def_86 fp.i4))
(define-fun def_304 () (_ BitVec 1) (bvnot def_280))
(define-fun def_236 () (_ BitVec 1) ((_ extract 53 53) fp.i3))
(define-fun def_230 () (_ BitVec 52) ((_ extract 51 0) fp.i3))
(define-fun def_231 () (_ BitVec 1) (bvcomp def_230 (_ bv0 52)))
(define-fun def_232 () (_ BitVec 1) (bvnot def_231))
(define-fun def_239 () (_ BitVec 1) (bvor def_232 def_236))
(define-fun def_233 () (_ BitVec 1) ((_ extract 52 52) fp.i3))
(define-fun def_240 () (_ BitVec 1) (bvand def_233 def_239))
(define-fun def_241 () (_ BitVec 54) ((_ zero_extend 53) def_240))
(define-fun def_234 () (_ BitVec 53) ((_ extract 105 53) fp.i3))
(define-fun def_237 () (_ BitVec 54) ((_ zero_extend 1) def_234))
(define-fun def_242 () (_ BitVec 54) (bvadd def_237 def_241))
(define-fun def_303 () (_ BitVec 1) ((_ extract 0 0) def_242))
(define-fun def_306 () (_ BitVec 1) (bvand def_303 def_304))
(define-fun def_89 () (_ BitVec 1) (bvand def_65 def_72))
(define-fun def_87 () (_ BitVec 1) (bvand def_63 def_74))
(define-fun def_91 () (_ BitVec 1) (bvor def_87 def_89))
(define-fun def_92 () (_ BitVec 1) (bvor def_69 def_91))
(define-fun def_93 () (_ BitVec 1) (bvor def_67 def_92))
(define-fun def_307 () (_ BitVec 1) (bvor def_93 def_306))
(define-fun def_301 () (_ BitVec 1) (bvor def_93 def_280))
(define-fun def_310 () (_ BitVec 1) (bvnot def_301))
(define-fun def_311 () (_ BitVec 51) ((_ sign_extend 50) def_310))
(define-fun def_309 () (_ BitVec 51) ((_ extract 51 1) def_242))
(define-fun def_313 () (_ BitVec 51) (bvand def_309 def_311))
(define-fun def_314 () (_ BitVec 52) (concat def_313 def_307))
(define-fun def_315 () (_ BitVec 11) ((_ sign_extend 10) def_301))
(define-fun def_247 () (_ BitVec 2) ((_ extract 53 52) def_242))
(define-fun def_248 () (_ BitVec 1) (bvcomp def_247 (_ bv0 2)))
(define-fun def_287 () (_ BitVec 11) ((_ sign_extend 10) def_248))
(define-fun def_290 () (_ BitVec 11) (bvnot def_287))
(define-fun def_244 () (_ BitVec 1) ((_ extract 53 53) def_242))
(define-fun def_245 () (_ BitVec 13) ((_ zero_extend 12) def_244))
(define-fun def_246 () (_ BitVec 13) (bvadd fp.i1 def_245))
(define-fun def_252 () (_ BitVec 11) ((_ extract 10 0) def_246))
(define-fun def_282 () (_ BitVec 11) (bvadd (_ bv1023 11) def_252))
(define-fun def_292 () (_ BitVec 11) (bvand def_282 def_290))
(define-fun def_317 () (_ BitVec 11) (bvor def_292 def_315))
(define-fun def_318 () (_ BitVec 63) (concat def_317 def_314))
(define-fun def_270 () (_ BitVec 1) (bvnot def_93))
(define-fun def_45 () (_ BitVec 1) ((_ extract 63 63) fp.f1))
(define-fun def_44 () (_ BitVec 1) ((_ extract 63 63) fp.f2))
(define-fun def_84 () (_ BitVec 1) (bvcomp def_44 def_45))
(define-fun def_85 () (_ BitVec 1) (bvnot def_84))
(define-fun def_294 () (_ BitVec 1) (bvand def_85 def_270))
(define-fun def_319 () (_ BitVec 64) (concat def_294 def_318))
(define-fun def_379 () Bool (= def_319 fp.f3))
(define-fun def_351 () (_ BitVec 1) (bvcomp def_318 (_ bv0 63)))
(define-fun def_352 () (_ BitVec 1) (bvand def_348 def_351))
(define-fun def_353 () Bool (= def_352 (_ bv1 1)))
(define-fun def_381 () Bool (or def_353 def_379))
(define-fun def_334 () (_ BitVec 1) (bvcomp def_317 (_ bv2047 11)))
(define-fun def_332 () (_ BitVec 1) (bvcomp def_314 (_ bv0 52)))
(define-fun def_333 () (_ BitVec 1) (bvnot def_332))
(define-fun def_336 () (_ BitVec 1) (bvand def_333 def_334))
(define-fun def_345 () (_ BitVec 1) (bvor def_336 def_343))
(define-fun def_346 () Bool (= def_345 (_ bv1 1)))
(define-fun def_380 () Bool (not def_346))
(define-fun def_382 () Bool (and def_380 def_381))
(define-fun def_393 () Bool (and def_382 def_392))
(define-fun def_415 () Bool (and def_393 def_414))
(define-fun def_39 () (_ BitVec 1) (bvcomp def_35 (_ bv0 11)))
(define-fun def_57 () (_ BitVec 1) (bvnot def_39))
(define-fun def_56 () (_ BitVec 1) (bvnot def_55))
(define-fun def_59 () (_ BitVec 1) (bvand def_56 def_57))
(define-fun def_60 () (_ BitVec 53) (concat def_59 def_54))
(define-fun def_76 () (_ BitVec 106) ((_ zero_extend 53) def_60))
(define-fun def_30 () (_ BitVec 1) (bvcomp def_23 (_ bv0 11)))
(define-fun def_50 () (_ BitVec 1) (bvnot def_30))
(define-fun def_49 () (_ BitVec 1) (bvnot def_48))
(define-fun def_52 () (_ BitVec 1) (bvand def_49 def_50))
(define-fun def_53 () (_ BitVec 53) (concat def_52 def_46))
(define-fun def_75 () (_ BitVec 106) ((_ zero_extend 53) def_53))
(define-fun def_77 () (_ BitVec 106) (bvmul def_75 def_76))
(define-fun def_130 () (_ BitVec 128) ((_ zero_extend 22) def_77))
(define-fun def_132 () (_ BitVec 128) (bvand (_ bv340282366920938463444927863358058659840 128) def_130))
(define-fun def_133 () (_ BitVec 1) (bvcomp def_132 (_ bv0 128)))
(define-fun def_134 () (_ BitVec 1) (bvnot def_133))
(define-fun def_135 () (_ BitVec 128) ((_ sign_extend 127) def_134))
(define-fun def_136 () (_ BitVec 128) (bvand (_ bv64 128) def_135))
(define-fun def_137 () (_ BitVec 128) (bvlshr def_130 def_136))
(define-fun def_140 () (_ BitVec 128) (bvand (_ bv18446744069414584320 128) def_137))
(define-fun def_141 () (_ BitVec 1) (bvcomp def_140 (_ bv0 128)))
(define-fun def_142 () (_ BitVec 1) (bvnot def_141))
(define-fun def_143 () (_ BitVec 128) ((_ sign_extend 127) def_142))
(define-fun def_144 () (_ BitVec 128) (bvand (_ bv32 128) def_143))
(define-fun def_145 () (_ BitVec 128) (bvlshr def_137 def_144))
(define-fun def_148 () (_ BitVec 128) (bvand (_ bv4294901760 128) def_145))
(define-fun def_149 () (_ BitVec 1) (bvcomp def_148 (_ bv0 128)))
(define-fun def_150 () (_ BitVec 1) (bvnot def_149))
(define-fun def_151 () (_ BitVec 128) ((_ sign_extend 127) def_150))
(define-fun def_152 () (_ BitVec 128) (bvand (_ bv16 128) def_151))
(define-fun def_153 () (_ BitVec 128) (bvlshr def_145 def_152))
(define-fun def_156 () (_ BitVec 128) (bvand (_ bv65280 128) def_153))
(define-fun def_157 () (_ BitVec 1) (bvcomp def_156 (_ bv0 128)))
(define-fun def_158 () (_ BitVec 1) (bvnot def_157))
(define-fun def_159 () (_ BitVec 128) ((_ sign_extend 127) def_158))
(define-fun def_160 () (_ BitVec 128) (bvand (_ bv8 128) def_159))
(define-fun def_161 () (_ BitVec 128) (bvlshr def_153 def_160))
(define-fun def_164 () (_ BitVec 128) (bvand (_ bv240 128) def_161))
(define-fun def_165 () (_ BitVec 1) (bvcomp def_164 (_ bv0 128)))
(define-fun def_166 () (_ BitVec 1) (bvnot def_165))
(define-fun def_167 () (_ BitVec 128) ((_ sign_extend 127) def_166))
(define-fun def_168 () (_ BitVec 128) (bvand (_ bv4 128) def_167))
(define-fun def_169 () (_ BitVec 128) (bvlshr def_161 def_168))
(define-fun def_172 () (_ BitVec 128) (bvand (_ bv12 128) def_169))
(define-fun def_173 () (_ BitVec 1) (bvcomp def_172 (_ bv0 128)))
(define-fun def_174 () (_ BitVec 1) (bvnot def_173))
(define-fun def_175 () (_ BitVec 128) ((_ sign_extend 127) def_174))
(define-fun def_176 () (_ BitVec 128) (bvand (_ bv2 128) def_175))
(define-fun def_177 () (_ BitVec 128) (bvlshr def_169 def_176))
(define-fun def_180 () (_ BitVec 128) (bvand (_ bv2 128) def_177))
(define-fun def_181 () (_ BitVec 1) (bvcomp def_180 (_ bv0 128)))
(define-fun def_182 () (_ BitVec 1) (bvnot def_181))
(define-fun def_183 () (_ BitVec 128) ((_ sign_extend 127) def_182))
(define-fun def_184 () (_ BitVec 128) (bvand (_ bv1 128) def_183))
(define-fun def_146 () (_ BitVec 128) (bvor def_136 def_144))
(define-fun def_154 () (_ BitVec 128) (bvor def_146 def_152))
(define-fun def_162 () (_ BitVec 128) (bvor def_154 def_160))
(define-fun def_170 () (_ BitVec 128) (bvor def_162 def_168))
(define-fun def_178 () (_ BitVec 128) (bvor def_170 def_176))
(define-fun def_186 () (_ BitVec 128) (bvor def_178 def_184))
(define-fun def_189 () (_ BitVec 128) (bvneg def_186))
(define-fun def_190 () (_ BitVec 128) (bvadd (_ bv105 128) def_189))
(define-fun def_193 () (_ BitVec 13) ((_ extract 12 0) def_190))
(define-fun def_195 () (_ BitVec 13) (bvneg def_193))
(define-fun def_40 () (_ BitVec 11) ((_ zero_extend 10) def_39))
(define-fun def_42 () (_ BitVec 11) (bvadd def_35 def_40))
(define-fun def_43 () (_ BitVec 11) (bvadd (_ bv1025 11) def_42))
(define-fun def_79 () (_ BitVec 13) ((_ sign_extend 2) def_43))
(define-fun def_31 () (_ BitVec 11) ((_ zero_extend 10) def_30))
(define-fun def_33 () (_ BitVec 11) (bvadd def_23 def_31))
(define-fun def_34 () (_ BitVec 11) (bvadd (_ bv1025 11) def_33))
(define-fun def_78 () (_ BitVec 13) ((_ sign_extend 2) def_34))
(define-fun def_80 () (_ BitVec 13) (bvadd def_78 def_79))
(define-fun def_197 () (_ BitVec 13) (bvadd def_80 def_195))
(define-fun def_198 () (_ BitVec 13) (bvadd (_ bv1 13) def_197))
(define-fun def_201 () (_ BitVec 13) (bvneg def_198))
(define-fun def_202 () (_ BitVec 13) (bvadd (_ bv7170 13) def_201))
(define-fun def_204 () Bool (bvslt (_ bv0 13) def_202))
(define-fun def_209 () Bool (not def_204))
(define-fun def_208 () Bool (= fp.i1 (_ bv7169 13)))
(define-fun def_210 () Bool (or def_208 def_209))
(define-fun def_416 () Bool (and def_210 def_415))
(define-fun def_211 () Bool (= def_198 fp.i1))
(define-fun def_212 () Bool (or def_204 def_211))
(define-fun def_417 () Bool (and def_212 def_416))
(define-fun def_213 () (_ BitVec 106) ((_ zero_extend 93) def_202))
(define-fun def_215 () Bool (bvult def_213 (_ bv105 106)))
(define-fun def_219 () Bool (not def_215))
(define-fun def_218 () Bool (= def_213 fp.i2))
(define-fun def_220 () Bool (or def_218 def_219))
(define-fun def_418 () Bool (and def_220 def_417))
(define-fun def_221 () Bool (= fp.i2 (_ bv105 106)))
(define-fun def_222 () Bool (or def_215 def_221))
(define-fun def_419 () Bool (and def_222 def_418))
(define-fun def_191 () (_ BitVec 106) ((_ extract 105 0) def_190))
(define-fun def_192 () (_ BitVec 106) (bvshl def_77 def_191))
(define-fun def_223 () (_ BitVec 106) (bvlshr def_192 fp.i2))
(define-fun def_226 () Bool (= def_223 fp.i3))
(define-fun def_227 () Bool (or def_209 def_226))
(define-fun def_420 () Bool (and def_227 def_419))
(define-fun def_228 () Bool (= def_192 fp.i3))
(define-fun def_229 () Bool (or def_204 def_228))
(define-fun def_421 () Bool (and def_229 def_420))
(define-fun def_257 () Bool (bvslt def_246 (_ bv1024 13)))
(define-fun def_258 () Bool (not def_257))
(define-fun def_250 () (_ BitVec 52) ((_ extract 51 0) def_242))
(define-fun def_249 () (_ BitVec 1) (bvnot def_248))
(define-fun def_251 () (_ BitVec 53) (concat def_249 def_250))
(define-fun def_255 () Bool (= def_251 (_ bv0 53)))
(define-fun def_256 () Bool (not def_255))
(define-fun def_259 () Bool (and def_256 def_258))
(define-fun def_263 () Bool (not def_259))
(define-fun def_262 () Bool (= fp.i4 (_ bv1 1)))
(define-fun def_264 () Bool (or def_262 def_263))
(define-fun def_422 () Bool (and def_264 def_421))
(define-fun def_265 () Bool (= fp.i4 (_ bv0 1)))
(define-fun def_266 () Bool (or def_259 def_265))
(define-fun def_423 () Bool (and def_266 def_422))
(assert def_423)
(check-sat)