Decision #1201 — malloc.c:4778
Status: no_witness
Truth table
| row | c0 br 8248 | c1 br 8249 | c2 br 8250 | c3 br 8251 | c4 br 8252 | c5 br 8253 | c6 br 8254 | c7 br 8255 | c8 br 8256 | c9 br 8257 | c10 br 8258 | c11 br 8259 | outcome |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 2991 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 6745 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 10633 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 12763 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 14121 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 15464 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 24168 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 24169 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 24170 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 24171 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 24172 | * | * | * | * | F | F | * | * | * | T | T | T | T |
| 24173 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 24174 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 24175 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 24176 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 24177 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 24178 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 24179 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 24180 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 24181 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 24182 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 24183 | * | * | * | * | F | T | * | T | T | * | * | T | T |
| 24184 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 24185 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 33630 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 33631 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 33632 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 33633 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 33634 | * | * | * | * | F | F | * | * | * | T | T | T | T |
| 33635 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 33636 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 33637 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 33638 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 33639 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 33640 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 33641 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 33642 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 33643 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 33644 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 33645 | * | * | * | * | F | T | * | T | T | * | * | T | T |
| 33646 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 33647 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 39766 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 39767 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 39768 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 39769 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 39770 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 45979 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 45980 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 45981 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 45982 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 45983 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 50310 | * | * | * | * | F | F | * | * | * | T | T | T | T |
| 50311 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 54599 | * | * | * | * | F | F | * | * | * | T | T | T | T |
| 54600 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 59086 | * | * | * | * | F | F | * | * | * | T | T | T | T |
| 59087 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 63234 | * | * | * | * | F | F | * | * | * | T | T | T | T |
| 63235 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 74456 | * | * | * | * | F | F | * | * | * | F | T | T | T |
| 74457 | * | * | * | * | F | F | * | * | * | T | T | T | T |
| 74458 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 74459 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 74460 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 74461 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 74462 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 74463 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 74464 | * | * | * | * | F | F | * | * | * | T | T | T | T |
| 74465 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 74466 | * | * | * | * | F | F | * | * | * | T | T | T | T |
| 74467 | * | * | * | * | F | F | * | * | * | T | T | T | T |
| 74468 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 74469 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 74470 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 74471 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 74472 | * | * | * | * | F | T | * | F | T | * | * | T | T |
| 74473 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 74474 | * | * | * | * | F | F | * | * | * | T | T | T | T |
| 74475 | * | * | * | * | F | F | * | * | * | T | T | T | T |
| 74476 | * | * | * | * | F | F | * | * | * | T | T | T | T |
| 74477 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 74478 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 74479 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 74480 | * | * | * | * | F | T | * | F | T | * | * | T | T |
| 74481 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 85969 | * | * | * | * | F | F | * | * | * | F | T | T | T |
| 85970 | * | * | * | * | F | F | * | * | * | T | T | T | T |
| 85971 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 85972 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 85973 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 85974 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 85975 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 85976 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 85977 | * | * | * | * | F | F | * | * | * | T | T | T | T |
| 85978 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 85979 | * | * | * | * | F | F | * | * | * | T | T | T | T |
| 85980 | * | * | * | * | F | F | * | * | * | T | T | T | T |
| 85981 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 85982 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 85983 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 85984 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 85985 | * | * | * | * | F | T | * | F | T | * | * | T | T |
| 85986 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 85987 | * | * | * | * | F | F | * | * | * | T | T | T | T |
| 85988 | * | * | * | * | F | F | * | * | * | T | T | T | T |
| 85989 | * | * | * | * | F | F | * | * | * | T | T | T | T |
| 85990 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 85991 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 85992 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 85993 | * | * | * | * | F | T | * | F | T | * | * | T | T |
| 85994 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 90620 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 90621 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 94888 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 94889 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 98886 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 100381 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 101819 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 104171 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 104172 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 104173 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 107990 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 107991 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 107992 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 107993 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 107994 | F | F | * | * | F | F | F | * | * | * | * | T | T |
| 107995 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 107996 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 110238 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 110239 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 113314 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 113315 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 113316 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 113317 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 113318 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 116418 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 116419 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 116420 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 116421 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138065 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138066 | * | * | * | * | F | F | * | * | * | T | T | T | T |
| 138067 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138068 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138069 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138070 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138071 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138072 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138073 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138074 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138075 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138076 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138077 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138078 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138079 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138080 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138081 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138082 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138083 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138084 | * | * | * | * | F | F | * | * | * | T | T | T | T |
| 138085 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138086 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138087 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138088 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138089 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138090 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138091 | * | * | * | * | F | T | * | F | T | * | * | T | T |
| 138092 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138093 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138094 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138095 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138096 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138097 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138098 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138099 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138100 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138101 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138102 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138103 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138104 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138105 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138106 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138107 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138108 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138109 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 138110 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161001 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161002 | * | * | * | * | F | F | * | * | * | T | T | T | T |
| 161003 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161004 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161005 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161006 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161007 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161008 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161009 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161010 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161011 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161012 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161013 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161014 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161015 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161016 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161017 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161018 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161019 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161020 | * | * | * | * | F | F | * | * | * | T | T | T | T |
| 161021 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161022 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161023 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161024 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161025 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161026 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161027 | * | * | * | * | F | T | * | F | T | * | * | T | T |
| 161028 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161029 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161030 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161031 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161032 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161033 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161034 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161035 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161036 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161037 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161038 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161039 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161040 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161041 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161042 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161043 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161044 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161045 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 161046 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 164217 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 165839 | * | * | * | * | F | F | F | * | * | * | * | T | T |
| 167539 | * | * | * | * | F | F | F | * | * | * | * | T | T |
Independent-effect pairs
All 12 conditions live in dlmalloc — 12 br_if
c0(branch8248): GAP view gap →c1(branch8249): GAP view gap →c2(branch8250): DEAD view gap →c3(branch8251): DEAD view gap →c4(branch8252): GAP view gap →c5(branch8253): GAP view gap →c6(branch8254): GAP view gap →c7(branch8255): GAP view gap →c8(branch8256): GAP view gap →c9(branch8257): GAP view gap →c10(branch8258): GAP view gap →c11(branch8259): GAP view gap →