Decision #434 — library/core/src/cmp.rs:2011
Status: no_witness
Truth table
| row | c0 br 2549 | c1 br 2550 | c2 br 2860 | c3 br 2861 | outcome |
|---|---|---|---|---|---|
| 21614 | * | * | T | * | T |
| 21615 | * | * | T | * | T |
| 24357 | * | * | T | * | T |
| 24358 | * | * | T | * | T |
| 27000 | * | * | T | * | T |
| 27001 | * | * | T | * | T |
| 30482 | F | F | * | * | T |
| 30483 | F | F | * | * | T |
| 30484 | F | F | * | * | T |
| 30485 | F | F | * | * | T |
| 30486 | F | F | * | * | T |
| 30487 | F | F | * | * | T |
| 51337 | F | F | * | * | T |
| 51338 | F | F | * | * | T |
| 51339 | F | F | * | * | T |
| 51340 | F | F | * | * | T |
| 51341 | F | F | * | * | T |
| 51342 | F | F | * | * | T |
| 72148 | F | F | T | * | T |
| 72149 | F | F | T | * | T |
| 72150 | F | F | T | * | T |
| 72151 | F | F | T | * | T |
| 72152 | F | F | T | * | T |
| 72153 | F | F | T | * | T |
| 72154 | F | F | T | * | T |
| 72155 | F | F | T | * | T |
| 72156 | F | F | T | * | T |
| 72157 | F | F | T | * | T |
| 72158 | F | F | T | * | T |
| 72159 | F | F | T | * | T |
| 72160 | F | F | T | * | T |
| 72161 | F | F | T | * | T |
| 82031 | F | F | T | * | T |
| 82032 | F | F | T | * | T |
| 82033 | F | F | T | * | T |
| 82034 | F | F | T | * | T |
| 82035 | F | F | T | * | T |
| 82036 | F | F | T | * | T |
| 82037 | F | F | T | * | T |
| 82038 | F | F | T | * | T |
| 82039 | F | F | T | * | T |
| 82040 | F | F | T | * | T |
| 82041 | F | F | T | * | T |
| 82042 | F | F | T | * | T |
| 82043 | F | F | T | * | T |
| 82044 | F | F | T | * | T |
| 91806 | * | * | T | * | T |
| 91807 | * | * | T | * | T |
| 91808 | * | * | T | * | T |
| 91809 | * | * | T | * | T |
| 99583 | * | * | T | * | T |
| 99584 | * | * | T | * | T |
| 99585 | * | * | T | * | T |
| 99586 | * | * | T | * | T |
| 108072 | * | * | T | * | T |
| 108073 | * | * | T | * | T |
| 108074 | * | * | T | * | T |
| 108075 | * | * | T | * | T |
| 116150 | * | * | T | * | T |
| 116151 | * | * | T | * | T |
| 116152 | * | * | T | * | T |
| 116153 | * | * | T | * | T |
| 124140 | F | F | * | * | T |
| 124141 | F | F | * | * | T |
| 124142 | F | F | * | * | T |
| 124143 | F | F | * | * | T |
| 124144 | F | F | * | * | T |
| 124145 | F | F | * | * | T |
| 124146 | F | F | * | * | T |
| 124147 | F | F | * | * | T |
| 140859 | F | F | * | * | T |
| 140860 | F | F | * | * | T |
| 140861 | F | F | * | * | T |
| 140862 | F | F | * | * | T |
| 140863 | F | F | * | * | T |
| 140864 | F | F | * | * | T |
| 140865 | F | F | * | * | T |
| 140866 | F | F | * | * | T |
| 158007 | * | * | T | * | T |
| 158008 | * | * | T | * | T |
| 158009 | * | * | T | * | T |
| 158010 | * | * | T | * | T |
| 167865 | * | * | T | * | T |
| 167866 | * | * | T | * | T |
| 167867 | * | * | T | * | T |
| 167868 | * | * | T | * | T |
| 181107 | * | * | T | * | T |
| 181108 | * | * | T | * | T |
| 184427 | * | * | T | * | T |
| 184428 | * | * | T | * | T |
| 187534 | * | * | T | * | T |
| 187535 | * | * | T | * | T |
| 196206 | * | * | T | * | T |
| 196207 | * | * | T | * | T |
| 196208 | * | * | T | * | T |
| 196209 | * | * | T | * | T |
| 196210 | * | * | T | * | T |
| 196211 | * | * | T | * | T |
| 207545 | * | * | * | F | T |
| 207546 | * | * | * | F | T |
| 207547 | * | * | * | F | T |
| 207548 | * | * | * | F | T |
| 215496 | F | F | * | * | T |
| 215497 | F | F | * | * | T |
| 223766 | * | * | T | * | T |
| 223767 | * | * | T | * | T |
| 223768 | * | * | T | * | T |
| 223769 | * | * | T | * | T |
| 223770 | * | * | T | * | T |
| 223771 | * | * | T | * | T |
| 223772 | * | * | T | * | T |
| 223773 | * | * | T | * | T |
| 223774 | * | * | T | * | T |
| 223775 | * | * | T | * | T |
| 223776 | * | * | T | * | T |
| 223777 | * | * | T | * | T |
| 223778 | * | * | T | * | T |
| 223779 | * | * | T | * | T |
| 223780 | * | * | T | * | T |
| 223781 | * | * | T | * | T |
| 223782 | * | * | T | * | T |
| 223783 | * | * | T | * | T |
| 223784 | * | * | T | * | T |
| 223785 | * | * | T | * | T |
| 301143 | * | * | T | * | T |
| 301144 | * | * | T | * | T |
| 301145 | * | * | T | * | T |
| 301146 | * | * | T | * | T |
| 301147 | * | * | T | * | T |
| 301148 | * | * | T | * | T |
| 301149 | * | * | T | * | T |
| 301150 | * | * | T | * | T |
| 301151 | * | * | T | * | T |
| 301152 | * | * | T | * | T |
| 301153 | * | * | T | * | T |
| 301154 | * | * | T | * | T |
| 301155 | * | * | T | * | T |
| 301156 | * | * | T | * | T |
| 301157 | * | * | T | * | T |
| 301158 | * | * | T | * | T |
| 301159 | * | * | T | * | T |
| 301160 | * | * | T | * | T |
| 301161 | * | * | T | * | T |
| 301162 | * | * | T | * | T |
| 377009 | * | * | T | * | T |
| 377010 | * | * | T | * | T |
| 379646 | * | * | T | * | T |
| 379647 | * | * | T | * | T |
| 382530 | * | * | T | * | T |
| 382531 | * | * | T | * | T |
Independent-effect pairs
c0(branch2549): GAP view gap →<scry_analyze_core::Interp>::seq· br_if
inlined: lib.rs:5346 ← library/alloc/src/collections/btree/set.rs:611 ← library/alloc/src/collections/btree/map.rs:984 ← library/alloc/src/collections/btree/map.rs:723 ← library/alloc/src/collections/btree/search.rs:203 ← library/alloc/src/collections/btree/search.rs:226c1(branch2550): GAP view gap →<scry_analyze_core::Interp>::seq· br_if
inlined: lib.rs:5346 ← library/alloc/src/collections/btree/set.rs:611 ← library/alloc/src/collections/btree/map.rs:984 ← library/alloc/src/collections/btree/map.rs:723 ← library/alloc/src/collections/btree/search.rs:203 ← library/alloc/src/collections/btree/search.rs:226c2(branch2860): GAP view gap →<scry_analyze_core::Interp>::seq· br_if
inlined: lib.rs:6854 ← library/alloc/src/collections/btree/set.rs:1058 ← library/alloc/src/collections/btree/map.rs:1134 ← library/alloc/src/collections/btree/search.rs:58 ← library/alloc/src/collections/btree/search.rs:226c3(branch2861): GAP view gap →<scry_analyze_core::Interp>::seq· br_if
inlined: lib.rs:6854 ← library/alloc/src/collections/btree/set.rs:1058 ← library/alloc/src/collections/btree/map.rs:1134 ← library/alloc/src/collections/btree/search.rs:58 ← library/alloc/src/collections/btree/search.rs:226