-
Notifications
You must be signed in to change notification settings - Fork 0
/
sqrt.c.15-sfxp_16.16_RU_WP.smt2
561 lines (561 loc) · 28.7 KB
/
sqrt.c.15-sfxp_16.16_RU_WP.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
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
(set-info :smt-lib-version 2.6)
(set-logic QF_FXP)
(set-info :category "crafted")
(set-info :source |Alberto Griggio <griggio@fbk.eu>. These benchmarks were used for the evaluation in the following paper: L. Haller, A. Griggio, M. Brain, D. Kroening: Deciding floating-point logic with systematic abstraction. FMCAD 2012. Real-numbered literals have been automatically translated by MathSAT|)
(set-info :status sat)
;; MathSAT API call trace ;; generated on 05/20/15 17:24:54
(declare-fun b662 () (_ SFXP 32 16))
(declare-fun b1084 () (_ SFXP 32 16))
(declare-fun b1141 () (_ SFXP 32 16))
(declare-fun b1554 () (_ SFXP 32 16))
(declare-fun b1110 () (_ SFXP 32 16))
(declare-fun b1246 () (_ SFXP 32 16))
(declare-fun b1211 () (_ SFXP 32 16))
(declare-fun b1421 () (_ SFXP 32 16))
(declare-fun b1491 () (_ SFXP 32 16))
(declare-fun b652 () (_ SFXP 32 16))
(declare-fun b1545 () (_ SFXP 32 16))
(declare-fun b174 () (_ SFXP 32 16))
(declare-fun b1461 () (_ SFXP 32 16))
(declare-fun b1089 () (_ SFXP 32 16))
(declare-fun b1281 () (_ SFXP 32 16))
(declare-fun b1316 () (_ SFXP 32 16))
(declare-fun b1496 () (_ SFXP 32 16))
(declare-fun b1526 () (_ SFXP 32 16))
(declare-fun b176 () (_ SFXP 32 16))
(declare-fun b1456 () (_ SFXP 32 16))
(declare-fun b1216 () (_ SFXP 32 16))
(declare-fun b169 () (_ SFXP 32 16))
(declare-fun b1181 () (_ SFXP 32 16))
(declare-fun b1351 () (_ SFXP 32 16))
(declare-fun b1391 () (_ SFXP 32 16))
(declare-fun b1426 () (_ SFXP 32 16))
(declare-fun b185 () (_ SFXP 32 16))
(declare-fun b1146 () (_ SFXP 32 16))
(declare-fun b1356 () (_ SFXP 32 16))
(declare-fun b1321 () (_ SFXP 32 16))
(declare-fun b1251 () (_ SFXP 32 16))
(declare-fun b171 () (_ SFXP 32 16))
(declare-fun b1176 () (_ SFXP 32 16))
(declare-fun b1286 () (_ SFXP 32 16))
(declare-fun b1386 () (_ SFXP 32 16))
(declare-fun b1105 () (_ SFXP 32 16))
(define-fun _t_3 () RoundingMode roundUp)
(define-fun _t_9 () (_ SFXP 32 16) b169)
(define-fun _t_10 () (_ SFXP 32 16) b171)
(define-fun _t_11 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_9 _t_10))
(define-fun _t_12 () (_ SFXP 32 16) _t_11)
(define-fun _t_13 () (_ SFXP 32 16) b185)
(define-fun _t_14 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_12 _t_13))
(define-fun _t_15 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_11 _t_11))
(define-fun _t_16 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_15))
(define-fun _t_17 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_16))
(define-fun _t_18 () (_ SFXP 32 16) _t_17)
(define-fun _t_19 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_18 _t_14))
(define-fun _t_20 () (_ SFXP 32 16) _t_19)
(define-fun _t_21 () (_ SFXP 32 16) (sfxp.add wrapAround _t_11 _t_20))
(define-fun _t_22 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_21 _t_21))
(define-fun _t_23 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_22))
(define-fun _t_24 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_23))
(define-fun _t_25 () (_ SFXP 32 16) _t_24)
(define-fun _t_26 () (_ SFXP 32 16) _t_25)
(define-fun _t_27 () (_ SFXP 32 16) b1554)
(define-fun _t_28 () Bool (= _t_26 _t_27))
(define-fun _t_29 () Bool (not _t_28))
(define-fun _t_30 () (_ SFXP 32 16) _t_21)
(define-fun _t_31 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_13 _t_30))
(define-fun _t_32 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_25 _t_31))
(define-fun _t_33 () (_ SFXP 32 16) _t_32)
(define-fun _t_34 () (_ SFXP 32 16) (sfxp.add wrapAround _t_21 _t_33))
(define-fun _t_35 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_34 _t_34))
(define-fun _t_36 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_35))
(define-fun _t_37 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_36))
(define-fun _t_38 () (_ SFXP 32 16) _t_37)
(define-fun _t_39 () (_ SFXP 32 16) _t_38)
(define-fun _t_40 () (_ SFXP 32 16) b1545)
(define-fun _t_41 () Bool (= _t_39 _t_40))
(define-fun _t_42 () Bool (not _t_41))
(define-fun _t_43 () (_ SFXP 32 16) b1496)
(define-fun _t_44 () Bool (= _t_34 _t_43))
(define-fun _t_45 () Bool (not _t_44))
(define-fun _t_46 () (_ SFXP 32 16) _t_43)
(define-fun _t_47 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_13 _t_46))
(define-fun _t_48 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_43 _t_43))
(define-fun _t_49 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_48))
(define-fun _t_50 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_49))
(define-fun _t_51 () (_ SFXP 32 16) _t_50)
(define-fun _t_52 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_51 _t_47))
(define-fun _t_53 () (_ SFXP 32 16) _t_52)
(define-fun _t_54 () (_ SFXP 32 16) (sfxp.add wrapAround _t_43 _t_53))
(define-fun _t_55 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_54 _t_54))
(define-fun _t_56 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_55))
(define-fun _t_57 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_56))
(define-fun _t_58 () (_ SFXP 32 16) _t_57)
(define-fun _t_59 () (_ SFXP 32 16) _t_58)
(define-fun _t_60 () (_ SFXP 32 16) b1526)
(define-fun _t_61 () Bool (= _t_59 _t_60))
(define-fun _t_62 () Bool (not _t_61))
(define-fun _t_63 () (_ SFXP 32 16) b1461)
(define-fun _t_64 () Bool (= _t_54 _t_63))
(define-fun _t_65 () Bool (not _t_64))
(define-fun _t_66 () (_ SFXP 32 16) _t_63)
(define-fun _t_67 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_13 _t_66))
(define-fun _t_68 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_63 _t_63))
(define-fun _t_69 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_68))
(define-fun _t_70 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_69))
(define-fun _t_71 () (_ SFXP 32 16) _t_70)
(define-fun _t_72 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_71 _t_67))
(define-fun _t_73 () (_ SFXP 32 16) _t_72)
(define-fun _t_74 () (_ SFXP 32 16) (sfxp.add wrapAround _t_63 _t_73))
(define-fun _t_75 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_74 _t_74))
(define-fun _t_76 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_75))
(define-fun _t_77 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_76))
(define-fun _t_78 () (_ SFXP 32 16) _t_77)
(define-fun _t_79 () (_ SFXP 32 16) _t_78)
(define-fun _t_80 () (_ SFXP 32 16) b1491)
(define-fun _t_81 () Bool (= _t_79 _t_80))
(define-fun _t_82 () Bool (not _t_81))
(define-fun _t_83 () (_ SFXP 32 16) b1426)
(define-fun _t_84 () (_ SFXP 32 16) _t_83)
(define-fun _t_85 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_13 _t_84))
(define-fun _t_86 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_83 _t_83))
(define-fun _t_87 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_86))
(define-fun _t_88 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_87))
(define-fun _t_89 () (_ SFXP 32 16) _t_88)
(define-fun _t_90 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_89 _t_85))
(define-fun _t_91 () (_ SFXP 32 16) _t_90)
(define-fun _t_92 () (_ SFXP 32 16) (sfxp.add wrapAround _t_83 _t_91))
(define-fun _t_93 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_92 _t_92))
(define-fun _t_94 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_93))
(define-fun _t_95 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_94))
(define-fun _t_96 () (_ SFXP 32 16) _t_95)
(define-fun _t_97 () (_ SFXP 32 16) _t_96)
(define-fun _t_98 () (_ SFXP 32 16) b1456)
(define-fun _t_99 () Bool (= _t_97 _t_98))
(define-fun _t_100 () Bool (not _t_99))
(define-fun _t_101 () Bool (= _t_74 _t_83))
(define-fun _t_102 () Bool (not _t_101))
(define-fun _t_103 () (_ SFXP 32 16) b1391)
(define-fun _t_104 () Bool (= _t_92 _t_103))
(define-fun _t_105 () Bool (not _t_104))
(define-fun _t_106 () (_ SFXP 32 16) _t_103)
(define-fun _t_107 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_13 _t_106))
(define-fun _t_108 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_103 _t_103))
(define-fun _t_109 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_108))
(define-fun _t_110 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_109))
(define-fun _t_111 () (_ SFXP 32 16) _t_110)
(define-fun _t_112 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_111 _t_107))
(define-fun _t_113 () (_ SFXP 32 16) _t_112)
(define-fun _t_114 () (_ SFXP 32 16) (sfxp.add wrapAround _t_103 _t_113))
(define-fun _t_115 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_114 _t_114))
(define-fun _t_116 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_115))
(define-fun _t_117 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_116))
(define-fun _t_118 () (_ SFXP 32 16) _t_117)
(define-fun _t_119 () (_ SFXP 32 16) _t_118)
(define-fun _t_120 () (_ SFXP 32 16) b1421)
(define-fun _t_121 () Bool (= _t_119 _t_120))
(define-fun _t_122 () Bool (not _t_121))
(define-fun _t_123 () (_ SFXP 32 16) b1356)
(define-fun _t_124 () Bool (= _t_114 _t_123))
(define-fun _t_125 () Bool (not _t_124))
(define-fun _t_126 () (_ SFXP 32 16) _t_123)
(define-fun _t_127 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_13 _t_126))
(define-fun _t_128 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_123 _t_123))
(define-fun _t_129 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_128))
(define-fun _t_130 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_129))
(define-fun _t_131 () (_ SFXP 32 16) _t_130)
(define-fun _t_132 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_131 _t_127))
(define-fun _t_133 () (_ SFXP 32 16) _t_132)
(define-fun _t_134 () (_ SFXP 32 16) (sfxp.add wrapAround _t_123 _t_133))
(define-fun _t_135 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_134 _t_134))
(define-fun _t_136 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_135))
(define-fun _t_137 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_136))
(define-fun _t_138 () (_ SFXP 32 16) _t_137)
(define-fun _t_139 () (_ SFXP 32 16) _t_138)
(define-fun _t_140 () (_ SFXP 32 16) b1386)
(define-fun _t_141 () Bool (= _t_139 _t_140))
(define-fun _t_142 () Bool (not _t_141))
(define-fun _t_143 () (_ SFXP 32 16) b1321)
(define-fun _t_144 () Bool (= _t_134 _t_143))
(define-fun _t_145 () Bool (not _t_144))
(define-fun _t_146 () (_ SFXP 32 16) _t_143)
(define-fun _t_147 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_13 _t_146))
(define-fun _t_148 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_143 _t_143))
(define-fun _t_149 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_148))
(define-fun _t_150 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_149))
(define-fun _t_151 () (_ SFXP 32 16) _t_150)
(define-fun _t_152 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_151 _t_147))
(define-fun _t_153 () (_ SFXP 32 16) _t_152)
(define-fun _t_154 () (_ SFXP 32 16) (sfxp.add wrapAround _t_143 _t_153))
(define-fun _t_155 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_154 _t_154))
(define-fun _t_156 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_155))
(define-fun _t_157 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_156))
(define-fun _t_158 () (_ SFXP 32 16) _t_157)
(define-fun _t_159 () (_ SFXP 32 16) _t_158)
(define-fun _t_160 () (_ SFXP 32 16) b1351)
(define-fun _t_161 () Bool (= _t_159 _t_160))
(define-fun _t_162 () Bool (not _t_161))
(define-fun _t_163 () (_ SFXP 32 16) b1286)
(define-fun _t_164 () Bool (= _t_154 _t_163))
(define-fun _t_165 () Bool (not _t_164))
(define-fun _t_166 () (_ SFXP 32 16) _t_163)
(define-fun _t_167 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_13 _t_166))
(define-fun _t_168 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_163 _t_163))
(define-fun _t_169 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_168))
(define-fun _t_170 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_169))
(define-fun _t_171 () (_ SFXP 32 16) _t_170)
(define-fun _t_172 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_171 _t_167))
(define-fun _t_173 () (_ SFXP 32 16) _t_172)
(define-fun _t_174 () (_ SFXP 32 16) (sfxp.add wrapAround _t_163 _t_173))
(define-fun _t_175 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_174 _t_174))
(define-fun _t_176 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_175))
(define-fun _t_177 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_176))
(define-fun _t_178 () (_ SFXP 32 16) _t_177)
(define-fun _t_179 () (_ SFXP 32 16) _t_178)
(define-fun _t_180 () (_ SFXP 32 16) b1316)
(define-fun _t_181 () Bool (= _t_179 _t_180))
(define-fun _t_182 () Bool (not _t_181))
(define-fun _t_183 () (_ SFXP 32 16) b1251)
(define-fun _t_184 () Bool (= _t_174 _t_183))
(define-fun _t_185 () Bool (not _t_184))
(define-fun _t_186 () (_ SFXP 32 16) _t_183)
(define-fun _t_187 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_13 _t_186))
(define-fun _t_188 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_183 _t_183))
(define-fun _t_189 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_188))
(define-fun _t_190 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_189))
(define-fun _t_191 () (_ SFXP 32 16) _t_190)
(define-fun _t_192 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_191 _t_187))
(define-fun _t_193 () (_ SFXP 32 16) _t_192)
(define-fun _t_194 () (_ SFXP 32 16) (sfxp.add wrapAround _t_183 _t_193))
(define-fun _t_195 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_194 _t_194))
(define-fun _t_196 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_195))
(define-fun _t_197 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_196))
(define-fun _t_198 () (_ SFXP 32 16) _t_197)
(define-fun _t_199 () (_ SFXP 32 16) _t_198)
(define-fun _t_200 () (_ SFXP 32 16) b1281)
(define-fun _t_201 () Bool (= _t_199 _t_200))
(define-fun _t_202 () Bool (not _t_201))
(define-fun _t_203 () (_ SFXP 32 16) b1216)
(define-fun _t_204 () Bool (= _t_194 _t_203))
(define-fun _t_205 () Bool (not _t_204))
(define-fun _t_206 () (_ SFXP 32 16) _t_203)
(define-fun _t_207 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_13 _t_206))
(define-fun _t_208 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_203 _t_203))
(define-fun _t_209 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_208))
(define-fun _t_210 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_209))
(define-fun _t_211 () (_ SFXP 32 16) _t_210)
(define-fun _t_212 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_211 _t_207))
(define-fun _t_213 () (_ SFXP 32 16) _t_212)
(define-fun _t_214 () (_ SFXP 32 16) (sfxp.add wrapAround _t_203 _t_213))
(define-fun _t_215 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_214 _t_214))
(define-fun _t_216 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_215))
(define-fun _t_217 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_216))
(define-fun _t_218 () (_ SFXP 32 16) _t_217)
(define-fun _t_219 () (_ SFXP 32 16) _t_218)
(define-fun _t_220 () (_ SFXP 32 16) b1246)
(define-fun _t_221 () Bool (= _t_219 _t_220))
(define-fun _t_222 () Bool (not _t_221))
(define-fun _t_223 () (_ SFXP 32 16) b1181)
(define-fun _t_224 () Bool (= _t_214 _t_223))
(define-fun _t_225 () Bool (not _t_224))
(define-fun _t_226 () (_ SFXP 32 16) _t_223)
(define-fun _t_227 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_13 _t_226))
(define-fun _t_228 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_223 _t_223))
(define-fun _t_229 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_228))
(define-fun _t_230 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_229))
(define-fun _t_231 () (_ SFXP 32 16) _t_230)
(define-fun _t_232 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_231 _t_227))
(define-fun _t_233 () (_ SFXP 32 16) _t_232)
(define-fun _t_234 () (_ SFXP 32 16) (sfxp.add wrapAround _t_223 _t_233))
(define-fun _t_235 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_234 _t_234))
(define-fun _t_236 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_235))
(define-fun _t_237 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_236))
(define-fun _t_238 () (_ SFXP 32 16) _t_237)
(define-fun _t_239 () (_ SFXP 32 16) _t_238)
(define-fun _t_240 () (_ SFXP 32 16) b1211)
(define-fun _t_241 () Bool (= _t_239 _t_240))
(define-fun _t_242 () Bool (not _t_241))
(define-fun _t_243 () (_ SFXP 32 16) b1146)
(define-fun _t_244 () Bool (= _t_234 _t_243))
(define-fun _t_245 () Bool (not _t_244))
(define-fun _t_246 () (_ SFXP 32 16) _t_243)
(define-fun _t_247 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_13 _t_246))
(define-fun _t_248 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_243 _t_243))
(define-fun _t_249 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_248))
(define-fun _t_250 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_249))
(define-fun _t_251 () (_ SFXP 32 16) _t_250)
(define-fun _t_252 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_251 _t_247))
(define-fun _t_253 () (_ SFXP 32 16) _t_252)
(define-fun _t_254 () (_ SFXP 32 16) (sfxp.add wrapAround _t_243 _t_253))
(define-fun _t_255 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_254 _t_254))
(define-fun _t_256 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_255))
(define-fun _t_257 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_256))
(define-fun _t_258 () (_ SFXP 32 16) _t_257)
(define-fun _t_259 () (_ SFXP 32 16) _t_258)
(define-fun _t_260 () (_ SFXP 32 16) b1176)
(define-fun _t_261 () Bool (= _t_259 _t_260))
(define-fun _t_262 () Bool (not _t_261))
(define-fun _t_263 () (_ SFXP 32 16) b1110)
(define-fun _t_264 () Bool (= _t_254 _t_263))
(define-fun _t_265 () Bool (not _t_264))
(define-fun _t_266 () (_ SFXP 32 16) _t_263)
(define-fun _t_267 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_13 _t_266))
(define-fun _t_268 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_263 _t_263))
(define-fun _t_269 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_268))
(define-fun _t_270 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_269))
(define-fun _t_271 () (_ SFXP 32 16) _t_270)
(define-fun _t_272 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_271 _t_267))
(define-fun _t_273 () (_ SFXP 32 16) _t_272)
(define-fun _t_274 () (_ SFXP 32 16) (sfxp.add wrapAround _t_263 _t_273))
(define-fun _t_275 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_274 _t_274))
(define-fun _t_276 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_275))
(define-fun _t_277 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_276))
(define-fun _t_278 () (_ SFXP 32 16) _t_277)
(define-fun _t_279 () (_ SFXP 32 16) _t_278)
(define-fun _t_280 () (_ SFXP 32 16) b1141)
(define-fun _t_281 () Bool (= _t_279 _t_280))
(define-fun _t_282 () Bool (not _t_281))
(define-fun _t_283 () (_ SFXP 32 16) b1089)
(define-fun _t_284 () Bool (= _t_274 _t_283))
(define-fun _t_285 () Bool (not _t_284))
(define-fun _t_286 () (_ SFXP 32 16) _t_283)
(define-fun _t_287 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_13 _t_286))
(define-fun _t_288 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_283 _t_283))
(define-fun _t_289 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_288))
(define-fun _t_290 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_289))
(define-fun _t_291 () (_ SFXP 32 16) _t_290)
(define-fun _t_292 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_291 _t_287))
(define-fun _t_293 () (_ SFXP 32 16) _t_292)
(define-fun _t_294 () (_ SFXP 32 16) (sfxp.add wrapAround _t_283 _t_293))
(define-fun _t_295 () (_ SFXP 32 16) (sfxp.mul wrapAround _t_3 _t_294 _t_294))
(define-fun _t_296 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_295))
(define-fun _t_297 () (_ SFXP 32 16) (sfxp.add wrapAround _t_9 _t_296))
(define-fun _t_298 () (_ SFXP 32 16) _t_297)
(define-fun _t_299 () (_ SFXP 32 16) _t_298)
(define-fun _t_300 () (_ SFXP 32 16) b1105)
(define-fun _t_301 () Bool (= _t_299 _t_300))
(define-fun _t_302 () Bool (not _t_301))
(define-fun _t_303 () (_ SFXP 32 16) b652)
(define-fun _t_304 () (_ SFXP 32 16) _t_303)
(define-fun _t_305 () (_ SFXP 32 16) b1084)
(define-fun _t_306 () Bool (= _t_304 _t_305))
(define-fun _t_307 () Bool (not _t_306))
(define-fun _t_308 () (_ SFXP 32 16) b176)
(define-fun _t_309 () Bool (= _t_9 _t_308))
(define-fun _t_310 () Bool (not _t_309))
(define-fun _t_311 () Bool (sfxp.leq _t_308 _t_9))
(define-fun _t_312 () Bool (and _t_310 _t_311))
(define-fun _t_313 () Bool (sfxp.leq _t_308 _t_304))
(define-fun _t_314 () Bool (not _t_313))
(define-fun _t_315 () Bool (and _t_312 _t_314))
(define-fun _t_316 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_304))
(define-fun _t_317 () Bool (= _t_305 _t_316))
(define-fun _t_318 () Bool (and _t_315 _t_317))
(define-fun _t_319 () Bool (and _t_307 _t_318))
(define-fun _t_320 () Bool (sfxp.leq _t_308 _t_299))
(define-fun _t_321 () Bool (not _t_320))
(define-fun _t_322 () Bool (and _t_319 _t_321))
(define-fun _t_323 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_299))
(define-fun _t_324 () Bool (= _t_300 _t_323))
(define-fun _t_325 () Bool (and _t_322 _t_324))
(define-fun _t_326 () Bool (and _t_302 _t_325))
(define-fun _t_327 () Bool (= _t_263 _t_283))
(define-fun _t_328 () Bool (and _t_326 _t_327))
(define-fun _t_329 () Bool (and _t_285 _t_328))
(define-fun _t_330 () (_ SFXP 32 16) _t_280)
(define-fun _t_331 () (_ SFXP 32 16) b174)
(define-fun _t_332 () Bool (sfxp.leq _t_330 _t_331))
(define-fun _t_333 () Bool (not _t_332))
(define-fun _t_334 () Bool (and _t_329 _t_333))
(define-fun _t_335 () Bool (sfxp.leq _t_308 _t_279))
(define-fun _t_336 () Bool (not _t_335))
(define-fun _t_337 () Bool (and _t_334 _t_336))
(define-fun _t_338 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_279))
(define-fun _t_339 () Bool (= _t_280 _t_338))
(define-fun _t_340 () Bool (and _t_337 _t_339))
(define-fun _t_341 () Bool (and _t_282 _t_340))
(define-fun _t_342 () Bool (= _t_243 _t_263))
(define-fun _t_343 () Bool (and _t_341 _t_342))
(define-fun _t_344 () Bool (and _t_265 _t_343))
(define-fun _t_345 () (_ SFXP 32 16) _t_260)
(define-fun _t_346 () Bool (sfxp.leq _t_345 _t_331))
(define-fun _t_347 () Bool (not _t_346))
(define-fun _t_348 () Bool (and _t_344 _t_347))
(define-fun _t_349 () Bool (sfxp.leq _t_308 _t_259))
(define-fun _t_350 () Bool (not _t_349))
(define-fun _t_351 () Bool (and _t_348 _t_350))
(define-fun _t_352 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_259))
(define-fun _t_353 () Bool (= _t_260 _t_352))
(define-fun _t_354 () Bool (and _t_351 _t_353))
(define-fun _t_355 () Bool (and _t_262 _t_354))
(define-fun _t_356 () Bool (= _t_223 _t_243))
(define-fun _t_357 () Bool (and _t_355 _t_356))
(define-fun _t_358 () Bool (and _t_245 _t_357))
(define-fun _t_359 () (_ SFXP 32 16) _t_240)
(define-fun _t_360 () Bool (sfxp.leq _t_359 _t_331))
(define-fun _t_361 () Bool (not _t_360))
(define-fun _t_362 () Bool (and _t_358 _t_361))
(define-fun _t_363 () Bool (sfxp.leq _t_308 _t_239))
(define-fun _t_364 () Bool (not _t_363))
(define-fun _t_365 () Bool (and _t_362 _t_364))
(define-fun _t_366 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_239))
(define-fun _t_367 () Bool (= _t_240 _t_366))
(define-fun _t_368 () Bool (and _t_365 _t_367))
(define-fun _t_369 () Bool (and _t_242 _t_368))
(define-fun _t_370 () Bool (= _t_203 _t_223))
(define-fun _t_371 () Bool (and _t_369 _t_370))
(define-fun _t_372 () Bool (and _t_225 _t_371))
(define-fun _t_373 () (_ SFXP 32 16) _t_220)
(define-fun _t_374 () Bool (sfxp.leq _t_373 _t_331))
(define-fun _t_375 () Bool (not _t_374))
(define-fun _t_376 () Bool (and _t_372 _t_375))
(define-fun _t_377 () Bool (sfxp.leq _t_308 _t_219))
(define-fun _t_378 () Bool (not _t_377))
(define-fun _t_379 () Bool (and _t_376 _t_378))
(define-fun _t_380 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_219))
(define-fun _t_381 () Bool (= _t_220 _t_380))
(define-fun _t_382 () Bool (and _t_379 _t_381))
(define-fun _t_383 () Bool (and _t_222 _t_382))
(define-fun _t_384 () Bool (= _t_183 _t_203))
(define-fun _t_385 () Bool (and _t_383 _t_384))
(define-fun _t_386 () Bool (and _t_205 _t_385))
(define-fun _t_387 () (_ SFXP 32 16) _t_200)
(define-fun _t_388 () Bool (sfxp.leq _t_387 _t_331))
(define-fun _t_389 () Bool (not _t_388))
(define-fun _t_390 () Bool (and _t_386 _t_389))
(define-fun _t_391 () Bool (sfxp.leq _t_308 _t_199))
(define-fun _t_392 () Bool (not _t_391))
(define-fun _t_393 () Bool (and _t_390 _t_392))
(define-fun _t_394 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_199))
(define-fun _t_395 () Bool (= _t_200 _t_394))
(define-fun _t_396 () Bool (and _t_393 _t_395))
(define-fun _t_397 () Bool (and _t_202 _t_396))
(define-fun _t_398 () Bool (= _t_163 _t_183))
(define-fun _t_399 () Bool (and _t_397 _t_398))
(define-fun _t_400 () Bool (and _t_185 _t_399))
(define-fun _t_401 () (_ SFXP 32 16) _t_180)
(define-fun _t_402 () Bool (sfxp.leq _t_401 _t_331))
(define-fun _t_403 () Bool (not _t_402))
(define-fun _t_404 () Bool (and _t_400 _t_403))
(define-fun _t_405 () Bool (sfxp.leq _t_308 _t_179))
(define-fun _t_406 () Bool (not _t_405))
(define-fun _t_407 () Bool (and _t_404 _t_406))
(define-fun _t_408 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_179))
(define-fun _t_409 () Bool (= _t_180 _t_408))
(define-fun _t_410 () Bool (and _t_407 _t_409))
(define-fun _t_411 () Bool (and _t_182 _t_410))
(define-fun _t_412 () Bool (= _t_143 _t_163))
(define-fun _t_413 () Bool (and _t_411 _t_412))
(define-fun _t_414 () Bool (and _t_165 _t_413))
(define-fun _t_415 () (_ SFXP 32 16) _t_160)
(define-fun _t_416 () Bool (sfxp.leq _t_415 _t_331))
(define-fun _t_417 () Bool (not _t_416))
(define-fun _t_418 () Bool (and _t_414 _t_417))
(define-fun _t_419 () (_ SFXP 32 16) _t_40)
(define-fun _t_420 () Bool (sfxp.leq _t_419 _t_331))
(define-fun _t_421 () Bool (not _t_420))
(define-fun _t_422 () Bool (and _t_418 _t_421))
(define-fun _t_423 () Bool (sfxp.leq _t_308 _t_159))
(define-fun _t_424 () Bool (not _t_423))
(define-fun _t_425 () Bool (and _t_422 _t_424))
(define-fun _t_426 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_159))
(define-fun _t_427 () Bool (= _t_160 _t_426))
(define-fun _t_428 () Bool (and _t_425 _t_427))
(define-fun _t_429 () Bool (and _t_162 _t_428))
(define-fun _t_430 () Bool (= _t_123 _t_143))
(define-fun _t_431 () Bool (and _t_429 _t_430))
(define-fun _t_432 () Bool (and _t_145 _t_431))
(define-fun _t_433 () (_ SFXP 32 16) _t_140)
(define-fun _t_434 () Bool (sfxp.leq _t_433 _t_331))
(define-fun _t_435 () Bool (not _t_434))
(define-fun _t_436 () Bool (and _t_432 _t_435))
(define-fun _t_437 () Bool (sfxp.leq _t_308 _t_139))
(define-fun _t_438 () Bool (not _t_437))
(define-fun _t_439 () Bool (and _t_436 _t_438))
(define-fun _t_440 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_139))
(define-fun _t_441 () Bool (= _t_140 _t_440))
(define-fun _t_442 () Bool (and _t_439 _t_441))
(define-fun _t_443 () Bool (and _t_142 _t_442))
(define-fun _t_444 () Bool (= _t_103 _t_123))
(define-fun _t_445 () Bool (and _t_443 _t_444))
(define-fun _t_446 () Bool (and _t_125 _t_445))
(define-fun _t_447 () (_ SFXP 32 16) _t_120)
(define-fun _t_448 () Bool (sfxp.leq _t_447 _t_331))
(define-fun _t_449 () Bool (not _t_448))
(define-fun _t_450 () Bool (and _t_446 _t_449))
(define-fun _t_451 () Bool (sfxp.leq _t_308 _t_119))
(define-fun _t_452 () Bool (not _t_451))
(define-fun _t_453 () Bool (and _t_450 _t_452))
(define-fun _t_454 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_119))
(define-fun _t_455 () Bool (= _t_120 _t_454))
(define-fun _t_456 () Bool (and _t_453 _t_455))
(define-fun _t_457 () Bool (and _t_122 _t_456))
(define-fun _t_458 () Bool (= _t_63 _t_83))
(define-fun _t_459 () Bool (and _t_457 _t_458))
(define-fun _t_460 () Bool (= _t_83 _t_103))
(define-fun _t_461 () Bool (and _t_459 _t_460))
(define-fun _t_462 () Bool (and _t_105 _t_461))
(define-fun _t_463 () Bool (and _t_102 _t_462))
(define-fun _t_464 () (_ SFXP 32 16) _t_98)
(define-fun _t_465 () Bool (sfxp.leq _t_464 _t_331))
(define-fun _t_466 () Bool (not _t_465))
(define-fun _t_467 () Bool (and _t_463 _t_466))
(define-fun _t_468 () Bool (sfxp.leq _t_308 _t_97))
(define-fun _t_469 () Bool (not _t_468))
(define-fun _t_470 () Bool (and _t_467 _t_469))
(define-fun _t_471 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_97))
(define-fun _t_472 () Bool (= _t_98 _t_471))
(define-fun _t_473 () Bool (and _t_470 _t_472))
(define-fun _t_474 () Bool (and _t_100 _t_473))
(define-fun _t_475 () (_ SFXP 32 16) _t_80)
(define-fun _t_476 () Bool (sfxp.leq _t_475 _t_331))
(define-fun _t_477 () Bool (not _t_476))
(define-fun _t_478 () Bool (and _t_474 _t_477))
(define-fun _t_479 () Bool (sfxp.leq _t_308 _t_79))
(define-fun _t_480 () Bool (not _t_479))
(define-fun _t_481 () Bool (and _t_478 _t_480))
(define-fun _t_482 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_79))
(define-fun _t_483 () Bool (= _t_80 _t_482))
(define-fun _t_484 () Bool (and _t_481 _t_483))
(define-fun _t_485 () Bool (and _t_82 _t_484))
(define-fun _t_486 () Bool (= _t_43 _t_63))
(define-fun _t_487 () Bool (and _t_485 _t_486))
(define-fun _t_488 () Bool (and _t_65 _t_487))
(define-fun _t_489 () (_ SFXP 32 16) _t_60)
(define-fun _t_490 () Bool (sfxp.leq _t_489 _t_331))
(define-fun _t_491 () Bool (not _t_490))
(define-fun _t_492 () Bool (and _t_488 _t_491))
(define-fun _t_493 () Bool (sfxp.leq _t_308 _t_59))
(define-fun _t_494 () Bool (not _t_493))
(define-fun _t_495 () Bool (and _t_492 _t_494))
(define-fun _t_496 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_59))
(define-fun _t_497 () Bool (= _t_60 _t_496))
(define-fun _t_498 () Bool (and _t_495 _t_497))
(define-fun _t_499 () Bool (and _t_62 _t_498))
(define-fun _t_500 () Bool (= _t_21 _t_43))
(define-fun _t_501 () Bool (and _t_499 _t_500))
(define-fun _t_502 () (_ SFXP 32 16) _t_27)
(define-fun _t_503 () Bool (sfxp.leq _t_502 _t_331))
(define-fun _t_504 () Bool (and _t_501 _t_503))
(define-fun _t_505 () Bool (and _t_45 _t_504))
(define-fun _t_506 () Bool (sfxp.leq _t_308 _t_39))
(define-fun _t_507 () Bool (not _t_506))
(define-fun _t_508 () Bool (and _t_505 _t_507))
(define-fun _t_509 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_39))
(define-fun _t_510 () Bool (= _t_40 _t_509))
(define-fun _t_511 () Bool (and _t_508 _t_510))
(define-fun _t_512 () Bool (and _t_42 _t_511))
(define-fun _t_513 () Bool (sfxp.leq _t_308 _t_26))
(define-fun _t_514 () Bool (not _t_513))
(define-fun _t_515 () Bool (and _t_512 _t_514))
(define-fun _t_516 () (_ SFXP 32 16) (sfxp.neg wrapAround _t_26))
(define-fun _t_517 () Bool (= _t_27 _t_516))
(define-fun _t_518 () Bool (and _t_515 _t_517))
(define-fun _t_519 () (_ SFXP 32 16) b662)
(define-fun _t_520 () Bool (sfxp.leq _t_305 _t_519))
(define-fun _t_521 () Bool (not _t_520))
(define-fun _t_522 () Bool (and _t_518 _t_521))
(define-fun _t_523 () Bool (and _t_29 _t_522))
(assert _t_523)
(check-sat)
(exit)