File: random5.btor

package info (click to toggle)
boolector 3.2.4-1
  • links: PTS, VCS
  • area: main
  • in suites: sid
  • size: 20,744 kB
  • sloc: ansic: 83,136; cpp: 18,159; sh: 3,668; python: 2,889; makefile: 210
file content (711 lines) | stat: -rw-r--r-- 13,436 bytes parent folder | download
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
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
1 array 4 4
2 array 2 2
3 array 1 2
4 var 2
5 array 2 3
6 var 2
7 var 1
8 array 2 4
9 array 2 3
10 array 1 3
11 array 3 3
12 array 2 2
13 var 4
14 var 4
15 var 3
16 array 1 4
17 var 2
18 var 3
19 array 3 4
20 var 4
21 slice 1 17 0 0
22 slice 1 6 0 0
23 and 1 -21 -22
24 and 1 21 22
25 and 1 -23 -24
26 write 2 2 2 4 6
27 slice 1 17 1 1
28 slice 1 -17 1 1
29 const 2 01
30 add 2 17 29
31 add 2 17 30
32 slice 1 31 1 1
33 and 1 -27 28
34 and 1 32 33
35 and 1 27 -28
36 and 1 -32 35
37 and 1 -34 -36
38 slice 1 -17 0 0
39 slice 1 4 0 0
40 and 1 38 39
41 const 3 000
42 const 3 111
43 slice 1 -25 0 0
44 cond 3 43 42 41
45 concat 4 44 -25
46 ult 1 13 -45
47 slice 3 13 3 1
48 slice 1 47 2 2
49 slice 1 -15 2 2
50 add 3 -15 47
51 slice 1 50 2 2
52 and 1 48 49
53 and 1 -51 52
54 and 1 -48 -49
55 and 1 51 54
56 and 1 -53 -55
57 mul 3 18 47
58 and 1 7 25
59 and 1 -7 -25
60 and 1 -58 -59
61 slice 1 29 1 1
62 slice 1 -61 0 0
63 slice 1 21 0 0
64 add 1 21 -61
65 slice 1 64 0 0
66 and 1 62 63
67 and 1 -65 66
68 and 1 -62 -63
69 and 1 65 68
70 and 1 -67 -69
71 mul 1 -7 -37
72 and 1 -7 -27
73 and 1 7 27
74 and 1 -72 -73
75 and 1 7 46
76 const 1 0
77 concat 2 76 71
78 const 1 1
79 slice 1 74 0 0
80 cond 1 79 78 76
81 concat 2 80 74
82 slice 1 77 1 1
83 slice 1 -81 1 1
84 add 2 29 81
85 add 2 77 84
86 slice 1 85 1 1
87 and 1 -82 83
88 and 1 86 87
89 and 1 82 -83
90 and 1 -86 89
91 and 1 -88 -90
92 add 2 -6 29
93 slice 1 -18 0 0
94 and 1 -21 93
95 and 1 21 -93
96 and 1 -94 -95
97 const 2 00
98 eq 1 17 97
99 slice 1 29 0 0
100 and 1 7 -99
101 array 1 1
102 write 1 1 101 -93 61
103 slice 1 92 0 0
104 ult 1 103 -70
105 slice 1 57 2 2
106 slice 1 18 2 2
107 slice 2 57 1 0
108 slice 2 18 1 0
109 ult 1 107 108
110 and 1 105 -106
111 and 1 -105 -106
112 and 1 105 106
113 and 1 109 111
114 and 1 109 112
115 and 1 -113 -114
116 and 1 -110 115
117 concat 2 76 -74
118 slice 1 -13 0 0
119 srl 2 117 118
120 slice 1 -104 0 0
121 cond 1 120 78 76
122 concat 2 121 -104
123 add 2 29 -92
124 add 2 122 123
125 concat 3 76 119
126 slice 2 125 2 1
127 eq 1 3 3
128 slice 1 15 2 2
129 ult 1 128 -40
130 concat 4 41 75
131 slice 1 -14 3 3
132 slice 1 -130 3 3
133 and 1 -131 -132
134 and 1 131 132
135 and 1 -133 -134
136 const 4 0001
137 add 4 14 136
138 add 4 130 136
139 cond 4 131 137 -14
140 cond 4 132 138 -130
141 udiv 4 139 140
142 add 4 136 -141
143 cond 4 135 142 141
144 slice 2 -15 2 1
145 write 2 2 12 29 -144
146 add 2 29 -77
147 add 2 29 146
148 and 1 56 71
149 and 1 7 100
150 concat 4 41 71
151 write 4 4 1 130 150
152 const 14 00000000000000
153 const 14 11111111111111
154 cond 14 27 153 152
155 concat 16 154 17
156 sll 16 155 130
157 add 4 -130 136
158 srl 16 155 157
159 and 16 -156 -158
160 add 1 -25 78
161 and 1 61 149
162 concat 4 41 -100
163 concat 5 76 -162
164 concat 5 76 150
165 add 5 163 164
166 slice 1 165 4 4
167 concat 3 97 149
168 read 1 10 -167
169 slice 1 57 0 0
170 slice 1 57 1 1
171 and 1 -169 -170
172 and 1 169 170
173 and 1 -171 -172
174 and 1 -105 -173
175 and 1 105 173
176 and 1 -174 -175
177 eq 1 70 116
178 add 1 78 -127
179 urem 3 -125 -47
180 cond 1 49 78 76
181 concat 4 180 -15
182 slice 1 40 0 0
183 cond 3 182 42 41
184 concat 4 183 40
185 udiv 4 -181 184
186 slice 1 -166 0 0
187 cond 3 186 42 41
188 concat 4 187 -166
189 concat 4 41 177
190 slice 1 188 3 3
191 slice 1 189 3 3
192 slice 3 188 2 0
193 slice 3 189 2 0
194 ult 1 192 193
195 and 1 190 -191
196 and 1 -190 -191
197 and 1 190 191
198 and 1 194 196
199 and 1 194 197
200 and 1 -198 -199
201 and 1 -195 200
202 write 3 4 19 -185 125
203 const 3 001
204 add 3 -15 203
205 add 3 57 204
206 slice 1 205 2 2
207 and 1 -105 128
208 and 1 206 207
209 and 1 105 -128
210 and 1 -206 209
211 and 1 -208 -210
212 slice 1 -46 0 0
213 cond 1 212 78 76
214 concat 2 213 -46
215 slice 1 -214 1 1
216 slice 1 126 1 1
217 slice 1 -214 0 0
218 slice 1 126 0 0
219 ult 1 217 218
220 and 1 215 -216
221 and 1 -215 -216
222 and 1 215 216
223 and 1 219 221
224 and 1 219 222
225 and 1 -223 -224
226 and 1 -220 225
227 slice 1 46 0 0
228 slice 1 -56 0 0
229 add 1 46 -56
230 slice 1 229 0 0
231 and 1 227 228
232 and 1 -230 231
233 and 1 -227 -228
234 and 1 230 233
235 and 1 -232 -234
236 slice 1 -15 1 1
237 const 2 11
238 slice 1 -37 0 0
239 cond 2 238 237 97
240 concat 3 239 -37
241 cond 3 236 240 57
242 array 3 1
243 write 3 1 242 161 167
244 slice 1 92 1 1
245 cond 2 244 237 97
246 concat 4 245 92
247 concat 5 76 189
248 concat 5 76 246
249 const 5 00001
250 add 5 248 249
251 add 5 247 250
252 slice 1 251 4 4
253 slice 1 14 1 1
254 ult 1 -100 253
255 array 2 1
256 write 2 1 255 -166 -126
257 write 3 1 243 -161 -241
258 const 7 0000000
259 const 7 1111111
260 slice 1 96 0 0
261 cond 7 260 259 258
262 concat 8 261 96
263 sll 8 262 57
264 slice 1 147 1 1
265 and 1 226 -264
266 mul 1 38 149
267 mul 1 -93 211
268 slice 2 241 1 0
269 write 1 2 3 268 7
270 ult 1 130 14
271 slice 1 -235 0 0
272 cond 3 271 42 41
273 concat 4 272 -235
274 srl 4 273 -29
275 slice 1 -98 0 0
276 cond 3 275 42 41
277 concat 4 276 -98
278 slice 1 277 3 3
279 var 3 130
280 concat 4 41 -149
281 udiv 4 -280 277
282 concat 3 76 -4
283 slice 1 282 2 2
284 slice 2 282 1 0
285 eq 1 97 284
286 and 1 283 285
287 cond 2 27 237 97
288 concat 4 287 17
289 ult 1 -281 288
290 slice 2 281 2 1
291 slice 1 122 1 1
292 slice 1 290 1 1
293 add 2 122 290
294 slice 1 293 1 1
295 and 1 291 292
296 and 1 -294 295
297 and 1 -291 -292
298 and 1 294 297
299 and 1 -296 -298
300 write 3 4 19 184 167
301 eq 1 -4 237
302 slice 1 -70 0 0
303 cond 2 302 237 97
304 concat 3 303 -70
305 slice 1 -143 3 3
306 write 1 3 10 304 305
307 slice 1 266 0 0
308 cond 3 307 42 41
309 concat 4 308 266
310 concat 2 76 -129
311 srl 4 309 -310
312 and 1 61 166
313 write 1 1 101 61 -60
314 and 1 -127 -211
315 and 1 127 211
316 and 1 -314 -315
317 cond 1 216 78 76
318 concat 3 317 126
319 cond 1 291 78 76
320 concat 3 319 122
321 mul 3 318 320
322 slice 1 321 2 2
323 slice 1 321 1 1
324 and 1 -322 -323
325 and 1 322 323
326 and 1 -324 -325
327 array 4 3
328 concat 3 97 71
329 write 4 3 327 -328 -13
330 slice 1 178 0 0
331 cond 2 330 237 97
332 concat 3 331 178
333 write 1 3 306 -332 71
334 slice 1 281 0 0
335 write 1 4 16 130 334
336 const 2 10
337 and 1 -46 -312
338 concat 2 76 7
339 read 1 3 338
340 slice 1 -29 1 1
341 cond 1 340 78 76
342 concat 3 341 -29
343 slice 1 76 0 0
344 cond 2 343 237 97
345 concat 3 344 76
346 add 3 203 345
347 add 3 342 346
348 slice 1 -45 3 3
349 slice 3 -45 2 0
350 slice 3 -143 2 0
351 ult 1 349 350
352 and 1 -305 348
353 and 1 -305 -348
354 and 1 305 348
355 and 1 351 353
356 and 1 351 354
357 and 1 -355 -356
358 and 1 -352 357
359 concat 3 97 98
360 urem 3 359 332
361 srl 16 159 309
362 add 4 136 -309
363 sll 16 159 362
364 and 16 -361 -363
365 and 1 -76 106
366 and 1 76 -106
367 and 1 -365 -366
368 slice 1 -100 0 0
369 cond 2 368 237 97
370 concat 3 369 -100
371 const 3 100
372 eq 1 -370 371
373 eq 1 -15 42
374 and 1 372 373
375 slice 1 270 0 0
376 cond 3 375 42 41
377 concat 4 376 270
378 add 4 181 377
379 and 1 46 -326
380 and 1 -46 326
381 and 1 -379 -380
382 slice 1 347 2 2
383 slice 1 -359 2 2
384 slice 2 347 1 0
385 slice 2 -359 1 0
386 ult 1 384 385
387 and 1 382 -383
388 and 1 -382 -383
389 and 1 382 383
390 and 1 386 388
391 and 1 386 389
392 and 1 -390 -391
393 and 1 -387 392
394 slice 2 378 3 2
395 concat 3 76 4
396 concat 3 76 -394
397 add 3 203 396
398 add 3 395 397
399 slice 1 398 2 2
400 write 1 3 333 347 96
401 write 2 4 8 143 126
402 slice 3 20 2 0
403 eq 1 41 402
404 concat 3 97 252
405 udiv 3 404 240
406 slice 1 241 0 0
407 and 1 -149 406
408 write 2 1 255 -70 124
409 slice 1 286 0 0
410 cond 1 409 78 76
411 concat 2 410 286
412 slice 1 411 0 0
413 slice 1 411 1 1
414 and 1 -412 -413
415 and 1 412 413
416 and 1 -414 -415
417 concat 4 41 -56
418 sll 16 -155 -417
419 slice 3 143 2 0
420 concat 3 97 -91
421 urem 3 419 420
422 eq 1 -46 253
423 eq 1 97 -268
424 read 2 5 167
425 read 2 9 -420
426 read 3 11 167
427 read 2 26 -29
428 read 1 102 116
429 read 2 145 -268
430 read 4 151 273
431 read 3 202 185
432 read 2 256 166
433 read 3 257 -99
434 read 1 269 17
435 read 3 300 181
436 read 1 313 27
437 read 4 329 304
438 read 1 335 311
439 read 1 400 -421
440 read 2 401 13
441 read 2 408 -211
442 slice 1 -29 0 0
443 eq 1 76 442
444 and 1 340 443
445 eq 1 42 179
446 slice 1 -263 0 0
447 slice 1 -263 1 1
448 and 1 -446 -447
449 and 1 446 447
450 and 1 -448 -449
451 slice 1 -263 2 2
452 and 1 -450 -451
453 and 1 450 451
454 and 1 -452 -453
455 slice 1 -263 3 3
456 and 1 -454 -455
457 and 1 454 455
458 and 1 -456 -457
459 slice 1 -263 4 4
460 and 1 -458 -459
461 and 1 458 459
462 and 1 -460 -461
463 slice 1 -263 5 5
464 and 1 -462 -463
465 and 1 462 463
466 and 1 -464 -465
467 slice 1 -263 6 6
468 and 1 -466 -467
469 and 1 466 467
470 and 1 -468 -469
471 slice 1 -263 7 7
472 and 1 -470 -471
473 and 1 470 471
474 and 1 -472 -473
475 slice 1 274 3 3
476 slice 3 274 2 0
477 eq 1 41 476
478 and 1 475 477
479 eq 1 42 279
480 slice 1 -97 0 0
481 slice 1 -97 1 1
482 and 1 -480 -481
483 and 1 480 481
484 and 1 -482 -483
485 const 4 0000
486 eq 1 -311 485
487 slice 1 336 1 1
488 slice 1 336 0 0
489 eq 1 76 488
490 and 1 487 489
491 eq 1 42 -360
492 slice 1 -364 0 0
493 slice 1 -364 1 1
494 and 1 -492 -493
495 and 1 492 493
496 and 1 -494 -495
497 slice 1 -364 2 2
498 and 1 -496 -497
499 and 1 496 497
500 and 1 -498 -499
501 slice 1 -364 3 3
502 and 1 -500 -501
503 and 1 500 501
504 and 1 -502 -503
505 slice 1 -364 4 4
506 and 1 -504 -505
507 and 1 504 505
508 and 1 -506 -507
509 slice 1 -364 5 5
510 and 1 -508 -509
511 and 1 508 509
512 and 1 -510 -511
513 slice 1 -364 6 6
514 and 1 -512 -513
515 and 1 512 513
516 and 1 -514 -515
517 slice 1 -364 7 7
518 and 1 -516 -517
519 and 1 516 517
520 and 1 -518 -519
521 slice 1 -364 8 8
522 and 1 -520 -521
523 and 1 520 521
524 and 1 -522 -523
525 slice 1 -364 9 9
526 and 1 -524 -525
527 and 1 524 525
528 and 1 -526 -527
529 slice 1 -364 10 10
530 and 1 -528 -529
531 and 1 528 529
532 and 1 -530 -531
533 slice 1 -364 11 11
534 and 1 -532 -533
535 and 1 532 533
536 and 1 -534 -535
537 slice 1 -364 12 12
538 and 1 -536 -537
539 and 1 536 537
540 and 1 -538 -539
541 slice 1 -364 13 13
542 and 1 -540 -541
543 and 1 540 541
544 and 1 -542 -543
545 slice 1 -364 14 14
546 and 1 -544 -545
547 and 1 544 545
548 and 1 -546 -547
549 slice 1 -364 15 15
550 and 1 -548 -549
551 and 1 548 549
552 and 1 -550 -551
553 slice 1 405 2 2
554 slice 2 405 1 0
555 eq 1 97 554
556 and 1 553 555
557 slice 1 418 15 15
558 slice 15 418 14 0
559 const 15 000000000000000
560 eq 1 558 559
561 and 1 557 560
562 slice 1 421 0 0
563 slice 1 421 1 1
564 and 1 -562 -563
565 and 1 562 563
566 and 1 -564 -565
567 slice 1 421 2 2
568 and 1 -566 -567
569 and 1 566 567
570 and 1 -568 -569
571 eq 1 237 -424
572 eq 1 237 425
573 slice 1 426 0 0
574 slice 1 426 1 1
575 and 1 -573 -574
576 and 1 573 574
577 and 1 -575 -576
578 slice 1 426 2 2
579 and 1 -577 -578
580 and 1 577 578
581 and 1 -579 -580
582 eq 1 237 427
583 slice 1 429 1 1
584 slice 1 429 0 0
585 eq 1 76 584
586 and 1 583 585
587 slice 1 430 0 0
588 slice 1 430 1 1
589 and 1 -587 -588
590 and 1 587 588
591 and 1 -589 -590
592 slice 1 430 2 2
593 and 1 -591 -592
594 and 1 591 592
595 and 1 -593 -594
596 slice 1 430 3 3
597 and 1 -595 -596
598 and 1 595 596
599 and 1 -597 -598
600 slice 1 -431 0 0
601 slice 1 -431 1 1
602 and 1 -600 -601
603 and 1 600 601
604 and 1 -602 -603
605 slice 1 -431 2 2
606 and 1 -604 -605
607 and 1 604 605
608 and 1 -606 -607
609 eq 1 97 432
610 eq 1 41 433
611 eq 1 41 435
612 slice 1 437 3 3
613 slice 3 437 2 0
614 eq 1 41 613
615 and 1 612 614
616 eq 1 237 440
617 slice 1 441 1 1
618 slice 1 441 0 0
619 eq 1 76 618
620 and 1 617 619
621 and 1 -38 148
622 and 1 38 -148
623 and 1 -621 -622
624 and 1 -160 -168
625 and 1 160 168
626 and 1 -624 -625
627 and 1 176 -201
628 and 1 -254 265
629 and 1 78 267
630 and 1 -278 -289
631 and 1 299 -301
632 and 1 -316 -337
633 and 1 339 358
634 and 1 367 374
635 and 1 -381 393
636 and 1 -399 -403
637 and 1 -407 -416
638 and 1 422 -423
639 and 1 428 434
640 and 1 436 438
641 and 1 -439 444
642 and 1 445 474
643 and 1 478 479
644 and 1 -484 486
645 and 1 490 -491
646 and 1 -552 556
647 and 1 552 -556
648 and 1 -646 -647
649 and 1 -561 -570
650 and 1 571 572
651 and 1 -581 -582
652 and 1 586 599
653 and 1 -608 609
654 and 1 608 -609
655 and 1 -653 -654
656 and 1 -610 611
657 and 1 -615 -616
658 and 1 615 616
659 and 1 -657 -658
660 and 1 -620 -623
661 and 1 620 623
662 and 1 -660 -661
663 and 1 -626 -627
664 and 1 628 629
665 and 1 -630 631
666 and 1 630 -631
667 and 1 -665 -666
668 and 1 632 -633
669 and 1 -634 635
670 and 1 634 -635
671 and 1 -669 -670
672 and 1 -636 637
673 and 1 636 -637
674 and 1 -672 -673
675 and 1 638 -639
676 and 1 -640 -641
677 and 1 640 641
678 and 1 -676 -677
679 and 1 -642 643
680 and 1 644 -645
681 and 1 -644 645
682 and 1 -680 -681
683 and 1 -648 649
684 and 1 -650 651
685 and 1 -652 655
686 and 1 656 -659
687 and 1 -662 -663
688 and 1 -664 667
689 and 1 664 -667
690 and 1 -688 -689
691 and 1 668 -671
692 and 1 674 675
693 and 1 -674 -675
694 and 1 -692 -693
695 and 1 678 679
696 and 1 -682 -683
697 and 1 684 685
698 and 1 -684 -685
699 and 1 -697 -698
700 and 1 686 687
701 and 1 690 -691
702 and 1 -694 695
703 and 1 -696 699
704 and 1 696 -699
705 and 1 -703 -704
706 and 1 700 701
707 and 1 -702 705
708 and 1 702 -705
709 and 1 -707 -708
710 and 1 706 709
711 root 1 710