Decision #1213 — malloc.c:4413
Status: no_witness
Truth table
| row | c0 br 8316 | c1 br 8317 | c2 br 8318 | c3 br 8319 | outcome |
|---|---|---|---|---|---|
| 3396 | * | * | F | F | T |
| 3397 | * | * | F | F | T |
| 3398 | * | * | F | F | T |
| 3399 | * | * | F | T | T |
| 3400 | * | * | F | T | T |
| 3401 | * | * | F | T | T |
| 3402 | * | * | F | T | T |
| 3403 | * | * | F | F | T |
| 3404 | * | * | F | F | T |
| 3405 | * | * | F | F | T |
| 3406 | * | * | F | F | T |
| 3407 | * | * | F | T | T |
| 3408 | * | * | F | T | T |
| 3409 | F | F | F | F | T |
| 3410 | * | * | F | F | T |
| 3411 | * | * | F | F | T |
| 3412 | * | * | F | F | T |
| 3413 | * | * | F | F | T |
| 3414 | * | * | F | F | T |
| 3415 | * | * | F | F | T |
| 7150 | * | * | F | F | T |
| 7151 | * | * | F | F | T |
| 7152 | * | * | F | F | T |
| 7153 | * | * | F | T | T |
| 7154 | * | * | F | T | T |
| 7155 | * | * | F | T | T |
| 7156 | * | * | F | T | T |
| 7157 | * | * | F | F | T |
| 7158 | * | * | F | F | T |
| 7159 | * | * | F | F | T |
| 7160 | * | * | F | F | T |
| 7161 | * | * | F | F | T |
| 7162 | * | * | F | T | T |
| 7163 | F | F | F | T | T |
| 7164 | * | * | F | F | T |
| 7165 | * | * | F | F | T |
| 7166 | * | * | F | F | T |
| 11091 | * | * | F | F | T |
| 11092 | * | * | F | F | T |
| 11093 | * | * | F | F | T |
| 11094 | * | * | F | T | T |
| 11095 | * | * | F | T | T |
| 11096 | * | * | F | T | T |
| 11097 | * | * | F | T | T |
| 11098 | * | * | F | F | T |
| 11099 | * | * | F | F | T |
| 11100 | * | * | F | F | T |
| 11101 | * | * | F | F | T |
| 11102 | * | * | F | T | T |
| 11103 | * | * | F | T | T |
| 11104 | * | * | F | F | T |
| 11105 | * | * | F | F | T |
| 11106 | * | * | F | F | T |
| 11107 | * | * | F | T | T |
| 11108 | * | * | F | T | T |
| 11109 | * | * | F | T | T |
| 11110 | * | * | F | F | T |
| 11111 | * | * | F | F | T |
| 11112 | * | * | F | F | T |
| 11113 | * | * | F | F | T |
| 11114 | * | * | F | F | T |
| 12895 | * | * | F | F | T |
| 12896 | * | * | F | F | T |
| 12897 | * | * | F | F | T |
| 12898 | * | * | F | F | T |
| 12899 | * | * | F | F | T |
| 12900 | * | * | F | F | T |
| 12901 | * | * | F | T | T |
| 12902 | * | * | F | F | T |
| 14247 | * | * | F | F | T |
| 14248 | * | * | F | F | T |
| 14249 | * | * | F | F | T |
| 14250 | * | * | F | F | T |
| 14251 | * | * | F | F | T |
| 14252 | * | * | F | F | T |
| 14253 | * | * | F | F | T |
| 15596 | * | * | F | F | T |
| 15597 | * | * | F | F | T |
| 15598 | * | * | F | F | T |
| 15599 | * | * | F | F | T |
| 15600 | * | * | F | F | T |
| 15601 | * | * | F | F | T |
| 15602 | * | * | F | T | T |
| 15603 | * | * | F | F | T |
| 24844 | * | * | F | F | T |
| 24845 | * | * | F | F | T |
| 24846 | * | * | T | * | T |
| 24847 | * | * | F | F | T |
| 24848 | F | F | T | * | T |
| 24849 | * | * | F | F | T |
| 24850 | * | * | F | T | T |
| 24851 | * | * | F | F | T |
| 24852 | * | * | F | F | T |
| 24853 | * | * | F | F | T |
| 24854 | * | * | F | F | T |
| 34305 | * | * | F | F | T |
| 34306 | * | * | F | F | T |
| 34307 | * | * | F | T | T |
| 34308 | * | * | F | F | T |
| 34309 | * | * | F | T | T |
| 34310 | * | * | F | F | T |
| 34311 | * | * | F | F | T |
| 34312 | * | * | F | T | T |
| 34313 | * | * | F | F | T |
| 34314 | * | * | F | F | T |
| 40473 | * | * | F | F | T |
| 40474 | * | * | F | F | T |
| 40475 | * | * | F | F | T |
| 40476 | * | * | F | F | T |
| 40477 | * | * | F | F | T |
| 40478 | * | * | F | F | T |
| 40479 | * | * | F | F | T |
| 40480 | * | * | F | F | T |
| 40481 | * | * | F | F | T |
| 40482 | * | * | F | F | T |
| 40483 | * | * | F | F | T |
| 40484 | * | * | F | F | T |
| 46686 | * | * | F | F | T |
| 46687 | * | * | F | F | T |
| 46688 | * | * | F | F | T |
| 46689 | * | * | F | F | T |
| 46690 | * | * | F | F | T |
| 46691 | * | * | F | F | T |
| 46692 | * | * | F | F | T |
| 46693 | * | * | F | F | T |
| 46694 | * | * | F | F | T |
| 46695 | * | * | F | F | T |
| 46696 | * | * | F | F | T |
| 46697 | * | * | F | F | T |
| 50792 | * | * | F | F | T |
| 50793 | * | * | F | F | T |
| 50794 | * | * | F | F | T |
| 50795 | * | * | F | F | T |
| 50796 | * | * | F | F | T |
| 50797 | * | * | F | F | T |
| 50798 | * | * | F | F | T |
| 50799 | * | * | F | F | T |
| 50800 | * | * | F | F | T |
| 50801 | * | * | F | F | T |
| 50802 | * | * | F | F | T |
| 50803 | * | * | F | T | T |
| 50804 | * | * | F | F | T |
| 50805 | F | F | F | F | T |
| 50806 | * | * | F | F | T |
| 50807 | * | * | F | F | T |
| 50808 | * | * | F | F | T |
| 50809 | * | * | F | F | T |
| 50810 | * | * | F | F | T |
| 50811 | * | * | F | F | T |
| 55119 | * | * | F | F | T |
| 55120 | * | * | F | F | T |
| 55121 | * | * | F | F | T |
| 55122 | * | * | F | F | T |
| 55123 | * | * | F | F | T |
| 55124 | * | * | F | F | T |
| 55125 | * | * | F | F | T |
| 55126 | * | * | F | F | T |
| 55127 | * | * | F | F | T |
| 55128 | * | * | F | F | T |
| 55129 | * | * | F | T | T |
| 55130 | F | F | F | T | T |
| 55131 | * | * | F | F | T |
| 55132 | * | * | F | T | T |
| 55133 | F | F | F | F | T |
| 55134 | * | * | F | F | T |
| 55135 | * | * | F | T | T |
| 55136 | F | F | F | F | T |
| 55137 | * | * | F | F | T |
| 55138 | * | * | F | T | T |
| 55139 | * | * | F | F | T |
| 55140 | * | * | F | T | T |
| 55141 | * | * | F | F | T |
| 59565 | * | * | F | F | T |
| 59566 | * | * | F | F | T |
| 59567 | * | * | F | F | T |
| 59568 | * | * | F | F | T |
| 59569 | * | * | F | F | T |
| 59570 | * | * | F | F | T |
| 59571 | * | * | F | F | T |
| 59572 | * | * | F | F | T |
| 59573 | * | * | F | F | T |
| 59574 | F | F | F | F | T |
| 59575 | * | * | F | F | T |
| 59576 | * | * | F | F | T |
| 59577 | * | * | F | F | T |
| 59578 | F | F | F | T | T |
| 59579 | * | * | F | F | T |
| 59580 | * | * | F | F | T |
| 59581 | * | * | F | T | T |
| 63716 | * | * | F | F | T |
| 63717 | * | * | F | F | T |
| 63718 | * | * | F | F | T |
| 63719 | * | * | F | F | T |
| 63720 | * | * | F | F | T |
| 63721 | * | * | F | F | T |
| 63722 | * | * | F | F | T |
| 63723 | * | * | F | F | T |
| 63724 | * | * | F | F | T |
| 63725 | * | * | F | F | T |
| 63726 | * | * | F | F | T |
| 63727 | * | * | F | T | T |
| 63728 | * | * | F | F | T |
| 63729 | F | F | F | F | T |
| 63730 | * | * | F | F | T |
| 63731 | * | * | F | F | T |
| 63732 | * | * | F | F | T |
| 63733 | * | * | F | F | T |
| 63734 | * | * | F | F | T |
| 63735 | * | * | F | F | T |
| 75237 | * | * | F | F | T |
| 75238 | * | * | F | F | T |
| 75239 | * | * | F | T | T |
| 75240 | * | * | F | F | T |
| 75241 | * | * | F | F | T |
| 75242 | * | * | F | F | T |
| 75243 | * | * | F | F | T |
| 75244 | * | * | F | F | T |
| 75245 | * | * | F | F | T |
| 75246 | * | * | F | F | T |
| 75247 | * | * | F | F | T |
| 75248 | * | * | F | F | T |
| 75249 | * | * | F | T | T |
| 75250 | F | F | F | T | T |
| 75251 | * | * | F | F | T |
| 75252 | * | * | F | T | T |
| 75253 | * | * | F | F | T |
| 86750 | * | * | F | F | T |
| 86751 | * | * | F | F | T |
| 86752 | * | * | F | T | T |
| 86753 | * | * | F | F | T |
| 86754 | * | * | F | F | T |
| 86755 | * | * | F | F | T |
| 86756 | * | * | F | F | T |
| 86757 | * | * | F | F | T |
| 86758 | * | * | F | F | T |
| 86759 | * | * | F | F | T |
| 86760 | * | * | F | F | T |
| 86761 | * | * | F | F | T |
| 86762 | * | * | F | T | T |
| 86763 | F | F | F | T | T |
| 86764 | * | * | F | F | T |
| 86765 | * | * | F | T | T |
| 86766 | * | * | F | F | T |
| 91011 | * | * | F | F | T |
| 91012 | * | * | F | T | T |
| 91013 | * | * | F | F | T |
| 91014 | * | * | F | F | T |
| 91015 | * | * | F | F | T |
| 91016 | * | * | F | F | T |
| 91017 | * | * | F | F | T |
| 91018 | * | * | F | F | T |
| 91019 | * | * | F | T | T |
| 91020 | * | * | F | F | T |
| 91021 | * | * | F | F | T |
| 91022 | * | * | F | T | T |
| 91023 | * | * | F | F | T |
| 91024 | * | * | F | F | T |
| 95279 | * | * | F | F | T |
| 95280 | * | * | F | T | T |
| 95281 | * | * | F | F | T |
| 95282 | * | * | F | F | T |
| 95283 | * | * | F | F | T |
| 95284 | * | * | F | F | T |
| 95285 | * | * | F | F | T |
| 95286 | * | * | F | F | T |
| 95287 | * | * | F | T | T |
| 95288 | * | * | F | F | T |
| 95289 | * | * | F | F | T |
| 95290 | * | * | F | T | T |
| 95291 | * | * | F | F | T |
| 95292 | * | * | F | F | T |
| 97434 | * | * | F | F | T |
| 97435 | * | * | F | F | T |
| 97436 | * | * | F | F | T |
| 97437 | * | * | F | F | T |
| 97438 | * | * | F | F | T |
| 97439 | * | * | F | F | T |
| 97440 | * | * | F | F | T |
| 97441 | * | * | F | F | T |
| 97442 | F | F | F | T | T |
| 97443 | * | * | F | F | T |
| 97444 | F | F | F | F | T |
| 97445 | * | * | F | F | T |
| 97446 | * | * | F | T | T |
| 97447 | * | * | F | F | T |
| 97448 | * | * | F | F | T |
| 97449 | * | * | F | F | T |
| 97450 | * | * | F | F | T |
| 99037 | * | * | F | F | T |
| 99038 | * | * | F | F | T |
| 99039 | * | * | F | F | T |
| 99040 | * | * | F | F | T |
| 99041 | * | * | F | F | T |
| 99042 | * | * | F | F | T |
| 99043 | * | * | T | * | T |
| 99044 | * | * | F | F | T |
| 100526 | * | * | F | F | T |
| 100527 | * | * | F | F | T |
| 100528 | * | * | F | F | T |
| 100529 | * | * | F | F | T |
| 100530 | * | * | F | F | T |
| 100531 | * | * | F | F | T |
| 100532 | * | * | F | F | T |
| 101970 | * | * | F | F | T |
| 101971 | * | * | F | F | T |
| 101972 | * | * | F | F | T |
| 101973 | * | * | F | F | T |
| 101974 | * | * | F | F | T |
| 101975 | * | * | F | F | T |
| 101976 | * | * | T | * | T |
| 101977 | * | * | F | F | T |
| 104446 | * | * | F | F | T |
| 104447 | * | * | F | F | T |
| 104448 | * | * | F | F | T |
| 104449 | * | * | F | F | T |
| 104450 | * | * | F | F | T |
| 104451 | * | * | F | F | T |
| 104452 | * | * | T | * | T |
| 104453 | * | * | F | F | T |
| 104454 | * | * | F | F | T |
| 104455 | * | * | F | F | T |
| 104456 | * | * | F | F | T |
| 104457 | * | * | F | F | T |
| 108313 | * | * | F | F | T |
| 108314 | F | F | F | F | T |
| 108315 | * | * | F | F | T |
| 108316 | * | * | F | F | T |
| 108317 | * | * | F | T | T |
| 108318 | * | * | F | T | T |
| 108319 | * | * | F | T | T |
| 108320 | * | * | F | T | T |
| 108321 | * | * | F | T | T |
| 108322 | * | * | F | T | T |
| 108323 | * | * | F | T | T |
| 108324 | * | * | F | T | T |
| 108325 | F | F | F | T | T |
| 108326 | * | * | F | F | T |
| 108327 | F | F | F | F | T |
| 108328 | * | * | F | F | T |
| 108329 | * | * | F | F | T |
| 108330 | * | * | F | F | T |
| 108331 | * | * | F | F | T |
| 108332 | * | * | F | F | T |
| 110457 | * | * | F | F | T |
| 110458 | * | * | F | F | T |
| 110459 | * | * | F | F | T |
| 110460 | * | * | F | F | T |
| 110461 | * | * | F | F | T |
| 110462 | * | * | F | F | T |
| 110463 | * | * | F | F | T |
| 110464 | * | * | F | F | T |
| 110465 | * | * | F | F | T |
| 110466 | * | * | F | F | T |
| 110467 | * | * | F | F | T |
| 113577 | * | * | F | F | T |
| 113578 | * | * | F | F | T |
| 113579 | * | * | F | F | T |
| 113580 | * | * | F | F | T |
| 113581 | * | * | F | F | T |
| 113582 | * | * | F | F | T |
| 113583 | * | * | F | F | T |
| 113584 | * | * | F | F | T |
| 113585 | * | * | F | F | T |
| 113586 | * | * | F | F | T |
| 113587 | * | * | F | F | T |
| 113588 | * | * | F | F | T |
| 113589 | F | F | T | * | T |
| 113590 | F | F | F | T | T |
| 113591 | * | * | F | F | T |
| 113592 | * | * | F | T | T |
| 113593 | * | * | F | T | T |
| 113594 | * | * | F | F | T |
| 113595 | * | * | F | F | T |
| 113596 | * | * | F | F | T |
| 116787 | * | * | F | F | T |
| 116788 | * | * | T | * | T |
| 116789 | * | * | F | F | T |
| 116790 | * | * | F | F | T |
| 116791 | * | * | F | F | T |
| 116792 | * | * | F | F | T |
| 116793 | F | F | F | F | T |
| 116794 | * | * | F | F | T |
| 116795 | * | * | F | F | T |
| 116796 | * | * | F | T | T |
| 116797 | * | * | F | F | T |
| 116798 | * | * | F | T | T |
| 116799 | * | * | F | F | T |
| 116800 | * | * | F | F | T |
| 116801 | * | * | F | F | T |
| 116802 | * | * | F | T | T |
| 116803 | * | * | F | F | T |
| 139385 | * | * | F | F | T |
| 139386 | * | * | F | F | T |
| 139387 | * | * | F | T | T |
| 139388 | * | * | F | F | T |
| 139389 | F | F | F | F | T |
| 139390 | F | F | F | F | T |
| 139391 | * | * | F | F | T |
| 139392 | * | * | F | F | T |
| 139393 | * | * | F | F | T |
| 139394 | * | * | F | F | T |
| 139395 | * | * | F | F | T |
| 139396 | F | F | F | F | T |
| 139397 | * | * | F | F | T |
| 139398 | * | * | F | F | T |
| 162321 | * | * | F | F | T |
| 162322 | * | * | F | F | T |
| 162323 | * | * | F | T | T |
| 162324 | * | * | F | F | T |
| 162325 | F | F | F | F | T |
| 162326 | F | F | F | F | T |
| 162327 | * | * | F | F | T |
| 162328 | * | * | F | F | T |
| 162329 | * | * | F | F | T |
| 162330 | * | * | F | F | T |
| 162331 | * | * | F | F | T |
| 162332 | F | F | F | F | T |
| 162333 | * | * | F | F | T |
| 162334 | * | * | F | F | T |
| 164403 | * | * | F | F | T |
| 164404 | * | * | F | F | T |
| 164405 | * | * | F | F | T |
| 164406 | * | * | F | F | T |
| 164407 | * | * | F | F | T |
| 166047 | * | * | F | F | T |
| 166048 | * | * | F | F | T |
| 166049 | * | * | F | F | T |
| 166050 | F | F | F | F | T |
| 166051 | * | * | F | F | T |
| 166052 | * | * | F | F | T |
| 166053 | * | * | F | F | T |
| 167738 | * | * | F | F | T |
| 167739 | * | * | F | F | T |
| 167740 | * | * | F | F | T |
| 167741 | * | * | F | F | T |
| 167742 | * | * | F | F | T |
| 167743 | * | * | F | F | T |
Independent-effect pairs
All 4 conditions live in dlfree — 4 br_if
c0(branch8316): GAP view gap →c1(branch8317): GAP view gap →c2(branch8318): GAP view gap →c3(branch8319): GAP view gap →