Decision #1217 — malloc.c:4443
Status: partial
Truth table
| row | c0 br 8337 | c1 br 8338 | c2 br 8339 | c3 br 8340 | c4 br 8341 | c5 br 8342 | c6 br 8343 | c7 br 8344 | outcome |
|---|---|---|---|---|---|---|---|---|---|
| 3631 | * | T | T | * | * | * | F | F | F |
| 3632 | * | T | T | * | * | * | F | F | F |
| 3633 | * | T | T | * | * | * | T | * | T |
| 3634 | * | T | T | * | * | * | T | * | T |
| 3635 | * | T | T | * | * | * | T | * | T |
| 3636 | * | T | T | * | * | * | T | * | T |
| 3637 | * | T | T | * | * | * | T | * | T |
| 3638 | * | T | T | * | * | * | T | * | T |
| 3639 | * | T | T | * | * | * | T | * | T |
| 3640 | * | T | T | * | * | * | T | * | T |
| 3641 | * | T | T | * | * | * | T | * | T |
| 3642 | * | T | T | * | * | * | T | * | T |
| 3643 | * | T | T | * | * | * | T | * | T |
| 3644 | * | T | T | * | * | * | T | * | T |
| 3645 | * | T | T | * | * | * | T | * | T |
| 3646 | * | T | T | * | * | * | T | * | T |
| 3647 | * | T | T | * | * | * | T | * | T |
| 3648 | * | T | T | * | * | * | T | * | T |
| 3649 | * | T | T | * | * | * | T | * | T |
| 7384 | * | T | T | * | * | * | F | F | F |
| 7385 | * | T | T | * | * | * | F | F | F |
| 7386 | * | T | T | * | * | * | T | * | T |
| 7387 | * | T | T | * | * | * | T | * | T |
| 7388 | * | T | T | * | * | * | T | * | T |
| 7389 | * | T | T | * | * | * | T | * | T |
| 7390 | * | T | T | * | * | * | T | * | T |
| 7391 | * | T | T | * | * | * | T | * | T |
| 7392 | * | T | T | * | * | * | T | * | T |
| 7393 | * | T | T | * | * | * | T | * | T |
| 7394 | * | T | T | * | * | * | T | * | T |
| 7395 | * | T | T | * | * | * | T | * | T |
| 7396 | * | T | T | * | * | * | T | * | T |
| 7397 | * | T | T | * | * | * | T | * | T |
| 7398 | * | T | T | * | * | * | T | * | T |
| 7399 | * | T | T | * | * | * | T | * | T |
| 7400 | * | T | T | * | * | * | T | * | T |
| 7401 | * | T | T | * | * | * | T | * | T |
| 7402 | * | T | T | * | * | * | T | * | T |
| 11364 | * | T | T | * | * | * | F | F | F |
| 11365 | * | T | T | * | * | * | F | F | F |
| 11366 | * | T | T | * | * | * | T | * | T |
| 11367 | * | T | T | * | * | * | T | * | T |
| 11368 | * | T | T | * | * | * | T | * | T |
| 11369 | * | T | T | * | * | * | T | * | T |
| 11370 | * | T | T | * | * | * | T | * | T |
| 11371 | * | T | T | * | * | * | T | * | T |
| 11372 | * | T | T | * | * | * | T | * | T |
| 11373 | * | T | T | * | * | * | T | * | T |
| 11374 | * | T | T | * | * | * | T | * | T |
| 11375 | * | T | T | * | * | * | T | * | T |
| 11376 | * | T | T | * | * | * | T | * | T |
| 11377 | * | T | T | * | * | * | T | * | T |
| 11378 | * | T | T | * | * | * | T | * | T |
| 11379 | * | T | T | * | * | * | T | * | T |
| 11380 | * | T | T | * | * | * | T | * | T |
| 11381 | * | T | T | * | * | * | T | * | T |
| 11382 | * | T | T | * | * | * | T | * | T |
| 11383 | * | T | T | * | * | * | T | * | T |
| 12981 | * | T | T | * | * | * | F | F | F |
| 12982 | * | T | T | * | * | * | T | * | T |
| 12983 | * | T | T | * | * | * | T | * | T |
| 12984 | * | T | T | * | * | * | T | * | T |
| 12985 | * | T | T | * | * | * | T | * | T |
| 14328 | * | T | T | * | * | * | F | F | F |
| 14329 | * | T | T | * | * | * | T | * | T |
| 14330 | * | T | T | * | * | * | T | * | T |
| 14331 | * | T | T | * | * | * | T | * | T |
| 14332 | * | T | T | * | * | * | T | * | T |
| 15682 | * | T | T | * | * | * | F | F | F |
| 15683 | * | T | T | * | * | * | T | * | T |
| 15684 | * | T | T | * | * | * | T | * | T |
| 15685 | * | T | T | * | * | * | T | * | T |
| 15686 | * | T | T | * | * | * | T | * | T |
| 25154 | * | T | T | * | * | * | F | F | F |
| 25155 | * | T | T | * | * | * | T | * | T |
| 25156 | * | T | T | * | * | * | T | * | T |
| 25157 | * | T | T | * | * | * | T | * | T |
| 25158 | * | T | T | * | * | * | T | * | T |
| 25159 | * | T | T | * | * | * | T | * | T |
| 25160 | * | T | T | * | * | * | T | * | T |
| 25161 | * | T | T | * | * | * | T | * | T |
| 25162 | * | T | T | * | * | * | T | * | T |
| 34613 | * | T | T | * | * | * | F | F | F |
| 34614 | * | T | T | * | * | * | T | * | T |
| 34615 | * | T | T | * | * | * | T | * | T |
| 34616 | * | T | T | * | * | * | T | * | T |
| 34617 | * | T | T | * | * | * | T | * | T |
| 34618 | * | T | T | * | * | * | T | * | T |
| 34619 | * | T | T | * | * | * | T | * | T |
| 34620 | * | T | T | * | * | * | T | * | T |
| 34621 | * | T | T | * | * | * | T | * | T |
| 40813 | * | T | T | * | * | * | F | F | F |
| 40814 | * | T | T | * | * | * | T | * | T |
| 40815 | * | T | T | * | * | * | T | * | T |
| 40816 | * | T | T | * | * | * | T | * | T |
| 40817 | * | T | T | * | * | * | T | * | T |
| 40818 | * | T | T | * | * | * | T | * | T |
| 47026 | * | T | T | * | * | * | F | F | F |
| 47027 | * | T | T | * | * | * | T | * | T |
| 47028 | * | T | T | * | * | * | T | * | T |
| 47029 | * | T | T | * | * | * | T | * | T |
| 47030 | * | T | T | * | * | * | T | * | T |
| 47031 | * | T | T | * | * | * | T | * | T |
| 51061 | * | T | T | * | * | * | F | F | F |
| 51062 | * | T | T | * | * | * | F | F | F |
| 51063 | * | T | T | * | * | * | T | * | T |
| 51064 | * | T | T | * | * | * | T | * | T |
| 51065 | * | T | T | * | * | * | T | * | T |
| 51066 | * | T | T | * | * | * | T | * | T |
| 51067 | * | T | T | * | * | * | T | * | T |
| 51068 | * | T | T | * | * | * | T | * | T |
| 51069 | * | T | T | * | * | * | T | * | T |
| 51070 | * | T | T | * | * | * | T | * | T |
| 51071 | * | T | T | * | * | * | T | * | T |
| 51072 | * | T | T | * | * | * | T | * | T |
| 51073 | * | T | T | * | * | * | T | * | T |
| 51074 | * | T | T | * | * | * | T | * | T |
| 55411 | * | T | T | * | * | * | F | F | F |
| 55412 | * | T | T | * | * | * | F | F | F |
| 55413 | * | T | T | * | * | * | T | * | T |
| 55414 | * | T | T | * | * | * | T | * | T |
| 55415 | * | T | T | * | * | * | T | * | T |
| 55416 | * | T | T | * | * | * | T | * | T |
| 55417 | * | T | T | * | * | * | T | * | T |
| 55418 | * | T | T | * | * | * | T | * | T |
| 55419 | * | T | T | * | * | * | T | * | T |
| 55420 | * | T | T | * | * | * | T | * | T |
| 55421 | * | T | T | * | * | * | T | * | T |
| 55422 | * | T | T | * | * | * | T | * | T |
| 55423 | * | T | T | * | * | * | T | * | T |
| 55424 | * | T | T | * | * | * | T | * | T |
| 55425 | * | T | T | * | * | * | T | * | T |
| 55426 | * | T | T | * | * | * | T | * | T |
| 59819 | * | T | T | * | * | * | F | F | F |
| 59820 | * | T | T | * | * | * | F | F | F |
| 59821 | * | T | T | * | * | * | T | * | T |
| 59822 | * | T | T | * | * | * | T | * | T |
| 59823 | * | T | T | * | * | * | T | * | T |
| 59824 | * | T | T | * | * | * | T | * | T |
| 59825 | * | T | T | * | * | * | T | * | T |
| 59826 | * | T | T | * | * | * | T | * | T |
| 59827 | * | T | T | * | * | * | T | * | T |
| 59828 | * | T | T | * | * | * | T | * | T |
| 59829 | * | T | T | * | * | * | T | * | T |
| 59830 | * | T | T | * | * | * | T | * | T |
| 59831 | * | T | T | * | * | * | T | * | T |
| 59832 | * | T | T | * | * | * | T | * | T |
| 63985 | * | T | T | * | * | * | F | F | F |
| 63986 | * | T | T | * | * | * | F | F | F |
| 63987 | * | T | T | * | * | * | T | * | T |
| 63988 | * | T | T | * | * | * | T | * | T |
| 63989 | * | T | T | * | * | * | T | * | T |
| 63990 | * | T | T | * | * | * | T | * | T |
| 63991 | * | T | T | * | * | * | T | * | T |
| 63992 | * | T | T | * | * | * | T | * | T |
| 63993 | * | T | T | * | * | * | T | * | T |
| 63994 | * | T | T | * | * | * | T | * | T |
| 63995 | * | T | T | * | * | * | T | * | T |
| 63996 | * | T | T | * | * | * | T | * | T |
| 63997 | * | T | T | * | * | * | T | * | T |
| 63998 | * | T | T | * | * | * | T | * | T |
| 75586 | * | T | T | * | * | * | F | F | F |
| 75587 | * | T | T | * | * | * | T | * | T |
| 75588 | * | T | T | * | * | * | T | * | T |
| 75589 | * | T | T | * | * | * | T | * | T |
| 75590 | * | T | T | * | * | * | T | * | T |
| 75591 | * | T | T | * | * | * | T | * | T |
| 75592 | * | T | T | * | * | * | T | * | T |
| 75593 | * | T | T | * | * | * | T | * | T |
| 75594 | * | T | T | * | * | * | T | * | T |
| 87099 | * | T | T | * | * | * | F | F | F |
| 87100 | * | T | T | * | * | * | T | * | T |
| 87101 | * | T | T | * | * | * | T | * | T |
| 87102 | * | T | T | * | * | * | T | * | T |
| 87103 | * | T | T | * | * | * | T | * | T |
| 87104 | * | T | T | * | * | * | T | * | T |
| 87105 | * | T | T | * | * | * | T | * | T |
| 87106 | * | T | T | * | * | * | T | * | T |
| 87107 | * | T | T | * | * | * | T | * | T |
| 91239 | * | T | T | * | * | * | F | F | F |
| 91240 | * | T | T | * | * | * | T | * | T |
| 91241 | * | T | T | * | * | * | T | * | T |
| 91242 | * | T | T | * | * | * | T | * | T |
| 91243 | * | T | T | * | * | * | T | * | T |
| 91244 | * | T | T | * | * | * | T | * | T |
| 91245 | * | T | T | * | * | * | T | * | T |
| 91246 | * | T | T | * | * | * | T | * | T |
| 91247 | * | T | T | * | * | * | T | * | T |
| 91248 | * | T | T | * | * | * | T | * | T |
| 91249 | * | T | T | * | * | * | T | * | T |
| 91250 | * | T | T | * | * | * | T | * | T |
| 91251 | * | T | T | * | * | * | T | * | T |
| 91252 | * | T | T | * | * | * | T | * | T |
| 91253 | * | T | T | * | * | * | T | * | T |
| 91254 | * | T | T | * | * | * | T | * | T |
| 91255 | * | T | T | * | * | * | T | * | T |
| 91256 | * | T | T | * | * | * | T | * | T |
| 91257 | * | T | T | * | * | * | T | * | T |
| 91258 | * | T | T | * | * | * | T | * | T |
| 91259 | * | T | T | * | * | * | T | * | T |
| 91260 | * | T | T | * | * | * | T | * | T |
| 91261 | * | T | T | * | * | * | T | * | T |
| 91262 | * | T | T | * | * | * | T | * | T |
| 91263 | * | T | T | * | * | * | T | * | T |
| 95507 | * | T | T | * | * | * | F | F | F |
| 95508 | * | T | T | * | * | * | T | * | T |
| 95509 | * | T | T | * | * | * | T | * | T |
| 95510 | * | T | T | * | * | * | T | * | T |
| 95511 | * | T | T | * | * | * | T | * | T |
| 95512 | * | T | T | * | * | * | T | * | T |
| 95513 | * | T | T | * | * | * | T | * | T |
| 95514 | * | T | T | * | * | * | T | * | T |
| 95515 | * | T | T | * | * | * | T | * | T |
| 95516 | * | T | T | * | * | * | T | * | T |
| 95517 | * | T | T | * | * | * | T | * | T |
| 95518 | * | T | T | * | * | * | T | * | T |
| 95519 | * | T | T | * | * | * | T | * | T |
| 95520 | * | T | T | * | * | * | T | * | T |
| 95521 | * | T | T | * | * | * | T | * | T |
| 95522 | * | T | T | * | * | * | T | * | T |
| 95523 | * | T | T | * | * | * | T | * | T |
| 95524 | * | T | T | * | * | * | T | * | T |
| 95525 | * | T | T | * | * | * | T | * | T |
| 95526 | * | T | T | * | * | * | T | * | T |
| 95527 | * | T | T | * | * | * | T | * | T |
| 95528 | * | T | T | * | * | * | T | * | T |
| 95529 | * | T | T | * | * | * | T | * | T |
| 95530 | * | T | T | * | * | * | T | * | T |
| 95531 | * | T | T | * | * | * | T | * | T |
| 97579 | * | T | T | * | * | * | T | * | T |
| 97580 | * | T | T | * | * | * | T | * | T |
| 99135 | * | T | T | * | * | * | F | F | F |
| 99136 | * | T | T | * | * | * | T | * | T |
| 99137 | * | T | T | * | * | * | T | * | T |
| 99138 | * | T | T | * | * | * | T | * | T |
| 99139 | * | T | T | * | * | * | T | * | T |
| 100618 | * | T | T | * | * | * | F | F | F |
| 100619 | * | T | T | * | * | * | T | * | T |
| 100620 | * | T | T | * | * | * | T | * | T |
| 100621 | * | T | T | * | * | * | T | * | T |
| 100622 | * | T | T | * | * | * | T | * | T |
| 102068 | * | T | T | * | * | * | F | F | F |
| 102069 | * | T | T | * | * | * | T | * | T |
| 102070 | * | T | T | * | * | * | T | * | T |
| 102071 | * | T | T | * | * | * | T | * | T |
| 102072 | * | T | T | * | * | * | T | * | T |
| 104601 | * | T | T | * | * | * | F | F | F |
| 104602 | * | T | T | * | * | * | T | * | T |
| 104603 | * | T | T | * | * | * | T | * | T |
| 104604 | * | T | T | * | * | * | T | * | T |
| 104605 | * | T | T | * | * | * | T | * | T |
| 104606 | * | T | T | * | * | * | T | * | T |
| 104607 | * | T | T | * | * | * | T | * | T |
| 108521 | * | T | T | * | * | * | F | F | F |
| 108522 | * | T | T | * | * | * | T | * | T |
| 108523 | * | T | T | * | * | * | T | * | T |
| 108524 | * | T | T | * | * | * | T | * | T |
| 108525 | * | T | T | * | * | * | T | * | T |
| 108526 | * | T | T | * | * | * | T | * | T |
| 108527 | * | T | T | * | * | * | T | * | T |
| 108528 | * | T | T | * | * | * | T | * | T |
| 108529 | * | T | T | * | * | * | T | * | T |
| 108530 | * | T | T | * | * | * | T | * | T |
| 108531 | * | T | T | * | * | * | T | * | T |
| 108532 | * | T | T | * | * | * | T | * | T |
| 108533 | * | T | T | * | * | * | T | * | T |
| 108534 | * | T | T | * | * | * | T | * | T |
| 108535 | * | T | T | * | * | * | T | * | T |
| 108536 | * | T | T | * | * | * | T | * | T |
| 108537 | * | T | T | * | * | * | T | * | T |
| 108538 | * | T | T | * | * | * | T | * | T |
| 108539 | * | T | T | * | * | * | T | * | T |
| 108540 | * | T | T | * | * | * | T | * | T |
| 108541 | * | T | T | * | * | * | T | * | T |
| 108542 | * | T | T | * | * | * | T | * | T |
| 108543 | * | T | T | * | * | * | T | * | T |
| 110586 | * | T | T | * | * | * | F | F | F |
| 110587 | * | T | T | * | * | * | T | * | T |
| 110588 | * | T | T | * | * | * | T | * | T |
| 110589 | * | T | T | * | * | * | T | * | T |
| 110590 | * | T | T | * | * | * | T | * | T |
| 113764 | * | T | T | * | * | * | F | F | F |
| 113765 | * | T | T | * | * | * | T | * | T |
| 113766 | * | T | T | * | * | * | T | * | T |
| 113767 | * | T | T | * | * | * | T | * | T |
| 113768 | * | T | T | * | * | * | T | * | T |
| 113769 | * | T | T | * | * | * | T | * | T |
| 113770 | * | T | T | * | * | * | T | * | T |
| 113771 | * | T | T | * | * | * | T | * | T |
| 113772 | * | T | T | * | * | * | T | * | T |
| 113773 | * | T | T | * | * | * | T | * | T |
| 113774 | * | T | T | * | * | * | T | * | T |
| 113775 | * | T | T | * | * | * | T | * | T |
| 113776 | * | T | T | * | * | * | T | * | T |
| 113777 | * | T | T | * | * | * | T | * | T |
| 113778 | * | T | T | * | * | * | T | * | T |
| 113779 | * | T | T | * | * | * | T | * | T |
| 113780 | * | T | T | * | * | * | T | * | T |
| 116992 | * | T | T | * | * | * | F | F | F |
| 116993 | * | T | T | * | * | * | T | * | T |
| 116994 | * | T | T | * | * | * | T | * | T |
| 116995 | * | T | T | * | * | * | T | * | T |
| 116996 | * | T | T | * | * | * | T | * | T |
| 116997 | * | T | T | * | * | * | T | * | T |
| 116998 | * | T | T | * | * | * | T | * | T |
| 116999 | * | T | T | * | * | * | T | * | T |
| 117000 | * | T | T | * | * | * | T | * | T |
| 117001 | * | T | T | * | * | * | T | * | T |
| 117002 | * | T | T | * | * | * | T | * | T |
| 139994 | * | T | T | * | * | * | F | F | F |
| 139995 | * | T | T | * | * | * | T | * | T |
| 139996 | * | T | T | * | * | * | T | * | T |
| 139997 | * | T | T | * | * | * | T | * | T |
| 139998 | * | T | T | * | * | * | T | * | T |
| 139999 | * | T | T | * | * | * | T | * | T |
| 140000 | * | T | T | * | * | * | T | * | T |
| 140001 | * | T | T | * | * | * | T | * | T |
| 162930 | * | T | T | * | * | * | F | F | F |
| 162931 | * | T | T | * | * | * | T | * | T |
| 162932 | * | T | T | * | * | * | T | * | T |
| 162933 | * | T | T | * | * | * | T | * | T |
| 162934 | * | T | T | * | * | * | T | * | T |
| 162935 | * | T | T | * | * | * | T | * | T |
| 162936 | * | T | T | * | * | * | T | * | T |
| 162937 | * | T | T | * | * | * | T | * | T |
| 164499 | * | T | T | * | * | * | F | F | F |
| 164500 | * | T | T | * | * | * | T | * | T |
| 164501 | * | T | T | * | * | * | T | * | T |
| 166166 | * | T | T | * | * | * | F | F | F |
| 166167 | * | T | T | * | * | * | T | * | T |
| 166168 | * | T | T | * | * | * | T | * | T |
| 167850 | * | T | T | * | * | * | F | F | F |
| 167851 | * | T | T | * | * | * | T | * | T |
| 167852 | * | T | T | * | * | * | T | * | T |
Independent-effect pairs
All 8 conditions live in realloc — 8 br_if
c0(branch8337): DEAD view gap →c1(branch8338): GAP view gap →c2(branch8339): GAP view gap →c3(branch8340): DEAD view gap →c4(branch8341): DEAD view gap →c5(branch8342): DEAD view gap →c6(branch8343): PROVED — pair rows3631,3633(masking)c7(branch8344): GAP view gap →