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