Decision #1433 — malloc.c:4798
Status: no_witness
Truth table
| row | c0 br 9505 | c1 br 9506 | c2 br 9507 | c3 br 9508 | outcome |
|---|---|---|---|---|---|
| 4484 | F | * | * | * | T |
| 4485 | F | * | * | * | T |
| 4486 | F | * | * | * | T |
| 11410 | F | * | * | * | T |
| 11411 | F | * | * | * | T |
| 11412 | F | * | * | * | T |
| 11413 | F | * | * | * | T |
| 18365 | F | * | * | * | T |
| 18366 | F | * | * | * | T |
| 18367 | F | * | * | * | T |
| 23018 | F | * | * | * | T |
| 23019 | F | * | * | * | T |
| 25737 | F | * | * | * | T |
| 25738 | F | * | * | * | T |
| 28404 | F | * | * | * | T |
| 28405 | F | * | * | * | T |
| 44215 | F | * | * | * | T |
| 44216 | F | * | * | * | T |
| 44217 | F | * | * | * | T |
| 44218 | F | * | * | * | T |
| 44219 | F | * | * | * | T |
| 44220 | F | * | * | * | T |
| 44221 | F | * | * | * | T |
| 44222 | F | * | * | * | T |
| 44223 | F | * | * | * | T |
| 44224 | F | * | * | * | T |
| 44225 | F | * | * | * | T |
| 44226 | F | * | * | * | T |
| 44227 | F | * | * | * | T |
| 44228 | F | * | * | * | T |
| 44229 | F | * | * | * | T |
| 44230 | F | * | * | * | T |
| 44231 | F | * | * | * | T |
| 44232 | F | * | * | * | T |
| 44233 | F | * | * | * | T |
| 44234 | F | * | * | * | T |
| 44235 | F | * | * | * | T |
| 44236 | F | * | * | * | T |
| 44237 | F | * | * | * | T |
| 44238 | F | * | * | * | T |
| 44239 | F | * | * | * | T |
| 44240 | F | * | * | * | T |
| 44241 | F | * | * | * | T |
| 44242 | F | * | * | * | T |
| 44243 | F | * | * | * | T |
| 44244 | F | * | * | * | T |
| 44245 | F | * | * | T | T |
| 44246 | F | * | * | T | T |
| 44247 | F | * | * | * | T |
| 65043 | F | * | * | * | T |
| 65044 | F | * | * | * | T |
| 65045 | F | * | * | * | T |
| 65046 | F | * | * | * | T |
| 65047 | F | * | * | * | T |
| 65048 | F | * | * | * | T |
| 65049 | F | * | * | * | T |
| 65050 | F | * | * | * | T |
| 65051 | F | * | * | * | T |
| 65052 | F | * | * | * | T |
| 65053 | F | * | * | * | T |
| 65054 | F | * | * | * | T |
| 65055 | F | * | * | * | T |
| 65056 | F | * | * | * | T |
| 65057 | F | * | * | * | T |
| 65058 | F | * | * | * | T |
| 65059 | F | * | * | * | T |
| 65060 | F | * | * | * | T |
| 65061 | F | * | * | * | T |
| 65062 | F | * | * | * | T |
| 65063 | F | * | * | * | T |
| 65064 | F | * | * | * | T |
| 65065 | F | * | * | * | T |
| 65066 | F | * | * | * | T |
| 65067 | F | * | * | * | T |
| 65068 | F | * | * | * | T |
| 65069 | F | * | * | * | T |
| 65070 | F | * | * | * | T |
| 65071 | F | * | * | * | T |
| 65072 | F | * | * | * | T |
| 65073 | F | * | * | T | T |
| 65074 | F | * | * | T | T |
| 77822 | F | * | * | * | T |
| 77823 | F | * | * | * | T |
| 77824 | F | * | * | * | T |
| 77825 | F | * | * | * | T |
| 77826 | F | * | * | * | T |
| 77827 | F | * | * | * | T |
| 77828 | F | * | * | * | T |
| 77829 | F | F | T | * | T |
| 77830 | F | * | * | * | T |
| 87705 | F | * | * | * | T |
| 87706 | F | * | * | * | T |
| 87707 | F | * | * | * | T |
| 87708 | F | * | * | * | T |
| 87709 | F | * | * | * | T |
| 87710 | F | * | * | * | T |
| 87711 | F | * | * | * | T |
| 87712 | F | F | T | * | T |
| 87713 | F | * | * | * | T |
| 95669 | F | * | * | T | T |
| 95670 | F | * | * | T | T |
| 95671 | F | * | * | * | T |
| 103742 | F | * | * | T | T |
| 103743 | F | * | * | T | T |
| 103744 | F | * | * | * | T |
| 112172 | F | * | * | T | T |
| 112173 | F | * | * | T | T |
| 112174 | F | * | * | * | T |
| 120013 | F | * | * | T | T |
| 120014 | F | * | * | T | T |
| 120015 | F | * | * | * | T |
| 135682 | F | * | * | * | T |
| 135683 | F | F | T | * | T |
| 135684 | F | * | * | * | T |
| 135685 | F | * | * | * | T |
| 135686 | F | * | * | T | T |
| 135687 | F | * | * | * | T |
| 135688 | F | * | * | * | T |
| 135689 | F | * | * | * | T |
| 135690 | F | * | * | * | T |
| 135691 | F | * | * | * | T |
| 135692 | F | * | * | * | T |
| 135693 | F | * | * | T | T |
| 135694 | F | * | * | T | T |
| 135695 | F | * | * | * | T |
| 135696 | F | * | * | * | T |
| 135697 | F | * | * | * | T |
| 135698 | F | * | * | * | T |
| 135699 | F | * | * | * | T |
| 135700 | F | * | * | * | T |
| 135701 | F | * | * | * | T |
| 135702 | F | * | * | * | T |
| 135703 | F | * | * | T | T |
| 135704 | F | * | * | * | T |
| 135705 | F | * | * | * | T |
| 135706 | F | * | * | T | T |
| 135707 | F | * | * | * | T |
| 135708 | F | * | * | * | T |
| 152401 | F | * | * | * | T |
| 152402 | F | F | T | * | T |
| 152403 | F | * | * | * | T |
| 152404 | F | * | * | * | T |
| 152405 | F | * | * | T | T |
| 152406 | F | * | * | * | T |
| 152407 | F | * | * | * | T |
| 152408 | F | * | * | * | T |
| 152409 | F | * | * | * | T |
| 152410 | F | * | * | * | T |
| 152411 | F | * | * | * | T |
| 152412 | F | * | * | T | T |
| 152413 | F | * | * | T | T |
| 152414 | F | * | * | * | T |
| 152415 | F | * | * | * | T |
| 152416 | F | * | * | * | T |
| 152417 | F | * | * | * | T |
| 152418 | F | * | * | * | T |
| 152419 | F | * | * | * | T |
| 152420 | F | * | * | * | T |
| 152421 | F | * | * | * | T |
| 152422 | F | * | * | T | T |
| 152423 | F | * | * | * | T |
| 152424 | F | * | * | * | T |
| 152425 | F | * | * | T | T |
| 152426 | F | * | * | * | T |
| 152427 | F | * | * | * | T |
| 162658 | F | * | * | * | T |
| 162659 | F | * | * | * | T |
| 162660 | F | * | * | * | T |
| 162661 | F | * | * | * | T |
| 172516 | F | * | * | * | T |
| 172517 | F | * | * | * | T |
| 172518 | F | * | * | * | T |
| 172519 | F | * | * | * | T |
| 178630 | F | * | * | * | T |
| 182698 | F | * | * | * | T |
| 182699 | F | * | * | * | T |
| 185905 | F | * | * | * | T |
| 185906 | F | * | * | * | T |
| 189125 | F | * | * | * | T |
| 189126 | F | * | * | * | T |
| 193482 | F | * | * | * | T |
| 193483 | F | * | * | * | T |
| 193484 | F | * | * | * | T |
| 193485 | F | * | * | * | T |
| 200457 | F | * | * | * | T |
| 200458 | F | * | * | * | T |
| 200459 | F | * | * | * | T |
| 200460 | F | * | * | * | T |
| 200461 | F | * | * | * | T |
| 200462 | F | * | * | * | T |
| 200463 | F | * | * | * | T |
| 205064 | F | * | * | * | T |
| 205065 | F | * | * | * | T |
| 205066 | F | * | * | * | T |
| 211568 | F | * | * | * | T |
| 211569 | F | * | * | * | T |
| 211570 | F | * | * | * | T |
| 211571 | F | * | * | * | T |
| 211572 | F | * | * | * | T |
| 211573 | F | * | * | * | T |
| 211574 | F | * | * | * | T |
| 211575 | F | * | * | * | T |
| 218946 | F | * | * | * | T |
| 218947 | F | * | * | * | T |
| 218948 | F | * | * | * | T |
| 218949 | F | * | * | * | T |
| 218950 | F | * | * | * | T |
| 274593 | F | * | * | * | T |
| 274594 | F | * | * | * | T |
| 274595 | F | * | * | * | T |
| 274596 | F | * | * | * | T |
| 274597 | F | * | * | * | T |
| 274598 | F | * | * | * | T |
| 274599 | F | * | * | * | T |
| 274600 | F | * | * | T | T |
| 274601 | F | * | * | * | T |
| 274602 | F | * | * | * | T |
| 274603 | F | * | * | * | T |
| 274604 | F | * | * | * | T |
| 274605 | F | * | * | * | T |
| 274606 | F | * | * | * | T |
| 274607 | F | * | * | * | T |
| 274608 | F | * | * | * | T |
| 274609 | F | * | * | * | T |
| 274610 | F | * | * | * | T |
| 274611 | F | * | * | * | T |
| 274612 | F | * | * | * | T |
| 274613 | F | * | * | * | T |
| 274614 | F | * | * | * | T |
| 274615 | F | * | * | * | T |
| 274616 | F | * | * | * | T |
| 274617 | F | * | * | * | T |
| 274618 | F | * | * | * | T |
| 274619 | F | * | * | * | T |
| 274620 | F | * | * | * | T |
| 274621 | F | * | * | * | T |
| 274622 | F | * | * | * | T |
| 274623 | F | * | * | * | T |
| 274624 | F | * | * | * | T |
| 274625 | F | * | * | * | T |
| 274626 | F | * | * | * | T |
| 274627 | F | * | * | * | T |
| 274628 | F | * | * | * | T |
| 274629 | F | F | T | * | T |
| 274630 | F | F | T | * | T |
| 274631 | F | * | * | * | T |
| 274632 | F | * | * | * | T |
| 274633 | F | * | * | * | T |
| 274634 | F | * | * | * | T |
| 274635 | F | * | * | F | T |
| 274636 | F | * | * | T | T |
| 274637 | F | * | * | * | T |
| 274638 | F | * | * | * | T |
| 274639 | F | * | * | * | T |
| 274640 | F | * | * | * | T |
| 274641 | F | * | * | * | T |
| 274642 | F | * | * | * | T |
| 274643 | F | * | * | * | T |
| 274644 | F | * | * | * | T |
| 274645 | F | * | * | * | T |
| 274646 | F | * | * | * | T |
| 274647 | F | * | * | * | T |
| 274648 | F | * | * | * | T |
| 274649 | F | * | * | * | T |
| 274650 | F | * | * | * | T |
| 274651 | F | * | * | * | T |
| 274652 | F | * | * | * | T |
| 274653 | F | * | * | * | T |
| 274654 | F | * | * | * | T |
| 274655 | F | * | * | * | T |
| 274656 | F | * | * | * | T |
| 274657 | F | * | * | * | T |
| 274658 | F | * | * | T | T |
| 274659 | F | * | * | * | T |
| 274660 | F | * | * | * | T |
| 274661 | F | * | * | * | T |
| 274662 | F | * | * | * | T |
| 274663 | F | * | * | * | T |
| 274664 | F | * | * | * | T |
| 274665 | F | F | F | T | T |
| 274666 | F | * | * | * | T |
| 274667 | F | * | * | T | T |
| 274668 | F | * | * | * | T |
| 274669 | F | * | * | * | T |
| 274670 | F | * | * | * | T |
| 274671 | F | * | * | * | T |
| 274672 | F | * | * | * | T |
| 274673 | F | * | * | * | T |
| 274674 | F | * | * | * | T |
| 274675 | F | * | * | * | T |
| 274676 | F | * | * | * | T |
| 274677 | F | * | * | * | T |
| 274678 | F | * | * | * | T |
| 274679 | F | * | * | * | T |
| 274680 | F | * | * | * | T |
| 274681 | F | * | * | * | T |
| 274682 | F | * | * | * | T |
| 274683 | F | * | * | * | T |
| 274684 | F | * | * | * | T |
| 274685 | F | * | * | * | T |
| 274686 | F | * | * | * | T |
| 274687 | F | * | * | * | T |
| 274688 | F | * | * | * | T |
| 274689 | F | * | * | * | T |
| 274690 | F | * | * | * | T |
| 274691 | F | * | * | * | T |
| 274692 | F | * | * | * | T |
| 274693 | F | * | * | * | T |
| 274694 | F | * | * | * | T |
| 274695 | F | * | * | * | T |
| 274696 | F | * | * | T | T |
| 274697 | F | * | * | * | T |
| 274698 | F | * | * | * | T |
| 274699 | F | * | * | * | T |
| 274700 | F | * | * | * | T |
| 274701 | F | * | * | * | T |
| 274702 | F | * | * | * | T |
| 274703 | F | * | * | * | T |
| 274704 | F | * | * | * | T |
| 274705 | F | * | * | * | T |
| 274706 | F | F | T | * | T |
| 274707 | F | * | * | * | T |
| 274708 | F | * | * | * | T |
| 274709 | F | * | * | * | T |
| 274710 | F | * | * | * | T |
| 274711 | F | * | * | * | T |
| 274712 | F | * | * | * | T |
| 274713 | F | * | * | * | T |
| 274714 | F | * | * | * | T |
| 274715 | F | * | * | * | T |
| 274716 | F | * | * | T | T |
| 274717 | F | * | * | * | T |
| 274718 | F | * | * | * | T |
| 274719 | F | * | * | * | T |
| 274720 | F | * | * | * | T |
| 274721 | F | F | T | * | T |
| 274722 | F | * | * | * | T |
| 274723 | F | * | * | T | T |
| 274724 | F | * | * | T | T |
| 274725 | F | * | * | * | T |
| 274726 | F | * | * | T | T |
| 274727 | F | * | * | * | T |
| 274728 | F | * | * | * | T |
| 274729 | F | * | * | * | T |
| 274730 | F | * | * | * | T |
| 274731 | F | * | * | * | T |
| 274732 | F | * | * | * | T |
| 274733 | F | * | * | T | T |
| 274734 | F | * | * | * | T |
| 274735 | F | * | * | * | T |
| 274736 | F | * | * | * | T |
| 274737 | F | * | * | * | T |
| 274738 | F | * | * | * | T |
| 274739 | F | * | * | T | T |
| 274740 | F | * | * | * | T |
| 274741 | F | * | * | * | T |
| 274742 | F | * | * | * | T |
| 274743 | F | * | * | * | T |
| 274744 | F | * | * | * | T |
| 274745 | F | * | * | * | T |
| 274746 | F | * | * | * | T |
| 274747 | F | * | * | * | T |
| 274748 | F | * | * | * | T |
| 274749 | F | * | * | T | T |
| 274750 | F | * | * | * | T |
| 274751 | F | * | * | T | T |
| 274752 | F | * | * | * | T |
| 274753 | F | * | * | * | T |
| 274754 | F | F | T | * | T |
| 274755 | F | * | * | * | T |
| 274756 | F | * | * | * | T |
| 274757 | F | * | * | * | T |
| 274758 | F | * | * | * | T |
| 274759 | F | * | * | * | T |
| 274760 | F | * | * | * | T |
| 274761 | F | * | * | * | T |
| 274762 | F | * | * | * | T |
| 274763 | F | * | * | * | T |
| 274764 | F | * | * | * | T |
| 274765 | F | * | * | * | T |
| 274766 | F | * | * | * | T |
| 274767 | F | * | * | * | T |
| 274768 | F | * | * | * | T |
| 274769 | F | F | F | T | T |
| 274770 | F | F | T | * | T |
| 274771 | F | * | * | * | T |
| 351970 | F | * | * | * | T |
| 351971 | F | * | * | * | T |
| 351972 | F | * | * | * | T |
| 351973 | F | * | * | * | T |
| 351974 | F | * | * | * | T |
| 351975 | F | * | * | * | T |
| 351976 | F | * | * | * | T |
| 351977 | F | * | * | T | T |
| 351978 | F | * | * | * | T |
| 351979 | F | * | * | * | T |
| 351980 | F | * | * | * | T |
| 351981 | F | * | * | * | T |
| 351982 | F | * | * | * | T |
| 351983 | F | * | * | * | T |
| 351984 | F | * | * | * | T |
| 351985 | F | * | * | * | T |
| 351986 | F | * | * | * | T |
| 351987 | F | * | * | * | T |
| 351988 | F | * | * | * | T |
| 351989 | F | * | * | * | T |
| 351990 | F | * | * | * | T |
| 351991 | F | * | * | * | T |
| 351992 | F | * | * | * | T |
| 351993 | F | * | * | * | T |
| 351994 | F | * | * | * | T |
| 351995 | F | * | * | * | T |
| 351996 | F | * | * | * | T |
| 351997 | F | * | * | * | T |
| 351998 | F | * | * | * | T |
| 351999 | F | * | * | * | T |
| 352000 | F | * | * | * | T |
| 352001 | F | * | * | * | T |
| 352002 | F | * | * | * | T |
| 352003 | F | * | * | * | T |
| 352004 | F | * | * | * | T |
| 352005 | F | * | * | * | T |
| 352006 | F | F | T | * | T |
| 352007 | F | F | T | * | T |
| 352008 | F | * | * | * | T |
| 352009 | F | * | * | * | T |
| 352010 | F | * | * | * | T |
| 352011 | F | * | * | * | T |
| 352012 | F | * | * | F | T |
| 352013 | F | * | * | T | T |
| 352014 | F | * | * | * | T |
| 352015 | F | * | * | * | T |
| 352016 | F | * | * | * | T |
| 352017 | F | * | * | * | T |
| 352018 | F | * | * | * | T |
| 352019 | F | * | * | * | T |
| 352020 | F | * | * | * | T |
| 352021 | F | * | * | * | T |
| 352022 | F | * | * | * | T |
| 352023 | F | * | * | * | T |
| 352024 | F | * | * | * | T |
| 352025 | F | * | * | * | T |
| 352026 | F | * | * | * | T |
| 352027 | F | * | * | * | T |
| 352028 | F | * | * | * | T |
| 352029 | F | * | * | * | T |
| 352030 | F | * | * | * | T |
| 352031 | F | * | * | * | T |
| 352032 | F | * | * | * | T |
| 352033 | F | * | * | * | T |
| 352034 | F | * | * | * | T |
| 352035 | F | * | * | T | T |
| 352036 | F | * | * | * | T |
| 352037 | F | * | * | * | T |
| 352038 | F | * | * | * | T |
| 352039 | F | * | * | * | T |
| 352040 | F | * | * | * | T |
| 352041 | F | * | * | * | T |
| 352042 | F | F | F | T | T |
| 352043 | F | * | * | * | T |
| 352044 | F | * | * | T | T |
| 352045 | F | * | * | * | T |
| 352046 | F | * | * | * | T |
| 352047 | F | * | * | * | T |
| 352048 | F | * | * | * | T |
| 352049 | F | * | * | * | T |
| 352050 | F | * | * | * | T |
| 352051 | F | * | * | * | T |
| 352052 | F | * | * | * | T |
| 352053 | F | * | * | * | T |
| 352054 | F | * | * | * | T |
| 352055 | F | * | * | * | T |
| 352056 | F | * | * | * | T |
| 352057 | F | * | * | * | T |
| 352058 | F | * | * | * | T |
| 352059 | F | * | * | * | T |
| 352060 | F | * | * | * | T |
| 352061 | F | * | * | * | T |
| 352062 | F | * | * | * | T |
| 352063 | F | * | * | * | T |
| 352064 | F | * | * | * | T |
| 352065 | F | * | * | * | T |
| 352066 | F | * | * | * | T |
| 352067 | F | * | * | * | T |
| 352068 | F | * | * | * | T |
| 352069 | F | * | * | * | T |
| 352070 | F | * | * | * | T |
| 352071 | F | * | * | * | T |
| 352072 | F | * | * | * | T |
| 352073 | F | * | * | T | T |
| 352074 | F | * | * | * | T |
| 352075 | F | * | * | * | T |
| 352076 | F | * | * | * | T |
| 352077 | F | * | * | * | T |
| 352078 | F | * | * | * | T |
| 352079 | F | * | * | * | T |
| 352080 | F | * | * | * | T |
| 352081 | F | * | * | * | T |
| 352082 | F | * | * | * | T |
| 352083 | F | F | T | * | T |
| 352084 | F | * | * | * | T |
| 352085 | F | * | * | * | T |
| 352086 | F | * | * | * | T |
| 352087 | F | * | * | * | T |
| 352088 | F | * | * | * | T |
| 352089 | F | * | * | * | T |
| 352090 | F | * | * | * | T |
| 352091 | F | * | * | * | T |
| 352092 | F | * | * | * | T |
| 352093 | F | * | * | T | T |
| 352094 | F | * | * | * | T |
| 352095 | F | * | * | * | T |
| 352096 | F | * | * | * | T |
| 352097 | F | * | * | * | T |
| 352098 | F | F | T | * | T |
| 352099 | F | * | * | * | T |
| 352100 | F | * | * | T | T |
| 352101 | F | * | * | T | T |
| 352102 | F | * | * | * | T |
| 352103 | F | * | * | T | T |
| 352104 | F | * | * | * | T |
| 352105 | F | * | * | * | T |
| 352106 | F | * | * | * | T |
| 352107 | F | * | * | * | T |
| 352108 | F | * | * | * | T |
| 352109 | F | * | * | * | T |
| 352110 | F | * | * | T | T |
| 352111 | F | * | * | * | T |
| 352112 | F | * | * | * | T |
| 352113 | F | * | * | * | T |
| 352114 | F | * | * | * | T |
| 352115 | F | * | * | * | T |
| 352116 | F | * | * | T | T |
| 352117 | F | * | * | * | T |
| 352118 | F | * | * | * | T |
| 352119 | F | * | * | * | T |
| 352120 | F | * | * | * | T |
| 352121 | F | * | * | * | T |
| 352122 | F | * | * | * | T |
| 352123 | F | * | * | * | T |
| 352124 | F | * | * | * | T |
| 352125 | F | * | * | * | T |
| 352126 | F | * | * | T | T |
| 352127 | F | * | * | * | T |
| 352128 | F | * | * | T | T |
| 352129 | F | * | * | * | T |
| 352130 | F | * | * | * | T |
| 352131 | F | F | T | * | T |
| 352132 | F | * | * | * | T |
| 352133 | F | * | * | * | T |
| 352134 | F | * | * | * | T |
| 352135 | F | * | * | * | T |
| 352136 | F | * | * | * | T |
| 352137 | F | * | * | * | T |
| 352138 | F | * | * | * | T |
| 352139 | F | * | * | * | T |
| 352140 | F | * | * | * | T |
| 352141 | F | * | * | * | T |
| 352142 | F | * | * | * | T |
| 352143 | F | * | * | * | T |
| 352144 | F | * | * | * | T |
| 352145 | F | * | * | * | T |
| 352146 | F | F | F | T | T |
| 352147 | F | F | T | * | T |
| 352148 | F | * | * | * | T |
| 378479 | F | * | * | T | T |
| 381214 | F | * | * | T | T |
| 384075 | F | * | * | T | T |
Independent-effect pairs
All 4 conditions live in dlmalloc — 4 br_if
c0(branch9505): GAP view gap →c1(branch9506): GAP view gap →c2(branch9507): GAP view gap →c3(branch9508): GAP view gap →