Decision #54 — library/alloc/src/raw_vec/mod.rs:424
Status: no_witness
Truth table
| row | c0 br 371 | c1 br 373 | outcome |
|---|---|---|---|
| 63 | F | T | T |
| 64 | * | F | T |
| 65 | * | T | T |
| 66 | * | F | T |
| 67 | * | T | T |
| 68 | * | F | T |
| 69 | * | T | T |
| 70 | * | T | T |
| 71 | * | F | T |
| 72 | * | T | T |
| 73 | * | T | T |
| 74 | * | F | T |
| 3857 | F | T | T |
| 3858 | * | F | T |
| 3859 | * | T | T |
| 3860 | * | F | T |
| 3861 | * | T | T |
| 3862 | * | F | T |
| 3863 | * | T | T |
| 3864 | * | T | T |
| 3865 | * | F | T |
| 3866 | * | T | T |
| 3867 | * | T | T |
| 3868 | * | F | T |
| 7540 | F | T | T |
| 7541 | * | F | T |
| 7542 | * | T | T |
| 7543 | * | F | T |
| 7544 | * | T | T |
| 7545 | * | F | T |
| 7546 | * | T | T |
| 7547 | * | T | T |
| 7548 | * | F | T |
| 7549 | * | T | T |
| 7550 | * | T | T |
| 7551 | * | F | T |
| 11677 | F | T | T |
| 11678 | * | T | T |
| 11679 | * | T | T |
| 11680 | * | T | T |
| 11681 | * | T | T |
| 11682 | * | F | T |
| 13053 | F | T | T |
| 13054 | * | T | T |
| 13055 | * | T | T |
| 13056 | * | T | T |
| 13057 | * | T | T |
| 13058 | * | F | T |
| 14378 | F | T | T |
| 14379 | * | T | T |
| 14380 | * | T | T |
| 14381 | * | T | T |
| 14382 | * | T | T |
| 14383 | * | F | T |
| 15844 | F | T | T |
| 15845 | * | T | T |
| 15846 | * | T | T |
| 15847 | * | T | T |
| 15848 | * | T | T |
| 15849 | * | T | T |
| 15850 | * | T | T |
| 15851 | * | T | T |
| 15852 | * | T | T |
| 15853 | * | T | T |
| 15854 | * | T | T |
| 15855 | * | T | T |
| 15856 | * | T | T |
| 15857 | * | T | T |
| 15858 | * | T | T |
| 15859 | * | F | T |
| 25324 | F | T | T |
| 25325 | * | T | T |
| 25326 | * | T | T |
| 25327 | * | T | T |
| 25328 | * | T | T |
| 25329 | * | T | T |
| 25330 | * | T | T |
| 25331 | * | T | T |
| 25332 | * | T | T |
| 25333 | * | T | T |
| 25334 | * | T | T |
| 25335 | * | T | T |
| 25336 | * | T | T |
| 25337 | * | T | T |
| 25338 | * | T | T |
| 25339 | * | F | T |
| 34788 | F | T | T |
| 34789 | * | T | T |
| 34790 | * | T | T |
| 34791 | * | T | T |
| 34792 | * | T | T |
| 34793 | * | T | T |
| 34794 | * | T | T |
| 34795 | * | T | T |
| 34796 | * | T | T |
| 34797 | * | T | T |
| 34798 | * | T | T |
| 34799 | * | T | T |
| 34800 | * | T | T |
| 34801 | * | T | T |
| 34802 | * | F | T |
| 41001 | F | T | T |
| 41002 | * | T | T |
| 41003 | * | T | T |
| 41004 | * | T | T |
| 41005 | * | T | T |
| 41006 | * | T | T |
| 41007 | * | T | T |
| 41008 | * | T | T |
| 41009 | * | T | T |
| 41010 | * | T | T |
| 41011 | * | T | T |
| 41012 | * | T | T |
| 41013 | * | T | T |
| 41014 | * | T | T |
| 41015 | * | F | T |
| 47132 | F | T | T |
| 47133 | * | T | T |
| 47134 | * | T | T |
| 47135 | * | F | T |
| 47136 | * | T | T |
| 47137 | * | T | T |
| 47138 | * | F | T |
| 47139 | * | T | T |
| 47140 | * | T | T |
| 47141 | * | T | T |
| 47142 | * | T | T |
| 47143 | * | T | T |
| 47144 | * | T | T |
| 47145 | * | F | T |
| 51260 | F | T | T |
| 51261 | * | T | T |
| 51262 | * | T | T |
| 51263 | * | F | T |
| 51264 | * | T | T |
| 51265 | * | T | T |
| 51266 | * | F | T |
| 51267 | * | T | T |
| 51268 | * | T | T |
| 51269 | * | T | T |
| 51270 | * | T | T |
| 51271 | * | T | T |
| 51272 | * | T | T |
| 51273 | * | F | T |
| 55798 | F | T | T |
| 55799 | * | T | T |
| 55800 | * | T | T |
| 55801 | * | F | T |
| 55802 | * | T | T |
| 55803 | * | T | T |
| 55804 | * | F | T |
| 55805 | * | T | T |
| 55806 | * | T | T |
| 55807 | * | T | T |
| 55808 | * | T | T |
| 55809 | * | T | T |
| 55810 | * | T | T |
| 55811 | * | F | T |
| 60056 | F | T | T |
| 60057 | * | T | T |
| 60058 | * | T | T |
| 60059 | * | F | T |
| 60060 | * | T | T |
| 60061 | * | T | T |
| 60062 | * | F | T |
| 60063 | * | T | T |
| 60064 | * | T | T |
| 60065 | * | T | T |
| 60066 | * | T | T |
| 60067 | * | T | T |
| 60068 | * | T | T |
| 60069 | * | F | T |
| 64259 | F | T | T |
| 64260 | * | T | T |
| 64261 | * | T | T |
| 64262 | * | T | T |
| 64263 | * | T | T |
| 64264 | * | T | T |
| 64265 | * | T | T |
| 64266 | * | T | T |
| 64267 | * | T | T |
| 64268 | * | T | T |
| 64269 | * | T | T |
| 64270 | * | T | T |
| 64271 | * | T | T |
| 64272 | * | T | T |
| 64273 | * | T | T |
| 64274 | * | F | T |
| 75772 | F | T | T |
| 75773 | * | T | T |
| 75774 | * | T | T |
| 75775 | * | T | T |
| 75776 | * | T | T |
| 75777 | * | T | T |
| 75778 | * | T | T |
| 75779 | * | T | T |
| 75780 | * | T | T |
| 75781 | * | T | T |
| 75782 | * | T | T |
| 75783 | * | T | T |
| 75784 | * | T | T |
| 75785 | * | T | T |
| 75786 | * | T | T |
| 75787 | * | F | T |
| 87235 | F | T | T |
| 87236 | * | T | T |
| 87237 | * | T | T |
| 87238 | * | F | T |
| 87239 | * | T | T |
| 87240 | * | T | T |
| 87241 | * | T | T |
| 87242 | * | F | T |
| 87243 | * | T | T |
| 87244 | * | T | T |
| 87245 | * | T | T |
| 87246 | * | F | T |
| 87247 | * | T | T |
| 87248 | * | T | T |
| 87249 | * | T | T |
| 87250 | * | F | T |
| 87251 | * | T | T |
| 87252 | * | T | T |
| 87253 | * | T | T |
| 87254 | * | F | T |
| 87255 | * | T | T |
| 87256 | * | T | T |
| 87257 | * | T | T |
| 87258 | * | F | T |
| 91503 | F | T | T |
| 91504 | * | T | T |
| 91505 | * | T | T |
| 91506 | * | F | T |
| 91507 | * | T | T |
| 91508 | * | T | T |
| 91509 | * | T | T |
| 91510 | * | F | T |
| 91511 | * | T | T |
| 91512 | * | T | T |
| 91513 | * | T | T |
| 91514 | * | F | T |
| 91515 | * | T | T |
| 91516 | * | T | T |
| 91517 | * | T | T |
| 91518 | * | F | T |
| 91519 | * | T | T |
| 91520 | * | T | T |
| 91521 | * | T | T |
| 91522 | * | F | T |
| 91523 | * | T | T |
| 91524 | * | T | T |
| 91525 | * | T | T |
| 91526 | * | F | T |
| 95728 | F | T | T |
| 95729 | * | F | T |
| 95730 | * | T | T |
| 95731 | * | F | T |
| 95732 | * | T | T |
| 95733 | * | F | T |
| 97764 | F | T | T |
| 97765 | * | T | T |
| 97766 | * | T | T |
| 97767 | * | T | T |
| 97768 | * | F | T |
| 99282 | F | T | T |
| 99283 | * | T | T |
| 99284 | * | T | T |
| 99285 | * | T | T |
| 99286 | * | F | T |
| 100697 | F | T | T |
| 100698 | * | T | T |
| 100699 | * | T | T |
| 100700 | * | T | T |
| 100701 | * | F | T |
| 102242 | F | T | T |
| 102243 | * | T | T |
| 102244 | * | T | T |
| 102245 | * | T | T |
| 102246 | * | T | T |
| 102247 | * | T | T |
| 102248 | * | T | T |
| 102249 | * | T | T |
| 102250 | * | T | T |
| 102251 | * | F | T |
| 104802 | F | T | T |
| 104803 | * | T | T |
| 104804 | * | T | T |
| 104805 | * | T | T |
| 104806 | * | T | T |
| 104807 | * | T | T |
| 104808 | * | T | T |
| 104809 | * | T | T |
| 104810 | * | T | T |
| 104811 | * | F | T |
| 104812 | * | T | T |
| 104813 | * | T | T |
| 104814 | * | T | T |
| 104815 | * | T | T |
| 104816 | * | T | T |
| 104817 | * | T | T |
| 104818 | * | T | T |
| 104819 | * | T | T |
| 104820 | * | T | T |
| 104821 | * | F | T |
| 104822 | * | T | T |
| 104823 | * | T | T |
| 104824 | * | T | T |
| 104825 | * | T | T |
| 104826 | * | T | T |
| 104827 | * | T | T |
| 104828 | * | T | T |
| 104829 | * | T | T |
| 104830 | * | T | T |
| 104831 | * | F | T |
| 108715 | F | T | T |
| 108716 | * | T | T |
| 108717 | * | T | T |
| 108718 | * | T | T |
| 108719 | * | T | T |
| 108720 | * | F | T |
| 110752 | F | T | T |
| 110753 | * | T | T |
| 110754 | * | T | T |
| 110755 | * | T | T |
| 110756 | * | T | T |
| 110757 | * | T | T |
| 110758 | * | T | T |
| 110759 | * | T | T |
| 110760 | * | T | T |
| 110761 | * | T | T |
| 110762 | * | T | T |
| 110763 | * | T | T |
| 110764 | * | T | T |
| 110765 | * | T | T |
| 110766 | * | T | T |
| 110767 | * | T | T |
| 110768 | * | F | T |
| 110769 | * | T | T |
| 110770 | * | T | T |
| 110771 | * | T | T |
| 110772 | * | T | T |
| 110773 | * | T | T |
| 110774 | * | T | T |
| 110775 | * | T | T |
| 110776 | * | T | T |
| 110777 | * | T | T |
| 110778 | * | T | T |
| 110779 | * | T | T |
| 110780 | * | T | T |
| 110781 | * | T | T |
| 110782 | * | T | T |
| 110783 | * | T | T |
| 110784 | * | T | T |
| 110785 | * | F | T |
| 114026 | F | T | T |
| 114027 | * | T | T |
| 114028 | * | T | T |
| 114029 | * | T | T |
| 114030 | * | T | T |
| 114031 | * | T | T |
| 114032 | * | T | T |
| 114033 | * | T | T |
| 114034 | * | T | T |
| 114035 | * | T | T |
| 114036 | * | T | T |
| 114037 | * | T | T |
| 114038 | * | T | T |
| 114039 | * | T | T |
| 114040 | * | T | T |
| 114041 | * | T | T |
| 114042 | * | T | T |
| 114043 | * | T | T |
| 114044 | * | T | T |
| 114045 | * | F | T |
| 117353 | F | T | T |
| 117354 | * | T | T |
| 117355 | * | T | T |
| 117356 | * | T | T |
| 117357 | * | T | T |
| 117358 | * | T | T |
| 117359 | * | T | T |
| 117360 | * | T | T |
| 117361 | * | T | T |
| 117362 | * | T | T |
| 117363 | * | T | T |
| 117364 | * | T | T |
| 117365 | * | T | T |
| 117366 | * | T | T |
| 117367 | * | T | T |
| 117368 | * | T | T |
| 117369 | * | F | T |
| 140289 | F | T | T |
| 140290 | * | T | T |
| 140291 | * | T | T |
| 140292 | * | T | T |
| 140293 | * | T | T |
| 140294 | * | T | T |
| 140295 | * | T | T |
| 140296 | * | T | T |
| 140297 | * | T | T |
| 140298 | * | T | T |
| 140299 | * | T | T |
| 140300 | * | T | T |
| 140301 | * | T | T |
| 140302 | * | T | T |
| 140303 | * | T | T |
| 140304 | * | T | T |
| 140305 | * | F | T |
| 163003 | F | T | T |
| 163004 | * | T | T |
| 163005 | * | T | T |
| 163006 | * | F | T |
| 164558 | F | T | T |
| 164559 | * | T | T |
| 164560 | * | T | T |
| 164561 | * | F | T |
| 166280 | F | T | T |
| 166281 | * | T | T |
| 166282 | * | T | T |
| 166283 | * | F | T |
Independent-effect pairs
c0(branch371): GAP view gap →<alloc::vec::Vec<scry_analyze_core::DefinedFunc> as core::ops::drop::Drop>::drop· br_ifc1(branch373): GAP view gap →<alloc::vec::Vec<scry_analyze_core::DefinedFunc> as core::ops::drop::Drop>::drop· br_if
inlined: library/core/src/slice/sort/stable/mod.rs:136 ← library/core/src/ptr/mod.rs:825 ← library/core/src/ptr/mod.rs:825