Decision #1189 — malloc.c:4231
Status: no_witness
Truth table
| row | c0 br 8150 | c1 br 8151 | outcome |
|---|---|---|---|
| 2756 | T | * | T |
| 2757 | T | * | T |
| 2758 | F | F | T |
| 2759 | F | F | T |
| 2760 | T | * | T |
| 2761 | T | * | T |
| 2762 | F | T | T |
| 2763 | T | * | T |
| 2764 | T | * | T |
| 2765 | T | * | T |
| 2766 | T | * | T |
| 2767 | T | * | T |
| 2768 | F | T | T |
| 2769 | F | T | T |
| 6532 | T | * | T |
| 6533 | T | * | T |
| 6534 | F | F | T |
| 6535 | F | F | T |
| 6536 | T | * | T |
| 6537 | T | * | T |
| 6538 | F | T | T |
| 6539 | T | * | T |
| 6540 | F | F | T |
| 6541 | T | * | T |
| 6542 | F | T | T |
| 6543 | T | * | T |
| 6544 | F | T | T |
| 6545 | F | F | T |
| 10382 | T | * | T |
| 10383 | T | * | T |
| 10384 | F | F | T |
| 10385 | F | F | T |
| 10386 | T | * | T |
| 10387 | T | * | T |
| 10388 | F | T | T |
| 10389 | T | * | T |
| 10390 | T | * | T |
| 10391 | T | * | T |
| 10392 | T | * | T |
| 10393 | T | * | T |
| 10394 | F | F | T |
| 10395 | F | T | T |
| 10396 | T | * | T |
| 10397 | F | F | T |
| 12671 | T | * | T |
| 12672 | T | * | T |
| 12673 | T | * | T |
| 12674 | T | * | T |
| 12675 | T | * | T |
| 12676 | T | * | T |
| 12677 | F | F | T |
| 14035 | T | * | T |
| 14036 | T | * | T |
| 14037 | T | * | T |
| 14038 | T | * | T |
| 14039 | T | * | T |
| 15372 | T | * | T |
| 15373 | T | * | T |
| 15374 | T | * | T |
| 15375 | T | * | T |
| 15376 | T | * | T |
| 15377 | T | * | T |
| 15378 | F | F | T |
| 23743 | T | * | T |
| 23744 | T | * | T |
| 23745 | T | * | T |
| 23746 | F | F | T |
| 23747 | T | * | T |
| 23748 | F | F | T |
| 23749 | T | * | T |
| 23750 | T | * | T |
| 23751 | F | F | T |
| 23752 | T | * | T |
| 23753 | F | T | T |
| 23754 | F | F | T |
| 23755 | T | * | T |
| 23756 | F | F | T |
| 23757 | T | * | T |
| 23758 | F | F | T |
| 23759 | F | F | T |
| 23760 | F | T | T |
| 33211 | T | * | T |
| 33212 | T | * | T |
| 33213 | T | * | T |
| 33214 | F | F | T |
| 33215 | T | * | T |
| 33216 | F | F | T |
| 33217 | T | * | T |
| 33218 | T | * | T |
| 33219 | F | F | T |
| 33220 | T | * | T |
| 33221 | F | T | T |
| 33222 | F | F | T |
| 33223 | T | * | T |
| 33224 | F | F | T |
| 33225 | T | * | T |
| 39424 | T | * | T |
| 39425 | T | * | T |
| 39426 | T | * | T |
| 39427 | T | * | T |
| 39428 | T | * | T |
| 39429 | T | * | T |
| 39430 | T | * | T |
| 39431 | T | * | T |
| 39432 | T | * | T |
| 39433 | T | * | T |
| 39434 | T | * | T |
| 39435 | T | * | T |
| 39436 | T | * | T |
| 39437 | T | * | T |
| 39438 | T | * | T |
| 39439 | T | * | T |
| 39440 | T | * | T |
| 39441 | T | * | T |
| 39442 | T | * | T |
| 39443 | T | * | T |
| 39444 | T | * | T |
| 39445 | T | * | T |
| 39446 | T | * | T |
| 39447 | T | * | T |
| 39448 | T | * | T |
| 39449 | T | * | T |
| 39450 | T | * | T |
| 39451 | T | * | T |
| 39452 | T | * | T |
| 39453 | T | * | T |
| 39454 | T | * | T |
| 39455 | T | * | T |
| 39456 | T | * | T |
| 39457 | T | * | T |
| 39458 | T | * | T |
| 39459 | T | * | T |
| 39460 | T | * | T |
| 39461 | T | * | T |
| 39462 | T | * | T |
| 39463 | T | * | T |
| 39464 | T | * | T |
| 39465 | T | * | T |
| 39466 | T | * | T |
| 39467 | F | F | T |
| 39468 | F | T | T |
| 39469 | F | T | T |
| 45637 | T | * | T |
| 45638 | T | * | T |
| 45639 | T | * | T |
| 45640 | T | * | T |
| 45641 | T | * | T |
| 45642 | T | * | T |
| 45643 | T | * | T |
| 45644 | T | * | T |
| 45645 | T | * | T |
| 45646 | T | * | T |
| 45647 | T | * | T |
| 45648 | T | * | T |
| 45649 | T | * | T |
| 45650 | T | * | T |
| 45651 | T | * | T |
| 45652 | T | * | T |
| 45653 | T | * | T |
| 45654 | T | * | T |
| 45655 | T | * | T |
| 45656 | T | * | T |
| 45657 | T | * | T |
| 45658 | T | * | T |
| 45659 | T | * | T |
| 45660 | T | * | T |
| 45661 | T | * | T |
| 45662 | T | * | T |
| 45663 | T | * | T |
| 45664 | T | * | T |
| 45665 | T | * | T |
| 45666 | T | * | T |
| 45667 | T | * | T |
| 45668 | T | * | T |
| 45669 | T | * | T |
| 45670 | T | * | T |
| 45671 | T | * | T |
| 45672 | T | * | T |
| 45673 | T | * | T |
| 45674 | T | * | T |
| 45675 | T | * | T |
| 45676 | T | * | T |
| 45677 | T | * | T |
| 45678 | T | * | T |
| 45679 | T | * | T |
| 45680 | F | F | T |
| 45681 | F | T | T |
| 45682 | F | T | T |
| 49991 | T | * | T |
| 49992 | T | * | T |
| 49993 | T | * | T |
| 49994 | T | * | T |
| 49995 | T | * | T |
| 49996 | T | * | T |
| 49997 | T | * | T |
| 49998 | F | F | T |
| 49999 | T | * | T |
| 50000 | F | F | T |
| 50001 | F | T | T |
| 50002 | T | * | T |
| 50003 | T | * | T |
| 50004 | F | F | T |
| 50005 | T | * | T |
| 50006 | T | * | T |
| 50007 | F | T | T |
| 54247 | T | * | T |
| 54248 | T | * | T |
| 54249 | T | * | T |
| 54250 | T | * | T |
| 54251 | T | * | T |
| 54252 | T | * | T |
| 54253 | T | * | T |
| 54254 | F | F | T |
| 54255 | T | * | T |
| 54256 | F | F | T |
| 54257 | F | T | T |
| 54258 | T | * | T |
| 54259 | T | * | T |
| 54260 | F | F | T |
| 54261 | T | * | T |
| 54262 | T | * | T |
| 54263 | F | T | T |
| 54264 | F | F | T |
| 54265 | F | F | T |
| 54266 | F | T | T |
| 54267 | F | F | T |
| 54268 | F | F | T |
| 58748 | T | * | T |
| 58749 | T | * | T |
| 58750 | T | * | T |
| 58751 | T | * | T |
| 58752 | T | * | T |
| 58753 | T | * | T |
| 58754 | T | * | T |
| 58755 | F | F | T |
| 58756 | T | * | T |
| 58757 | F | F | T |
| 58758 | F | T | T |
| 58759 | T | * | T |
| 58760 | T | * | T |
| 58761 | F | F | T |
| 58762 | T | * | T |
| 58763 | T | * | T |
| 58764 | F | T | T |
| 58765 | T | * | T |
| 58766 | F | F | T |
| 58767 | T | * | T |
| 58768 | T | * | T |
| 58769 | T | * | T |
| 58770 | T | * | T |
| 58771 | T | * | T |
| 62915 | T | * | T |
| 62916 | T | * | T |
| 62917 | T | * | T |
| 62918 | T | * | T |
| 62919 | T | * | T |
| 62920 | T | * | T |
| 62921 | T | * | T |
| 62922 | F | F | T |
| 62923 | T | * | T |
| 62924 | F | F | T |
| 62925 | F | T | T |
| 62926 | T | * | T |
| 62927 | T | * | T |
| 62928 | F | F | T |
| 62929 | T | * | T |
| 62930 | T | * | T |
| 62931 | F | T | T |
| 74003 | T | * | T |
| 74004 | T | * | T |
| 74005 | T | * | T |
| 74006 | T | * | T |
| 74007 | F | F | T |
| 74008 | F | F | T |
| 74009 | F | F | T |
| 74010 | T | * | T |
| 74011 | T | * | T |
| 74012 | T | * | T |
| 74013 | T | * | T |
| 74014 | T | * | T |
| 74015 | F | F | T |
| 74016 | T | * | T |
| 74017 | F | F | T |
| 74018 | T | * | T |
| 74019 | F | F | T |
| 74020 | T | * | T |
| 74021 | T | * | T |
| 74022 | F | F | T |
| 74023 | F | F | T |
| 74024 | F | F | T |
| 74025 | F | F | T |
| 74026 | F | F | T |
| 74027 | F | F | T |
| 74028 | F | T | T |
| 74029 | F | T | T |
| 74030 | T | * | T |
| 74031 | F | F | T |
| 85516 | T | * | T |
| 85517 | T | * | T |
| 85518 | T | * | T |
| 85519 | T | * | T |
| 85520 | F | F | T |
| 85521 | F | F | T |
| 85522 | F | F | T |
| 85523 | T | * | T |
| 85524 | T | * | T |
| 85525 | T | * | T |
| 85526 | T | * | T |
| 85527 | T | * | T |
| 85528 | F | F | T |
| 85529 | T | * | T |
| 85530 | F | F | T |
| 85531 | T | * | T |
| 85532 | F | F | T |
| 85533 | T | * | T |
| 85534 | T | * | T |
| 85535 | F | F | T |
| 85536 | F | F | T |
| 85537 | F | F | T |
| 85538 | F | F | T |
| 85539 | F | F | T |
| 85540 | F | F | T |
| 85541 | F | T | T |
| 85542 | F | T | T |
| 85543 | T | * | T |
| 85544 | F | F | T |
| 90384 | T | * | T |
| 90385 | T | * | T |
| 90386 | T | * | T |
| 90387 | F | F | T |
| 90388 | T | * | T |
| 90389 | T | * | T |
| 90390 | T | * | T |
| 90391 | T | * | T |
| 90392 | T | * | T |
| 90393 | T | * | T |
| 90394 | T | * | T |
| 90395 | T | * | T |
| 90396 | F | F | T |
| 90397 | F | T | T |
| 90398 | T | * | T |
| 90399 | F | T | T |
| 90400 | T | * | T |
| 90401 | T | * | T |
| 90402 | T | * | T |
| 90403 | T | * | T |
| 90404 | F | T | T |
| 90405 | F | F | T |
| 90406 | F | T | T |
| 90407 | F | T | T |
| 90408 | T | * | T |
| 90409 | T | * | T |
| 94652 | T | * | T |
| 94653 | T | * | T |
| 94654 | T | * | T |
| 94655 | F | F | T |
| 94656 | T | * | T |
| 94657 | T | * | T |
| 94658 | T | * | T |
| 94659 | T | * | T |
| 94660 | T | * | T |
| 94661 | T | * | T |
| 94662 | T | * | T |
| 94663 | T | * | T |
| 94664 | F | F | T |
| 94665 | F | T | T |
| 94666 | T | * | T |
| 94667 | F | T | T |
| 94668 | T | * | T |
| 94669 | T | * | T |
| 94670 | T | * | T |
| 94671 | T | * | T |
| 94672 | F | T | T |
| 94673 | F | F | T |
| 94674 | F | T | T |
| 94675 | F | T | T |
| 94676 | T | * | T |
| 94677 | T | * | T |
| 97094 | T | * | T |
| 97095 | T | * | T |
| 97096 | T | * | T |
| 97097 | T | * | T |
| 97098 | T | * | T |
| 97099 | T | * | T |
| 97100 | F | F | T |
| 97101 | T | * | T |
| 98781 | T | * | T |
| 98782 | T | * | T |
| 98783 | T | * | T |
| 98784 | T | * | T |
| 98785 | F | F | T |
| 98786 | T | * | T |
| 100284 | T | * | T |
| 100285 | T | * | T |
| 100286 | T | * | T |
| 100287 | T | * | T |
| 100288 | F | F | T |
| 100289 | F | F | T |
| 101714 | T | * | T |
| 101715 | T | * | T |
| 101716 | T | * | T |
| 101717 | T | * | T |
| 101718 | F | F | T |
| 101719 | T | * | T |
| 103974 | T | * | T |
| 103975 | T | * | T |
| 103976 | T | * | T |
| 107770 | T | * | T |
| 107771 | T | * | T |
| 107772 | T | * | T |
| 107773 | T | * | T |
| 107774 | T | * | T |
| 107775 | F | F | T |
| 107776 | F | T | T |
| 107777 | F | T | T |
| 107778 | T | * | T |
| 107779 | F | T | T |
| 107780 | F | T | T |
| 110077 | T | * | T |
| 110078 | T | * | T |
| 110079 | T | * | T |
| 110080 | T | * | T |
| 110081 | F | F | T |
| 110082 | T | * | T |
| 113152 | T | * | T |
| 113153 | T | * | T |
| 113154 | T | * | T |
| 113155 | T | * | T |
| 113156 | T | * | T |
| 113157 | T | * | T |
| 113158 | F | F | T |
| 113159 | T | * | T |
| 113160 | T | * | T |
| 116175 | T | * | T |
| 116176 | T | * | T |
| 116177 | T | * | T |
| 116178 | T | * | T |
| 116179 | T | * | T |
| 116180 | T | * | T |
| 116181 | F | F | T |
| 116182 | T | * | T |
| 116183 | F | T | T |
| 137415 | T | * | T |
| 137416 | T | * | T |
| 137417 | T | * | T |
| 137418 | F | T | T |
| 137419 | F | F | T |
| 137420 | F | T | T |
| 137421 | F | * | T |
| 137422 | T | * | T |
| 137423 | T | * | T |
| 137424 | F | F | T |
| 137425 | F | T | T |
| 137426 | T | * | T |
| 137427 | F | F | T |
| 137428 | T | * | T |
| 137429 | T | * | T |
| 137430 | F | F | T |
| 137431 | F | F | T |
| 137432 | F | T | T |
| 137433 | F | F | T |
| 137434 | F | F | T |
| 137435 | F | F | T |
| 137436 | F | T | T |
| 137437 | F | T | T |
| 137438 | F | F | T |
| 137439 | F | F | T |
| 137440 | F | F | T |
| 137441 | T | * | T |
| 137442 | F | F | T |
| 137443 | F | * | T |
| 137444 | F | T | T |
| 137445 | F | F | T |
| 137446 | F | T | T |
| 137447 | F | F | T |
| 137448 | F | F | T |
| 137449 | F | T | T |
| 137450 | F | F | T |
| 137451 | T | * | T |
| 137452 | T | * | T |
| 137453 | T | * | T |
| 137454 | F | F | T |
| 137455 | F | F | T |
| 137456 | F | F | T |
| 137457 | T | * | T |
| 137458 | F | F | T |
| 137459 | T | * | T |
| 137460 | F | F | T |
| 137461 | F | F | T |
| 137462 | T | * | T |
| 137463 | F | F | T |
| 137464 | F | F | T |
| 137465 | F | F | T |
| 137466 | F | F | T |
| 137467 | F | T | T |
| 137468 | F | F | T |
| 137469 | F | T | T |
| 137470 | F | F | T |
| 137471 | F | F | T |
| 137472 | F | T | T |
| 137473 | F | F | T |
| 137474 | F | F | T |
| 137475 | F | F | T |
| 137476 | F | T | T |
| 137477 | T | * | T |
| 137478 | F | F | T |
| 137479 | F | F | T |
| 137480 | F | T | T |
| 137481 | F | T | T |
| 137482 | F | T | T |
| 137483 | T | * | T |
| 137484 | T | * | T |
| 137485 | F | T | T |
| 137486 | F | T | T |
| 137487 | F | F | T |
| 137488 | F | T | T |
| 137489 | F | F | T |
| 137490 | T | * | T |
| 137491 | F | T | T |
| 137492 | F | * | T |
| 137493 | F | T | T |
| 137494 | F | F | T |
| 137495 | F | F | T |
| 137496 | F | * | T |
| 137497 | F | T | T |
| 137498 | F | * | T |
| 137499 | F | T | T |
| 137500 | F | T | T |
| 160351 | T | * | T |
| 160352 | T | * | T |
| 160353 | T | * | T |
| 160354 | F | T | T |
| 160355 | F | F | T |
| 160356 | F | T | T |
| 160357 | F | * | T |
| 160358 | T | * | T |
| 160359 | T | * | T |
| 160360 | F | F | T |
| 160361 | F | T | T |
| 160362 | T | * | T |
| 160363 | F | F | T |
| 160364 | T | * | T |
| 160365 | T | * | T |
| 160366 | F | F | T |
| 160367 | F | F | T |
| 160368 | F | T | T |
| 160369 | F | F | T |
| 160370 | F | F | T |
| 160371 | F | F | T |
| 160372 | F | T | T |
| 160373 | F | T | T |
| 160374 | F | F | T |
| 160375 | F | F | T |
| 160376 | F | F | T |
| 160377 | T | * | T |
| 160378 | F | F | T |
| 160379 | F | * | T |
| 160380 | F | T | T |
| 160381 | F | F | T |
| 160382 | F | T | T |
| 160383 | F | F | T |
| 160384 | F | F | T |
| 160385 | F | T | T |
| 160386 | F | F | T |
| 160387 | T | * | T |
| 160388 | T | * | T |
| 160389 | T | * | T |
| 160390 | F | F | T |
| 160391 | F | F | T |
| 160392 | F | F | T |
| 160393 | T | * | T |
| 160394 | F | F | T |
| 160395 | T | * | T |
| 160396 | F | F | T |
| 160397 | F | F | T |
| 160398 | T | * | T |
| 160399 | F | F | T |
| 160400 | F | F | T |
| 160401 | F | F | T |
| 160402 | F | F | T |
| 160403 | F | T | T |
| 160404 | F | F | T |
| 160405 | F | T | T |
| 160406 | F | F | T |
| 160407 | F | F | T |
| 160408 | F | T | T |
| 160409 | F | F | T |
| 160410 | F | F | T |
| 160411 | F | F | T |
| 160412 | F | T | T |
| 160413 | T | * | T |
| 160414 | F | F | T |
| 160415 | F | F | T |
| 160416 | F | T | T |
| 160417 | F | T | T |
| 160418 | F | T | T |
| 160419 | T | * | T |
| 160420 | T | * | T |
| 160421 | F | T | T |
| 160422 | F | T | T |
| 160423 | F | F | T |
| 160424 | F | T | T |
| 160425 | F | F | T |
| 160426 | T | * | T |
| 160427 | F | T | T |
| 160428 | F | * | T |
| 160429 | F | T | T |
| 160430 | F | F | T |
| 160431 | F | F | T |
| 160432 | F | * | T |
| 160433 | F | T | T |
| 160434 | F | * | T |
| 160435 | F | T | T |
| 160436 | F | T | T |
| 164076 | T | * | T |
| 164077 | T | * | T |
| 164078 | T | * | T |
| 165682 | T | * | T |
| 165683 | T | * | T |
| 165684 | T | * | T |
| 165685 | F | F | T |
| 165686 | T | * | T |
| 165687 | F | F | T |
| 165688 | T | * | T |
| 167390 | T | * | T |
| 167391 | T | * | T |
| 167392 | T | * | T |
| 167393 | F | F | T |
| 167394 | T | * | T |
| 167395 | F | F | T |
| 167396 | T | * | T |
Independent-effect pairs
c0(branch8150): GAP view gap →dlmalloc· br_ifc1(branch8151): GAP view gap →dlmalloc· br_if