Decision #792 — library/core/src/num/uint_macros.rs:1050
Status: no_witness
Truth table
| row | c0 br 5283 | c1 br 5284 | c2 br 5286 | c3 br 5289 | outcome |
|---|---|---|---|---|---|
| 1817 | * | * | * | T | T |
| 1818 | * | * | * | T | T |
| 1819 | * | * | * | T | T |
| 1820 | * | * | * | T | T |
| 1821 | * | * | * | T | T |
| 1822 | * | * | * | T | T |
| 1823 | * | * | * | T | T |
| 1824 | * | * | * | T | T |
| 1825 | * | * | * | T | T |
| 1826 | * | * | * | F | T |
| 1827 | * | * | * | F | T |
| 1828 | * | * | * | F | T |
| 5608 | * | * | * | T | T |
| 5609 | * | * | * | T | T |
| 5610 | * | * | * | T | T |
| 5611 | * | * | * | T | T |
| 5612 | * | * | * | T | T |
| 5613 | * | * | * | T | T |
| 5614 | * | * | * | T | T |
| 5615 | * | * | * | T | T |
| 5616 | * | * | * | T | T |
| 5617 | * | * | * | F | T |
| 5618 | * | * | * | F | T |
| 5619 | * | * | * | F | T |
| 9389 | * | * | * | T | T |
| 9390 | * | * | * | T | T |
| 9391 | * | * | * | T | T |
| 9392 | * | * | * | T | T |
| 9393 | * | * | * | T | T |
| 9394 | * | * | * | T | T |
| 9395 | * | * | * | T | T |
| 9396 | * | * | * | T | T |
| 9397 | * | * | * | T | T |
| 9398 | * | * | * | F | T |
| 9399 | * | * | * | F | T |
| 9400 | * | * | * | F | T |
| 12304 | * | * | * | T | T |
| 12305 | * | * | * | T | T |
| 12306 | * | * | * | T | T |
| 12307 | * | * | * | T | T |
| 12308 | * | * | * | T | T |
| 12309 | * | * | * | T | T |
| 13678 | * | * | * | T | T |
| 13679 | * | * | * | T | T |
| 13680 | * | * | * | T | T |
| 13681 | * | * | * | T | T |
| 13682 | * | * | * | T | T |
| 13683 | * | * | * | T | T |
| 15005 | * | * | * | T | T |
| 15006 | * | * | * | T | T |
| 15007 | * | * | * | T | T |
| 15008 | * | * | * | T | T |
| 15009 | * | * | * | T | T |
| 15010 | * | * | * | T | T |
| 22385 | F | F | * | F | T |
| 22386 | F | F | * | F | T |
| 22387 | F | F | * | F | T |
| 22388 | F | F | * | F | T |
| 22389 | F | F | * | F | T |
| 22390 | F | F | * | F | T |
| 22391 | F | F | * | F | T |
| 22392 | F | F | * | F | T |
| 22393 | F | F | * | F | T |
| 31863 | F | F | * | F | T |
| 31864 | F | F | * | F | T |
| 31865 | F | F | * | F | T |
| 31866 | F | F | * | F | T |
| 31867 | F | F | * | F | T |
| 31868 | F | F | * | F | T |
| 31869 | F | F | * | F | T |
| 31870 | F | F | * | F | T |
| 31871 | F | F | * | F | T |
| 38204 | * | * | * | F | T |
| 38205 | * | * | * | F | T |
| 38206 | * | * | * | F | T |
| 38207 | * | * | * | F | T |
| 38208 | * | * | * | F | T |
| 38209 | * | * | * | F | T |
| 38210 | * | * | * | F | T |
| 44417 | * | * | * | F | T |
| 44418 | * | * | * | F | T |
| 44419 | * | * | * | F | T |
| 44420 | * | * | * | F | T |
| 44421 | * | * | * | F | T |
| 44422 | * | * | * | F | T |
| 44423 | * | * | * | F | T |
| 49014 | * | * | * | F | T |
| 49015 | * | * | * | F | T |
| 49016 | * | * | * | F | T |
| 49017 | * | * | * | F | T |
| 49018 | * | * | * | T | T |
| 49019 | * | * | * | T | T |
| 49020 | * | * | * | T | T |
| 49021 | * | * | * | F | T |
| 49022 | * | * | * | F | T |
| 49023 | * | * | * | F | T |
| 49024 | * | * | * | F | T |
| 49025 | * | * | * | F | T |
| 49026 | * | * | * | F | T |
| 49027 | * | * | * | F | T |
| 53215 | * | * | * | F | T |
| 53216 | * | * | * | F | T |
| 53217 | * | * | * | F | T |
| 53218 | * | * | * | F | T |
| 53219 | * | * | * | T | T |
| 53220 | * | * | * | T | T |
| 53221 | * | * | * | T | T |
| 53222 | * | * | * | F | T |
| 53223 | * | * | * | F | T |
| 53224 | * | * | * | F | T |
| 53225 | * | * | * | F | T |
| 53226 | * | * | * | F | T |
| 53227 | * | * | * | F | T |
| 53228 | * | * | * | F | T |
| 57745 | * | * | * | F | T |
| 57746 | * | * | * | F | T |
| 57747 | * | * | * | F | T |
| 57748 | * | * | * | F | T |
| 57749 | * | * | * | T | T |
| 57750 | * | * | * | T | T |
| 57751 | * | * | * | T | T |
| 57752 | * | * | * | F | T |
| 57753 | * | * | * | F | T |
| 57754 | * | * | * | F | T |
| 57755 | * | * | * | F | T |
| 57756 | * | * | * | F | T |
| 57757 | * | * | * | F | T |
| 57758 | * | * | * | F | T |
| 61938 | * | * | * | F | T |
| 61939 | * | * | * | F | T |
| 61940 | * | * | * | F | T |
| 61941 | * | * | * | F | T |
| 61942 | * | * | * | T | T |
| 61943 | * | * | * | T | T |
| 61944 | * | * | * | T | T |
| 61945 | * | * | * | F | T |
| 61946 | * | * | * | F | T |
| 61947 | * | * | * | F | T |
| 61948 | * | * | * | F | T |
| 61949 | * | * | * | F | T |
| 61950 | * | * | * | F | T |
| 61951 | * | * | * | F | T |
| 72505 | F | F | * | F | T |
| 72506 | F | F | * | F | T |
| 72507 | F | F | * | F | T |
| 72508 | F | F | * | F | T |
| 72509 | F | F | * | F | T |
| 72510 | F | F | * | F | T |
| 72511 | F | F | * | F | T |
| 72512 | F | F | * | F | T |
| 72513 | F | F | * | F | T |
| 84018 | F | F | * | F | T |
| 84019 | F | F | * | F | T |
| 84020 | F | F | * | F | T |
| 84021 | F | F | * | F | T |
| 84022 | F | F | * | F | T |
| 84023 | F | F | * | F | T |
| 84024 | F | F | * | F | T |
| 84025 | F | F | * | F | T |
| 84026 | F | F | * | F | T |
| 89506 | * | * | * | T | T |
| 89507 | * | * | * | T | T |
| 89508 | * | * | * | T | T |
| 89509 | * | * | * | T | T |
| 89510 | * | * | * | T | T |
| 89511 | * | * | * | T | T |
| 89512 | * | * | * | T | T |
| 89513 | * | * | * | T | T |
| 89514 | * | * | * | T | T |
| 89515 | * | * | * | T | T |
| 89516 | * | * | * | T | T |
| 89517 | * | * | * | T | T |
| 89518 | * | * | * | T | T |
| 89519 | * | * | * | T | T |
| 89520 | * | * | * | T | T |
| 89521 | * | * | * | T | T |
| 89522 | * | * | * | T | T |
| 89523 | * | * | * | T | T |
| 89524 | * | * | * | T | T |
| 89525 | * | * | * | T | T |
| 89526 | * | * | * | T | T |
| 89527 | * | * | * | T | T |
| 89528 | * | * | * | T | T |
| 89529 | * | * | * | T | T |
| 93774 | * | * | * | T | T |
| 93775 | * | * | * | T | T |
| 93776 | * | * | * | T | T |
| 93777 | * | * | * | T | T |
| 93778 | * | * | * | T | T |
| 93779 | * | * | * | T | T |
| 93780 | * | * | * | T | T |
| 93781 | * | * | * | T | T |
| 93782 | * | * | * | T | T |
| 93783 | * | * | * | T | T |
| 93784 | * | * | * | T | T |
| 93785 | * | * | * | T | T |
| 93786 | * | * | * | T | T |
| 93787 | * | * | * | T | T |
| 93788 | * | * | * | T | T |
| 93789 | * | * | * | T | T |
| 93790 | * | * | * | T | T |
| 93791 | * | * | * | T | T |
| 93792 | * | * | * | T | T |
| 93793 | * | * | * | T | T |
| 93794 | * | * | * | T | T |
| 93795 | * | * | * | T | T |
| 93796 | * | * | * | T | T |
| 93797 | * | * | * | T | T |
| 96576 | * | * | * | T | T |
| 96577 | * | * | * | T | T |
| 98352 | * | * | * | T | T |
| 98353 | * | * | * | T | T |
| 98354 | * | * | * | T | T |
| 98355 | * | * | * | T | T |
| 98356 | * | * | * | T | T |
| 99867 | * | * | * | T | T |
| 99868 | * | * | * | T | T |
| 99869 | * | * | * | T | T |
| 99870 | * | * | * | T | T |
| 99871 | * | * | * | T | T |
| 101285 | * | * | * | T | T |
| 101286 | * | * | * | T | T |
| 101287 | * | * | * | T | T |
| 101288 | * | * | * | T | T |
| 101289 | * | * | * | T | T |
| 103317 | * | * | * | F | T |
| 103318 | * | * | * | F | T |
| 103319 | * | * | * | F | T |
| 103320 | * | * | * | F | T |
| 103321 | * | * | * | F | T |
| 103322 | * | * | * | F | T |
| 103323 | * | * | * | F | T |
| 103324 | * | * | * | F | T |
| 103325 | * | * | * | F | T |
| 103326 | * | * | * | F | T |
| 106949 | * | * | * | T | T |
| 106950 | * | * | * | T | T |
| 106951 | * | * | * | T | T |
| 106952 | * | * | * | T | T |
| 106953 | * | * | * | T | T |
| 106954 | * | * | * | T | T |
| 106955 | * | * | * | T | T |
| 106956 | * | * | * | T | T |
| 106957 | * | * | * | T | T |
| 106958 | * | * | * | T | T |
| 106959 | * | * | * | T | T |
| 106960 | * | * | * | T | T |
| 106961 | * | * | * | T | T |
| 106962 | * | * | * | T | T |
| 106963 | * | * | * | T | T |
| 106964 | * | * | * | T | T |
| 106965 | * | * | * | T | T |
| 106966 | * | * | * | T | T |
| 106967 | * | * | * | T | T |
| 106968 | * | * | * | T | T |
| 106969 | * | * | * | T | T |
| 106970 | * | * | * | T | T |
| 106971 | * | * | * | T | T |
| 106972 | * | * | * | T | T |
| 106973 | * | * | * | T | T |
| 106974 | * | * | * | T | T |
| 106975 | * | * | * | T | T |
| 106976 | * | * | * | T | T |
| 106977 | * | * | * | T | T |
| 106978 | * | * | * | T | T |
| 109502 | * | * | * | F | T |
| 109503 | * | * | * | F | T |
| 109504 | * | * | * | F | T |
| 109505 | * | * | * | F | T |
| 109506 | * | * | * | F | T |
| 109507 | * | * | * | F | T |
| 112426 | * | * | * | T | T |
| 112427 | * | * | * | T | T |
| 112428 | * | * | * | T | T |
| 112429 | * | * | * | T | T |
| 112430 | * | * | * | T | T |
| 112431 | * | * | * | T | T |
| 112432 | * | * | * | T | T |
| 112433 | * | * | * | T | T |
| 112434 | * | * | * | T | T |
| 112435 | * | * | * | T | T |
| 112436 | * | * | * | T | T |
| 112437 | * | * | * | T | T |
| 112438 | * | * | * | T | T |
| 112439 | * | * | * | T | T |
| 112440 | * | * | * | T | T |
| 112441 | * | * | * | T | T |
| 112442 | * | * | * | T | T |
| 112443 | * | * | * | T | T |
| 115372 | * | * | * | F | T |
| 115373 | * | * | * | F | T |
| 115374 | * | * | * | F | T |
| 115375 | * | * | * | F | T |
| 115376 | * | * | * | F | T |
| 115377 | * | * | * | F | T |
| 115378 | * | * | * | F | T |
| 115379 | * | * | * | F | T |
| 115380 | * | * | * | F | T |
| 135217 | F | F | * | F | T |
| 135218 | F | F | * | F | T |
| 135219 | F | F | T | F | T |
| 135220 | F | F | T | F | T |
| 135221 | F | F | T | F | T |
| 135222 | F | F | T | F | T |
| 135223 | F | F | T | F | T |
| 135224 | F | F | T | F | T |
| 135225 | F | F | T | F | T |
| 158153 | F | F | * | F | T |
| 158154 | F | F | * | F | T |
| 158155 | F | F | T | F | T |
| 158156 | F | F | T | F | T |
| 158157 | F | F | T | F | T |
| 158158 | F | F | T | F | T |
| 158159 | F | F | T | F | T |
| 158160 | F | F | T | F | T |
| 158161 | F | F | T | F | T |
| 163634 | * | * | * | F | T |
| 163635 | * | * | * | F | T |
| 163636 | * | * | * | F | T |
| 163637 | * | * | * | F | T |
| 165215 | * | * | * | F | T |
| 165216 | * | * | * | F | T |
| 165217 | * | * | * | F | T |
| 165218 | * | * | * | F | T |
| 166935 | * | * | * | F | T |
| 166936 | * | * | * | F | T |
| 166937 | * | * | * | F | T |
| 166938 | * | * | * | F | T |
Independent-effect pairs
c0(branch5283): GAP view gap →scry_octagon::relations· br_if
inlined: library/core/src/slice/index.rs:437c1(branch5284): GAP view gap →scry_octagon::relations· br_ifc2(branch5286): GAP view gap →scry_octagon::relations· br_ifc3(branch5289): GAP view gap →scry_octagon::relations· br_if
inlined: library/core/src/slice/index.rs:437