Decision #1434 — malloc.c:4803
Status: no_witness
Truth table
| row | c0 br 9510 | c1 br 9511 | c2 br 9512 | outcome |
|---|---|---|---|---|
| 4487 | T | F | T | T |
| 4488 | T | T | * | T |
| 4489 | T | F | T | T |
| 11414 | T | F | T | T |
| 11415 | T | T | * | T |
| 11416 | T | F | F | T |
| 11417 | T | T | * | T |
| 18368 | T | F | T | T |
| 18369 | T | T | * | T |
| 18370 | T | F | T | T |
| 23020 | T | T | * | T |
| 23021 | T | T | * | T |
| 25739 | T | T | * | T |
| 25740 | T | F | F | T |
| 28406 | T | T | * | T |
| 28407 | T | T | * | T |
| 44248 | T | T | * | T |
| 44249 | T | T | * | T |
| 44250 | T | T | * | T |
| 44251 | T | T | * | T |
| 44252 | T | F | F | T |
| 44253 | T | F | F | T |
| 44254 | T | F | F | T |
| 44255 | T | T | * | T |
| 44256 | T | T | * | T |
| 44257 | T | T | * | T |
| 44258 | T | F | F | T |
| 44259 | T | F | * | T |
| 44260 | T | F | F | T |
| 44261 | T | T | * | T |
| 44262 | T | T | * | T |
| 44263 | T | F | T | T |
| 44264 | T | F | T | T |
| 44265 | T | F | T | T |
| 44266 | T | F | F | T |
| 44267 | T | F | F | T |
| 44268 | T | F | T | T |
| 44269 | T | F | F | T |
| 44270 | T | T | * | T |
| 44271 | T | T | * | T |
| 44272 | T | T | * | T |
| 44273 | T | F | F | T |
| 44274 | T | T | * | T |
| 44275 | T | F | F | T |
| 44276 | T | F | F | T |
| 44277 | T | F | F | T |
| 44278 | T | F | F | T |
| 44279 | T | F | F | T |
| 44280 | T | F | F | T |
| 44281 | T | T | * | T |
| 44282 | T | F | F | T |
| 65075 | T | T | * | T |
| 65076 | T | T | * | T |
| 65077 | T | T | * | T |
| 65078 | T | T | * | T |
| 65079 | T | F | F | T |
| 65080 | T | F | F | T |
| 65081 | T | F | F | T |
| 65082 | T | T | * | T |
| 65083 | T | T | * | T |
| 65084 | T | T | * | T |
| 65085 | T | F | F | T |
| 65086 | T | F | * | T |
| 65087 | T | F | F | T |
| 65088 | T | T | * | T |
| 65089 | T | T | * | T |
| 65090 | T | F | T | T |
| 65091 | T | F | T | T |
| 65092 | T | F | T | T |
| 65093 | T | F | F | T |
| 65094 | T | F | F | T |
| 65095 | T | F | T | T |
| 65096 | T | F | F | T |
| 65097 | T | T | * | T |
| 65098 | T | T | * | T |
| 65099 | T | T | * | T |
| 65100 | T | F | F | T |
| 65101 | T | T | * | T |
| 65102 | T | F | F | T |
| 65103 | T | F | F | T |
| 65104 | T | F | F | T |
| 65105 | T | F | F | T |
| 65106 | T | F | F | T |
| 65107 | T | F | F | T |
| 65108 | T | T | * | T |
| 77831 | T | T | * | T |
| 77832 | T | T | * | T |
| 77833 | T | F | F | T |
| 77834 | T | T | * | T |
| 77835 | T | T | * | T |
| 77836 | T | T | * | T |
| 77837 | T | T | * | T |
| 77838 | T | T | * | T |
| 77839 | T | F | F | T |
| 77840 | T | F | F | T |
| 87714 | T | T | * | T |
| 87715 | T | T | * | T |
| 87716 | T | F | F | T |
| 87717 | T | T | * | T |
| 87718 | T | T | * | T |
| 87719 | T | T | * | T |
| 87720 | T | T | * | T |
| 87721 | T | T | * | T |
| 87722 | T | F | F | T |
| 87723 | T | F | F | T |
| 95672 | T | F | T | T |
| 95673 | T | T | * | T |
| 95674 | T | F | F | T |
| 95675 | T | F | F | T |
| 95676 | T | F | F | T |
| 103745 | T | F | T | T |
| 103746 | T | T | * | T |
| 103747 | T | F | F | T |
| 103748 | T | F | F | T |
| 103749 | T | F | F | T |
| 112175 | T | F | T | T |
| 112176 | T | T | * | T |
| 112177 | T | F | F | T |
| 112178 | T | F | F | T |
| 112179 | T | F | F | T |
| 120016 | T | F | T | T |
| 120017 | T | T | * | T |
| 120018 | T | F | F | T |
| 120019 | T | F | F | T |
| 120020 | T | F | F | T |
| 135709 | T | F | T | T |
| 135710 | T | F | T | T |
| 135711 | T | F | F | T |
| 135712 | T | F | F | T |
| 135713 | T | F | T | T |
| 135714 | T | F | F | T |
| 135715 | T | T | * | T |
| 135716 | T | F | T | T |
| 135717 | T | F | T | T |
| 135718 | T | F | T | T |
| 135719 | T | F | F | T |
| 135720 | T | F | F | T |
| 135721 | T | F | F | T |
| 135722 | T | T | * | T |
| 135723 | T | F | F | T |
| 135724 | T | T | * | T |
| 135725 | T | F | F | T |
| 135726 | T | T | * | T |
| 135727 | T | F | F | T |
| 135728 | T | F | F | T |
| 135729 | T | F | T | T |
| 135730 | T | F | F | T |
| 135731 | T | F | F | T |
| 135732 | T | F | F | T |
| 135733 | T | T | * | T |
| 135734 | T | T | * | T |
| 135735 | T | F | T | T |
| 135736 | T | F | F | T |
| 135737 | T | F | F | T |
| 135738 | T | F | F | T |
| 135739 | T | T | * | T |
| 135740 | T | F | F | T |
| 135741 | T | F | F | T |
| 152428 | T | F | T | T |
| 152429 | T | F | T | T |
| 152430 | T | F | F | T |
| 152431 | T | F | F | T |
| 152432 | T | F | T | T |
| 152433 | T | F | F | T |
| 152434 | T | T | * | T |
| 152435 | T | F | T | T |
| 152436 | T | F | T | T |
| 152437 | T | F | T | T |
| 152438 | T | F | F | T |
| 152439 | T | F | F | T |
| 152440 | T | F | F | T |
| 152441 | T | T | * | T |
| 152442 | T | F | F | T |
| 152443 | T | T | * | T |
| 152444 | T | F | F | T |
| 152445 | T | T | * | T |
| 152446 | T | F | F | T |
| 152447 | T | F | F | T |
| 152448 | T | F | T | T |
| 152449 | T | F | F | T |
| 152450 | T | F | F | T |
| 152451 | T | F | F | T |
| 152452 | T | T | * | T |
| 152453 | T | T | * | T |
| 152454 | T | F | T | T |
| 152455 | T | F | F | T |
| 152456 | T | F | F | T |
| 152457 | T | F | F | T |
| 152458 | T | T | * | T |
| 152459 | T | F | F | T |
| 152460 | T | F | F | T |
| 162662 | T | T | * | T |
| 162663 | T | T | * | T |
| 162664 | T | F | T | T |
| 162665 | T | F | T | T |
| 172520 | T | T | * | T |
| 172521 | T | T | * | T |
| 172522 | T | F | T | T |
| 172523 | T | F | T | T |
| 178631 | T | T | * | T |
| 182700 | T | T | * | T |
| 182701 | T | T | * | T |
| 185907 | T | T | * | T |
| 185908 | T | F | F | T |
| 189127 | T | T | * | T |
| 189128 | T | T | * | T |
| 193486 | T | T | * | T |
| 193487 | T | T | * | T |
| 193488 | T | F | F | T |
| 193489 | T | T | * | T |
| 200464 | T | F | F | T |
| 200465 | T | T | * | T |
| 200466 | T | T | * | T |
| 200467 | T | F | T | T |
| 200468 | T | T | * | T |
| 200469 | T | F | F | T |
| 200470 | T | F | F | T |
| 205067 | T | T | * | T |
| 205068 | T | T | * | T |
| 205069 | T | F | T | T |
| 211576 | T | T | * | T |
| 211577 | T | F | F | T |
| 211578 | T | T | * | T |
| 211579 | T | F | F | T |
| 211580 | T | F | T | T |
| 211581 | T | T | * | T |
| 211582 | T | T | * | T |
| 211583 | T | T | * | T |
| 218951 | T | T | * | T |
| 218952 | T | F | F | T |
| 218953 | T | F | F | T |
| 218954 | T | F | F | T |
| 218955 | T | F | F | T |
| 274772 | T | T | * | T |
| 274773 | T | T | * | T |
| 274774 | T | F | F | T |
| 274775 | T | F | * | T |
| 274776 | T | F | T | T |
| 274777 | T | F | T | T |
| 274778 | T | T | * | T |
| 274779 | T | T | * | T |
| 274780 | T | F | F | T |
| 274781 | T | F | F | T |
| 274782 | T | T | * | T |
| 274783 | T | F | T | T |
| 274784 | T | T | * | T |
| 274785 | T | T | * | T |
| 274786 | T | F | F | T |
| 274787 | T | T | * | T |
| 274788 | T | T | * | T |
| 274789 | T | F | T | T |
| 274790 | T | F | T | T |
| 274791 | T | T | * | T |
| 274792 | T | T | * | T |
| 274793 | T | F | F | T |
| 274794 | T | F | F | T |
| 274795 | T | T | * | T |
| 274796 | T | T | * | T |
| 274797 | T | T | * | T |
| 274798 | T | F | F | T |
| 274799 | T | F | F | T |
| 274800 | T | F | F | T |
| 274801 | T | F | F | T |
| 274802 | T | F | F | T |
| 274803 | T | F | F | T |
| 274804 | T | F | F | T |
| 274805 | T | F | F | T |
| 274806 | T | F | F | T |
| 274807 | T | F | F | T |
| 274808 | T | F | F | T |
| 274809 | T | F | T | T |
| 274810 | T | F | F | T |
| 274811 | T | F | T | T |
| 274812 | T | F | T | T |
| 274813 | T | F | T | T |
| 274814 | T | F | T | T |
| 274815 | T | F | F | T |
| 274816 | T | F | F | T |
| 274817 | T | T | * | T |
| 274818 | T | F | F | T |
| 274819 | T | F | F | T |
| 274820 | T | F | F | T |
| 274821 | T | F | * | T |
| 274822 | T | F | F | T |
| 274823 | T | T | * | T |
| 274824 | T | F | * | T |
| 274825 | T | F | T | T |
| 274826 | T | F | F | T |
| 274827 | T | F | T | T |
| 274828 | T | F | F | T |
| 274829 | T | F | F | T |
| 274830 | T | F | F | T |
| 274831 | T | F | F | T |
| 274832 | T | T | * | T |
| 274833 | T | T | * | T |
| 274834 | T | F | F | T |
| 274835 | T | F | F | T |
| 274836 | T | T | * | T |
| 274837 | T | T | * | T |
| 274838 | T | T | * | T |
| 274839 | T | T | * | T |
| 274840 | T | T | * | T |
| 274841 | T | F | * | T |
| 274842 | T | F | F | T |
| 274843 | T | F | F | T |
| 274844 | T | F | F | T |
| 274845 | T | F | T | T |
| 274846 | T | F | T | T |
| 274847 | T | T | * | T |
| 274848 | T | T | * | T |
| 274849 | T | T | * | T |
| 274850 | T | T | * | T |
| 274851 | T | F | F | T |
| 274852 | T | F | F | T |
| 274853 | T | T | * | T |
| 274854 | T | F | T | T |
| 274855 | T | F | F | T |
| 274856 | T | F | F | T |
| 274857 | T | T | * | T |
| 274858 | T | F | T | T |
| 274859 | T | T | * | T |
| 274860 | T | T | * | T |
| 274861 | T | F | T | T |
| 274862 | T | F | T | T |
| 274863 | T | F | T | T |
| 274864 | T | F | T | T |
| 274865 | T | F | T | T |
| 274866 | T | F | F | T |
| 274867 | T | F | T | T |
| 274868 | T | F | T | T |
| 274869 | T | F | T | T |
| 274870 | T | F | T | T |
| 274871 | T | F | T | T |
| 274872 | T | T | * | T |
| 274873 | T | T | * | T |
| 274874 | T | T | * | T |
| 274875 | T | F | F | T |
| 274876 | T | F | T | T |
| 274877 | T | F | T | T |
| 274878 | T | F | F | T |
| 274879 | T | F | T | T |
| 274880 | T | F | T | T |
| 274881 | T | T | * | T |
| 274882 | T | T | * | T |
| 274883 | T | F | T | T |
| 274884 | T | F | F | T |
| 274885 | T | F | F | T |
| 274886 | T | F | T | T |
| 274887 | T | F | T | T |
| 274888 | T | F | T | T |
| 274889 | T | F | T | T |
| 274890 | T | T | * | T |
| 274891 | T | T | * | T |
| 274892 | T | F | T | T |
| 274893 | T | F | T | T |
| 274894 | T | F | T | T |
| 274895 | T | F | T | T |
| 274896 | T | F | F | T |
| 274897 | T | T | * | T |
| 274898 | T | T | * | T |
| 274899 | T | F | F | T |
| 274900 | T | T | * | T |
| 274901 | T | T | * | T |
| 274902 | T | T | * | T |
| 274903 | T | F | T | T |
| 274904 | T | F | F | T |
| 274905 | T | F | T | T |
| 274906 | T | F | F | T |
| 274907 | T | F | F | T |
| 274908 | T | T | * | T |
| 274909 | T | F | F | T |
| 274910 | T | F | F | T |
| 274911 | T | F | F | T |
| 274912 | T | F | T | T |
| 274913 | T | F | T | T |
| 274914 | T | F | F | T |
| 274915 | T | F | T | T |
| 274916 | T | F | F | T |
| 274917 | T | F | F | T |
| 274918 | T | F | F | T |
| 274919 | T | F | T | T |
| 274920 | T | F | T | T |
| 274921 | T | F | F | T |
| 274922 | T | T | * | T |
| 274923 | T | F | F | T |
| 274924 | T | F | F | T |
| 274925 | T | F | F | T |
| 274926 | T | T | * | T |
| 274927 | T | T | * | T |
| 274928 | T | F | F | T |
| 274929 | T | F | T | T |
| 274930 | T | F | T | T |
| 274931 | T | F | F | T |
| 274932 | T | T | * | T |
| 274933 | T | F | F | T |
| 274934 | T | F | F | T |
| 274935 | T | F | * | T |
| 274936 | T | F | T | T |
| 274937 | T | F | F | T |
| 274938 | T | F | * | T |
| 274939 | T | F | * | T |
| 274940 | T | T | * | T |
| 274941 | T | T | * | T |
| 274942 | T | F | * | T |
| 274943 | T | F | T | T |
| 274944 | T | T | * | T |
| 274945 | T | F | * | T |
| 274946 | T | F | T | T |
| 274947 | T | F | F | T |
| 274948 | T | F | T | T |
| 274949 | T | T | * | T |
| 274950 | T | T | * | T |
| 274951 | T | F | F | T |
| 274952 | T | F | T | T |
| 274953 | T | F | T | T |
| 274954 | T | T | * | T |
| 274955 | T | F | T | T |
| 274956 | T | T | * | T |
| 274957 | T | T | * | T |
| 274958 | T | F | F | T |
| 274959 | T | F | T | T |
| 274960 | T | F | T | T |
| 274961 | T | F | * | T |
| 274962 | T | F | T | T |
| 274963 | T | F | F | T |
| 274964 | T | F | F | T |
| 274965 | T | F | F | T |
| 274966 | T | F | F | T |
| 274967 | T | T | * | T |
| 274968 | T | F | F | T |
| 274969 | T | F | F | T |
| 274970 | T | F | T | T |
| 274971 | T | T | * | T |
| 274972 | T | F | F | T |
| 352149 | T | T | * | T |
| 352150 | T | T | * | T |
| 352151 | T | F | F | T |
| 352152 | T | F | * | T |
| 352153 | T | F | T | T |
| 352154 | T | F | T | T |
| 352155 | T | T | * | T |
| 352156 | T | T | * | T |
| 352157 | T | F | F | T |
| 352158 | T | F | F | T |
| 352159 | T | T | * | T |
| 352160 | T | F | T | T |
| 352161 | T | T | * | T |
| 352162 | T | T | * | T |
| 352163 | T | F | F | T |
| 352164 | T | T | * | T |
| 352165 | T | T | * | T |
| 352166 | T | F | T | T |
| 352167 | T | F | T | T |
| 352168 | T | T | * | T |
| 352169 | T | T | * | T |
| 352170 | T | F | F | T |
| 352171 | T | F | F | T |
| 352172 | T | T | * | T |
| 352173 | T | T | * | T |
| 352174 | T | T | * | T |
| 352175 | T | F | F | T |
| 352176 | T | F | F | T |
| 352177 | T | F | F | T |
| 352178 | T | F | F | T |
| 352179 | T | F | F | T |
| 352180 | T | F | F | T |
| 352181 | T | F | F | T |
| 352182 | T | F | F | T |
| 352183 | T | F | F | T |
| 352184 | T | F | F | T |
| 352185 | T | F | F | T |
| 352186 | T | F | T | T |
| 352187 | T | F | F | T |
| 352188 | T | F | T | T |
| 352189 | T | F | T | T |
| 352190 | T | F | T | T |
| 352191 | T | F | T | T |
| 352192 | T | F | F | T |
| 352193 | T | F | F | T |
| 352194 | T | T | * | T |
| 352195 | T | F | F | T |
| 352196 | T | F | F | T |
| 352197 | T | F | F | T |
| 352198 | T | F | * | T |
| 352199 | T | F | F | T |
| 352200 | T | T | * | T |
| 352201 | T | F | * | T |
| 352202 | T | F | T | T |
| 352203 | T | F | F | T |
| 352204 | T | F | T | T |
| 352205 | T | F | F | T |
| 352206 | T | F | F | T |
| 352207 | T | F | F | T |
| 352208 | T | F | F | T |
| 352209 | T | T | * | T |
| 352210 | T | T | * | T |
| 352211 | T | F | F | T |
| 352212 | T | F | F | T |
| 352213 | T | T | * | T |
| 352214 | T | T | * | T |
| 352215 | T | T | * | T |
| 352216 | T | T | * | T |
| 352217 | T | T | * | T |
| 352218 | T | F | * | T |
| 352219 | T | F | F | T |
| 352220 | T | F | F | T |
| 352221 | T | F | F | T |
| 352222 | T | F | T | T |
| 352223 | T | F | T | T |
| 352224 | T | T | * | T |
| 352225 | T | T | * | T |
| 352226 | T | T | * | T |
| 352227 | T | T | * | T |
| 352228 | T | F | F | T |
| 352229 | T | F | F | T |
| 352230 | T | T | * | T |
| 352231 | T | F | T | T |
| 352232 | T | F | F | T |
| 352233 | T | F | F | T |
| 352234 | T | T | * | T |
| 352235 | T | F | T | T |
| 352236 | T | T | * | T |
| 352237 | T | T | * | T |
| 352238 | T | F | T | T |
| 352239 | T | F | T | T |
| 352240 | T | F | T | T |
| 352241 | T | F | T | T |
| 352242 | T | F | T | T |
| 352243 | T | F | F | T |
| 352244 | T | F | T | T |
| 352245 | T | F | T | T |
| 352246 | T | F | T | T |
| 352247 | T | F | T | T |
| 352248 | T | F | T | T |
| 352249 | T | T | * | T |
| 352250 | T | T | * | T |
| 352251 | T | T | * | T |
| 352252 | T | F | F | T |
| 352253 | T | F | T | T |
| 352254 | T | F | T | T |
| 352255 | T | F | F | T |
| 352256 | T | F | T | T |
| 352257 | T | F | T | T |
| 352258 | T | T | * | T |
| 352259 | T | T | * | T |
| 352260 | T | F | T | T |
| 352261 | T | F | F | T |
| 352262 | T | F | F | T |
| 352263 | T | F | T | T |
| 352264 | T | F | T | T |
| 352265 | T | F | T | T |
| 352266 | T | F | T | T |
| 352267 | T | T | * | T |
| 352268 | T | T | * | T |
| 352269 | T | F | T | T |
| 352270 | T | F | T | T |
| 352271 | T | F | T | T |
| 352272 | T | F | T | T |
| 352273 | T | F | F | T |
| 352274 | T | T | * | T |
| 352275 | T | T | * | T |
| 352276 | T | F | F | T |
| 352277 | T | T | * | T |
| 352278 | T | T | * | T |
| 352279 | T | T | * | T |
| 352280 | T | F | T | T |
| 352281 | T | F | F | T |
| 352282 | T | F | T | T |
| 352283 | T | F | F | T |
| 352284 | T | F | F | T |
| 352285 | T | T | * | T |
| 352286 | T | F | F | T |
| 352287 | T | F | F | T |
| 352288 | T | F | F | T |
| 352289 | T | F | T | T |
| 352290 | T | F | T | T |
| 352291 | T | F | F | T |
| 352292 | T | F | T | T |
| 352293 | T | F | F | T |
| 352294 | T | F | F | T |
| 352295 | T | F | F | T |
| 352296 | T | F | T | T |
| 352297 | T | F | T | T |
| 352298 | T | F | F | T |
| 352299 | T | T | * | T |
| 352300 | T | F | F | T |
| 352301 | T | F | F | T |
| 352302 | T | F | F | T |
| 352303 | T | T | * | T |
| 352304 | T | T | * | T |
| 352305 | T | F | F | T |
| 352306 | T | F | T | T |
| 352307 | T | F | T | T |
| 352308 | T | F | F | T |
| 352309 | T | T | * | T |
| 352310 | T | F | F | T |
| 352311 | T | F | F | T |
| 352312 | T | F | * | T |
| 352313 | T | F | T | T |
| 352314 | T | F | F | T |
| 352315 | T | F | * | T |
| 352316 | T | F | * | T |
| 352317 | T | T | * | T |
| 352318 | T | T | * | T |
| 352319 | T | F | * | T |
| 352320 | T | F | T | T |
| 352321 | T | T | * | T |
| 352322 | T | F | * | T |
| 352323 | T | F | T | T |
| 352324 | T | F | F | T |
| 352325 | T | F | T | T |
| 352326 | T | T | * | T |
| 352327 | T | T | * | T |
| 352328 | T | F | F | T |
| 352329 | T | F | T | T |
| 352330 | T | F | T | T |
| 352331 | T | T | * | T |
| 352332 | T | F | T | T |
| 352333 | T | T | * | T |
| 352334 | T | T | * | T |
| 352335 | T | F | F | T |
| 352336 | T | F | T | T |
| 352337 | T | F | T | T |
| 352338 | T | F | * | T |
| 352339 | T | F | T | T |
| 352340 | T | F | F | T |
| 352341 | T | F | F | T |
| 352342 | T | F | F | T |
| 352343 | T | F | F | T |
| 352344 | T | T | * | T |
| 352345 | T | F | F | T |
| 352346 | T | F | F | T |
| 352347 | T | F | T | T |
| 352348 | T | T | * | T |
| 352349 | T | F | F | T |
| 378480 | T | T | * | T |
| 378481 | T | F | F | T |
| 381215 | T | T | * | T |
| 381216 | T | F | F | T |
| 384076 | T | T | * | T |
| 384077 | T | F | F | T |
Independent-effect pairs
All 3 conditions live in dlmalloc — 3 br_if
c0(branch9510): GAP view gap →c1(branch9511): GAP view gap →c2(branch9512): GAP view gap →