Decision #1220 — malloc.c:4954
Status: no_witness
Truth table
| row | c0 br 8350 | c1 br 8351 | c2 br 8352 | c3 br 8353 | outcome |
|---|---|---|---|---|---|
| 3684 | T | * | * | * | T |
| 3685 | T | * | * | * | T |
| 3686 | T | * | * | * | T |
| 3687 | T | * | * | * | T |
| 3688 | T | * | * | * | T |
| 3689 | T | * | * | * | T |
| 3690 | T | * | * | * | T |
| 3691 | T | * | * | * | T |
| 3692 | T | * | * | * | T |
| 3693 | T | * | * | * | T |
| 3694 | T | * | * | * | T |
| 3695 | T | * | * | * | T |
| 3696 | T | * | * | * | T |
| 3697 | T | * | * | * | T |
| 7437 | T | * | * | * | T |
| 7438 | T | * | * | * | T |
| 7439 | T | * | * | * | T |
| 7440 | T | * | * | * | T |
| 7441 | T | * | * | * | T |
| 7442 | T | * | * | * | T |
| 7443 | T | * | * | * | T |
| 7444 | T | * | * | * | T |
| 7445 | T | * | * | * | T |
| 7446 | T | * | * | * | T |
| 7447 | T | * | * | * | T |
| 7448 | T | * | * | * | T |
| 7449 | T | * | * | * | T |
| 7450 | T | * | * | * | T |
| 7451 | T | * | * | * | T |
| 7452 | T | * | * | * | T |
| 7453 | T | * | * | * | T |
| 11420 | T | * | * | * | T |
| 11421 | T | * | * | * | T |
| 11422 | T | * | * | * | T |
| 11423 | T | * | * | * | T |
| 11424 | T | * | * | * | T |
| 11425 | T | * | * | * | T |
| 11426 | T | * | * | * | T |
| 11427 | T | * | * | * | T |
| 11428 | T | * | * | * | T |
| 11429 | T | * | * | * | T |
| 11430 | T | * | * | * | T |
| 11431 | T | * | * | * | T |
| 11432 | T | * | * | * | T |
| 11433 | T | * | * | * | T |
| 11434 | T | * | * | * | T |
| 11435 | T | * | * | * | T |
| 11436 | T | * | * | * | T |
| 11437 | T | * | * | * | T |
| 12993 | T | * | * | * | T |
| 12994 | T | * | * | * | T |
| 14340 | T | * | * | * | T |
| 14341 | T | * | * | * | T |
| 15694 | T | * | * | * | T |
| 15695 | T | * | * | * | T |
| 25176 | T | * | * | * | T |
| 25177 | T | * | * | * | T |
| 34635 | T | * | * | * | T |
| 34636 | T | * | * | * | T |
| 40826 | T | * | * | * | T |
| 40827 | T | * | * | * | T |
| 47039 | T | * | * | * | T |
| 47040 | T | * | * | * | T |
| 51095 | T | * | * | * | T |
| 51096 | T | * | * | * | T |
| 51097 | T | * | * | * | T |
| 51098 | T | * | * | * | T |
| 51099 | T | * | * | * | T |
| 55451 | T | * | * | * | T |
| 55452 | T | * | * | * | T |
| 55453 | T | * | * | * | T |
| 55454 | T | * | * | * | T |
| 55455 | T | * | * | * | T |
| 55456 | T | * | * | * | T |
| 55457 | T | * | * | * | T |
| 59853 | T | * | * | * | T |
| 59854 | T | * | * | * | T |
| 59855 | T | * | * | * | T |
| 59856 | T | * | * | * | T |
| 59857 | T | * | * | * | T |
| 64019 | T | * | * | * | T |
| 64020 | T | * | * | * | T |
| 64021 | T | * | * | * | T |
| 64022 | T | * | * | * | T |
| 64023 | T | * | * | * | T |
| 75607 | T | * | * | * | T |
| 75608 | T | * | * | * | T |
| 75609 | T | * | * | * | T |
| 87120 | T | * | * | * | T |
| 87121 | T | * | * | * | T |
| 87122 | T | * | * | * | T |
| 91310 | T | * | * | * | T |
| 91311 | T | * | * | * | T |
| 91312 | T | * | * | * | T |
| 91313 | T | * | * | * | T |
| 91314 | T | * | * | * | T |
| 91315 | T | * | * | * | T |
| 91316 | T | * | * | * | T |
| 91317 | T | * | * | * | T |
| 91318 | T | * | * | * | T |
| 91319 | T | * | * | * | T |
| 91320 | T | * | * | * | T |
| 91321 | T | * | * | * | T |
| 91322 | T | * | * | * | T |
| 91323 | T | * | * | * | T |
| 91324 | T | * | * | * | T |
| 91325 | T | * | * | * | T |
| 91326 | T | * | * | * | T |
| 91327 | T | * | * | * | T |
| 91328 | T | * | * | * | T |
| 91329 | T | * | * | * | T |
| 91330 | T | * | * | * | T |
| 95578 | T | * | * | * | T |
| 95579 | T | * | * | * | T |
| 95580 | T | * | * | * | T |
| 95581 | T | * | * | * | T |
| 95582 | T | * | * | * | T |
| 95583 | T | * | * | * | T |
| 95584 | T | * | * | * | T |
| 95585 | T | * | * | * | T |
| 95586 | T | * | * | * | T |
| 95587 | T | * | * | * | T |
| 95588 | T | * | * | * | T |
| 95589 | T | * | * | * | T |
| 95590 | T | * | * | * | T |
| 95591 | T | * | * | * | T |
| 95592 | T | * | * | * | T |
| 95593 | T | * | * | * | T |
| 95594 | T | * | * | * | T |
| 95595 | T | * | * | * | T |
| 95596 | T | * | * | * | T |
| 95597 | T | * | * | * | T |
| 95598 | T | * | * | * | T |
| 97585 | T | * | * | * | T |
| 97586 | T | * | * | * | T |
| 99146 | T | * | * | * | T |
| 99147 | T | * | * | * | T |
| 100629 | T | * | * | * | T |
| 100630 | T | * | * | * | T |
| 102079 | T | * | * | * | T |
| 102080 | T | * | * | * | T |
| 104617 | T | * | * | * | T |
| 104618 | T | * | * | * | T |
| 104619 | T | * | * | * | T |
| 108578 | T | * | * | * | T |
| 108579 | T | * | * | * | T |
| 108580 | T | * | * | * | T |
| 108581 | T | * | * | * | T |
| 108582 | T | * | * | * | T |
| 108583 | T | * | * | * | T |
| 108584 | T | * | * | * | T |
| 108585 | T | * | * | * | T |
| 108586 | T | * | * | * | T |
| 108587 | T | * | * | * | T |
| 110597 | T | * | * | * | T |
| 110598 | T | * | * | * | T |
| 113806 | T | * | * | * | T |
| 113807 | T | * | * | * | T |
| 113808 | T | * | * | * | T |
| 113809 | T | * | * | * | T |
| 113810 | T | * | * | * | T |
| 113811 | T | * | * | * | T |
| 113812 | T | * | * | * | T |
| 117019 | T | * | * | * | T |
| 117020 | T | * | * | * | T |
| 117021 | T | * | * | * | T |
| 117022 | T | * | * | * | T |
| 117023 | T | * | * | * | T |
| 140014 | T | * | * | * | T |
| 140015 | T | * | * | * | T |
| 140016 | T | * | * | * | T |
| 162950 | T | * | * | * | T |
| 162951 | T | * | * | * | T |
| 162952 | T | * | * | * | T |
| 164505 | T | * | * | * | T |
| 166172 | T | * | * | * | T |
| 167856 | T | * | * | * | T |
Independent-effect pairs
All 4 conditions live in realloc — 4 br_if
c0(branch8350): GAP view gap →c1(branch8351): DEAD view gap →c2(branch8352): DEAD view gap →c3(branch8353): DEAD view gap →