Decision #138 — library/core/src/ptr/mod.rs:1921
Status: no_witness
Truth table
| row | c0 br 968 | c1 br 971 | c2 br 1009 | c3 br 1012 | c4 br 1014 | c5 br 1044 | c6 br 1045 | c7 br 1046 | outcome |
|---|---|---|---|---|---|---|---|---|---|
| 421 | T | F | * | * | * | * | * | * | T |
| 422 | T | F | * | * | * | * | * | * | T |
| 423 | * | F | * | * | * | * | * | * | T |
| 424 | * | F | * | * | * | F | F | * | T |
| 425 | * | * | * | * | * | F | F | * | T |
| 426 | * | * | * | * | * | F | F | * | T |
| 427 | * | * | * | * | * | F | F | * | T |
| 428 | * | * | * | * | * | F | F | * | T |
| 429 | * | * | * | * | * | F | F | * | T |
| 430 | T | F | * | * | * | F | F | * | T |
| 431 | * | * | * | * | * | F | F | * | T |
| 432 | * | * | * | * | * | F | F | * | T |
| 433 | T | F | * | * | * | F | T | T | T |
| 434 | * | F | * | * | * | * | * | * | T |
| 435 | * | F | * | * | * | F | T | T | T |
| 436 | * | * | * | * | * | F | T | T | T |
| 3461 | T | F | * | * | * | * | * | * | T |
| 3462 | T | F | * | * | * | * | * | * | T |
| 3463 | * | F | * | * | * | * | * | * | T |
| 3464 | * | F | * | * | * | F | F | * | T |
| 3465 | * | * | * | * | * | F | F | * | T |
| 3466 | * | * | * | * | * | F | F | * | T |
| 3467 | * | * | * | * | * | F | F | * | T |
| 3468 | * | * | * | * | * | F | F | * | T |
| 3469 | * | * | * | * | * | F | F | * | T |
| 3470 | T | F | * | * | * | F | F | * | T |
| 3471 | * | * | * | * | * | F | F | * | T |
| 3472 | * | * | * | * | * | F | F | * | T |
| 3473 | T | F | * | * | * | F | T | T | T |
| 3474 | * | F | * | * | * | * | * | * | T |
| 3475 | * | F | * | * | * | F | T | T | T |
| 3476 | * | * | * | * | * | F | T | T | T |
| 6356 | T | F | * | * | * | * | * | * | T |
| 6357 | T | F | * | * | * | * | * | * | T |
| 6358 | * | F | * | * | * | * | * | * | T |
| 6359 | * | F | * | * | * | F | F | * | T |
| 6360 | * | * | * | * | * | F | F | * | T |
| 6361 | * | * | * | * | * | F | F | * | T |
| 6362 | * | * | * | * | * | F | F | * | T |
| 6363 | * | * | * | * | * | F | F | * | T |
| 6364 | * | * | * | * | * | F | F | * | T |
| 6365 | T | F | * | * | * | F | F | * | T |
| 6366 | * | * | * | * | * | F | F | * | T |
| 6367 | * | * | * | * | * | F | F | * | T |
| 6368 | T | F | * | * | * | F | T | T | T |
| 6369 | * | F | * | * | * | * | * | * | T |
| 6370 | * | F | * | * | * | F | T | T | T |
| 6371 | * | * | * | * | * | F | T | T | T |
| 9563 | * | * | * | * | * | F | F | * | T |
| 9564 | * | * | * | * | * | F | F | * | T |
| 9565 | * | * | * | * | * | F | F | * | T |
| 9566 | * | * | * | * | * | F | F | * | T |
| 9567 | * | * | * | * | * | F | F | * | T |
| 9568 | * | * | * | * | * | F | F | * | T |
| 10711 | * | * | * | * | * | F | F | * | T |
| 10712 | * | * | * | * | * | F | F | * | T |
| 10713 | * | * | * | * | * | F | F | * | T |
| 10714 | * | * | * | * | * | F | F | * | T |
| 10715 | * | * | * | * | * | F | F | * | T |
| 10716 | * | * | * | * | * | F | F | * | T |
| 11802 | * | * | * | * | * | F | F | * | T |
| 11803 | * | * | * | * | * | F | F | * | T |
| 11804 | * | * | * | * | * | F | F | * | T |
| 11805 | * | * | * | * | * | F | F | * | T |
| 11806 | * | * | * | * | * | F | F | * | T |
| 11807 | * | * | * | * | * | F | F | * | T |
| 13394 | * | * | * | * | * | F | T | F | T |
| 13395 | * | * | * | * | * | F | T | F | T |
| 13396 | * | * | * | * | * | F | T | F | T |
| 13397 | * | * | * | * | * | F | T | F | T |
| 13398 | * | * | * | * | * | F | T | F | T |
| 13399 | * | * | * | * | * | F | T | F | T |
| 13400 | * | * | * | * | * | F | T | F | T |
| 13401 | * | * | * | * | * | F | T | F | T |
| 21112 | * | * | * | * | * | F | T | F | T |
| 21113 | * | * | * | * | * | F | T | F | T |
| 21114 | * | * | * | * | * | F | T | F | T |
| 21115 | * | * | * | * | * | F | T | F | T |
| 21116 | * | * | * | * | * | F | T | F | T |
| 21117 | * | * | * | * | * | F | T | F | T |
| 21118 | * | * | * | * | * | F | T | F | T |
| 21119 | * | * | * | * | * | F | T | F | T |
| 28907 | * | * | * | * | * | F | T | T | T |
| 28908 | * | * | * | * | * | F | T | T | T |
| 28909 | * | * | * | * | * | F | T | T | T |
| 28910 | * | * | * | * | * | F | T | T | T |
| 28911 | * | * | * | * | * | F | T | T | T |
| 28912 | * | * | * | * | * | F | T | T | T |
| 34845 | * | * | * | * | * | F | T | T | T |
| 34846 | * | * | * | * | * | F | T | T | T |
| 34847 | * | * | * | * | * | F | T | T | T |
| 34848 | * | * | * | * | * | F | T | T | T |
| 34849 | * | * | * | * | * | F | T | T | T |
| 34850 | * | * | * | * | * | F | T | T | T |
| 40560 | * | * | T | * | * | * | * | * | T |
| 40561 | * | * | T | * | * | F | T | T | T |
| 40562 | * | * | * | * | * | F | T | T | T |
| 40563 | * | * | * | * | * | F | T | T | T |
| 40564 | * | * | * | * | * | F | T | T | T |
| 40565 | * | * | T | T | * | F | F | * | T |
| 40566 | * | * | * | * | * | F | F | * | T |
| 40567 | * | * | * | * | * | F | F | * | T |
| 40568 | * | * | * | * | * | F | T | T | T |
| 40569 | * | * | * | * | * | F | T | T | T |
| 40570 | * | * | T | T | * | F | T | T | T |
| 40571 | * | * | * | * | * | F | T | T | T |
| 40572 | * | * | * | * | * | F | T | T | T |
| 40573 | * | * | * | * | * | F | T | T | T |
| 40574 | * | * | * | * | * | F | T | T | T |
| 43528 | * | * | T | * | * | * | * | * | T |
| 43529 | * | * | T | * | * | F | T | T | T |
| 43530 | * | * | * | * | * | F | T | T | T |
| 43531 | * | * | * | * | * | F | T | T | T |
| 43532 | * | * | * | * | * | F | T | T | T |
| 43533 | * | * | T | T | * | F | F | * | T |
| 43534 | * | * | * | * | * | F | F | * | T |
| 43535 | * | * | * | * | * | F | F | * | T |
| 43536 | * | * | * | * | * | F | T | T | T |
| 43537 | * | * | * | * | * | F | T | T | T |
| 43538 | * | * | T | T | * | F | T | T | T |
| 43539 | * | * | * | * | * | F | T | T | T |
| 43540 | * | * | * | * | * | F | T | T | T |
| 43541 | * | * | * | * | * | F | T | T | T |
| 43542 | * | * | * | * | * | F | T | T | T |
| 46981 | * | * | T | * | * | * | * | * | T |
| 46982 | * | * | T | * | * | F | T | T | T |
| 46983 | * | * | * | * | * | F | T | T | T |
| 46984 | * | * | * | * | * | F | T | T | T |
| 46985 | * | * | * | * | * | F | T | T | T |
| 46986 | * | * | T | * | * | F | F | * | T |
| 46987 | * | * | * | * | * | F | F | * | T |
| 46988 | * | * | * | * | * | F | F | * | T |
| 46989 | * | * | * | * | * | F | T | T | T |
| 46990 | * | * | * | * | * | F | T | T | T |
| 46991 | * | * | T | * | * | F | T | T | T |
| 46992 | * | * | * | * | * | F | T | T | T |
| 46993 | * | * | * | * | * | F | T | T | T |
| 46994 | * | * | * | * | * | F | T | T | T |
| 46995 | * | * | * | * | * | F | T | T | T |
| 50100 | * | * | T | * | * | * | * | * | T |
| 50101 | * | * | T | * | * | F | T | T | T |
| 50102 | * | * | * | * | * | F | T | T | T |
| 50103 | * | * | * | * | * | F | T | T | T |
| 50104 | * | * | * | * | * | F | T | T | T |
| 50105 | * | * | T | T | * | F | F | * | T |
| 50106 | * | * | * | * | * | F | F | * | T |
| 50107 | * | * | * | * | * | F | F | * | T |
| 50108 | * | * | * | * | * | F | T | T | T |
| 50109 | * | * | * | * | * | F | T | T | T |
| 50110 | * | * | T | T | * | F | T | T | T |
| 50111 | * | * | * | * | * | F | T | T | T |
| 50112 | * | * | * | * | * | F | T | T | T |
| 50113 | * | * | * | * | * | F | T | T | T |
| 50114 | * | * | * | * | * | F | T | T | T |
| 53302 | * | * | * | * | * | F | T | F | T |
| 53303 | * | * | * | * | * | F | T | F | T |
| 53304 | * | * | * | * | * | F | T | F | T |
| 53305 | * | * | * | * | * | F | T | F | T |
| 53306 | * | * | * | * | * | F | T | F | T |
| 53307 | * | * | * | * | * | F | T | F | T |
| 53308 | * | * | * | * | * | F | T | F | T |
| 53309 | * | * | * | * | * | F | T | F | T |
| 63074 | * | * | * | * | * | F | T | F | T |
| 63075 | * | * | * | * | * | F | T | F | T |
| 63076 | * | * | * | * | * | F | T | F | T |
| 63077 | * | * | * | * | * | F | T | F | T |
| 63078 | * | * | * | * | * | F | T | F | T |
| 63079 | * | * | * | * | * | F | T | F | T |
| 63080 | * | * | * | * | * | F | T | F | T |
| 63081 | * | * | * | * | * | F | T | F | T |
| 72711 | * | * | * | * | * | F | F | * | T |
| 72712 | * | * | * | * | * | F | F | * | T |
| 72713 | * | * | * | * | * | F | F | * | T |
| 72714 | * | * | * | * | * | F | F | * | T |
| 72715 | * | * | * | * | * | F | F | * | T |
| 72716 | * | * | * | * | * | F | F | * | T |
| 72717 | * | * | * | * | * | F | F | * | T |
| 72718 | * | * | * | * | * | F | F | * | T |
| 72719 | * | * | * | * | * | F | F | * | T |
| 72720 | * | * | * | * | * | F | F | * | T |
| 72721 | * | * | * | * | * | F | F | * | T |
| 72722 | * | * | * | * | * | F | F | * | T |
| 72723 | * | * | * | * | * | F | F | * | T |
| 72724 | * | * | * | * | * | F | F | * | T |
| 72725 | * | * | * | * | * | F | F | * | T |
| 72726 | * | * | * | * | * | F | F | * | T |
| 72727 | * | * | * | * | * | F | F | * | T |
| 72728 | * | * | * | * | * | F | F | * | T |
| 72729 | * | * | * | * | * | F | F | * | T |
| 72730 | * | * | * | * | * | F | F | * | T |
| 72731 | * | * | * | * | * | F | F | * | T |
| 72732 | * | * | * | * | * | F | F | * | T |
| 72733 | * | * | * | * | * | F | F | * | T |
| 72734 | * | * | * | * | * | F | F | * | T |
| 76186 | * | * | * | * | * | F | F | * | T |
| 76187 | * | * | * | * | * | F | F | * | T |
| 76188 | * | * | * | * | * | F | F | * | T |
| 76189 | * | * | * | * | * | F | F | * | T |
| 76190 | * | * | * | * | * | F | F | * | T |
| 76191 | * | * | * | * | * | F | F | * | T |
| 76192 | * | * | * | * | * | F | F | * | T |
| 76193 | * | * | * | * | * | F | F | * | T |
| 76194 | * | * | * | * | * | F | F | * | T |
| 76195 | * | * | * | * | * | F | F | * | T |
| 76196 | * | * | * | * | * | F | F | * | T |
| 76197 | * | * | * | * | * | F | F | * | T |
| 76198 | * | * | * | * | * | F | F | * | T |
| 76199 | * | * | * | * | * | F | F | * | T |
| 76200 | * | * | * | * | * | F | F | * | T |
| 76201 | * | * | * | * | * | F | F | * | T |
| 76202 | * | * | * | * | * | F | F | * | T |
| 76203 | * | * | * | * | * | F | F | * | T |
| 76204 | * | * | * | * | * | F | F | * | T |
| 76205 | * | * | * | * | * | F | F | * | T |
| 76206 | * | * | * | * | * | F | F | * | T |
| 76207 | * | * | * | * | * | F | F | * | T |
| 76208 | * | * | * | * | * | F | F | * | T |
| 76209 | * | * | * | * | * | F | F | * | T |
| 79227 | * | * | * | T | * | F | F | * | T |
| 79228 | * | * | * | * | * | F | F | * | T |
| 80774 | * | * | * | * | * | F | F | * | T |
| 80775 | * | * | * | * | * | F | F | * | T |
| 80776 | * | * | * | * | * | F | F | * | T |
| 80777 | * | * | * | * | * | F | F | * | T |
| 80778 | * | * | * | * | * | F | F | * | T |
| 81961 | * | * | * | * | * | F | F | * | T |
| 81962 | * | * | * | * | * | F | F | * | T |
| 81963 | * | * | * | * | * | F | F | * | T |
| 81964 | * | * | * | * | * | F | F | * | T |
| 81965 | * | * | * | * | * | F | F | * | T |
| 83023 | * | * | * | * | * | F | F | * | T |
| 83024 | * | * | * | * | * | F | F | * | T |
| 83025 | * | * | * | * | * | F | F | * | T |
| 83026 | * | * | * | * | * | F | F | * | T |
| 83027 | * | * | * | * | * | F | F | * | T |
| 92998 | * | * | * | * | * | F | T | F | T |
| 92999 | * | * | * | * | * | F | T | F | T |
| 93000 | * | * | * | * | * | F | T | F | T |
| 93001 | * | * | * | * | * | F | T | F | T |
| 93002 | * | * | * | * | * | F | T | F | T |
| 93003 | * | * | * | * | * | F | T | F | T |
| 93004 | * | * | * | * | * | F | T | F | T |
| 93005 | * | * | * | * | * | F | T | F | T |
| 111861 | * | * | * | * | * | F | T | F | T |
| 111862 | * | * | * | * | * | F | T | F | T |
| 111863 | * | * | * | * | * | F | T | F | T |
| 111864 | * | * | * | * | * | F | T | F | T |
| 111865 | * | * | * | * | * | F | T | F | T |
| 111866 | * | * | * | * | * | F | T | F | T |
| 111867 | * | * | * | * | * | F | T | F | T |
| 111868 | * | * | * | * | * | F | T | F | T |
| 130006 | * | * | * | * | * | F | T | T | T |
| 130007 | * | * | * | * | * | F | T | T | T |
| 130008 | * | * | * | * | * | F | T | T | T |
| 130009 | * | * | * | * | * | F | T | T | T |
| 131165 | * | * | * | * | * | F | T | T | T |
| 131166 | * | * | * | * | * | F | T | T | T |
| 131167 | * | * | * | * | * | F | T | T | T |
| 131168 | * | * | * | * | * | F | T | T | T |
| 132492 | * | * | * | * | * | F | T | T | T |
| 132493 | * | * | * | * | * | F | T | T | T |
| 132494 | * | * | * | * | * | F | T | T | T |
| 132495 | * | * | * | * | * | F | T | T | T |
Independent-effect pairs
c0(branch968): GAP view gap →scry_analyze_core::Interp::seq· br_if
inlined: lib.rs:4320 ← library/alloc/src/vec/mod.rs:1004 ← library/alloc/src/vec/mod.rs:1045c1(branch971): GAP view gap →scry_analyze_core::Interp::seq· br_if
inlined: lib.rs:4329 ← library/alloc/src/vec/mod.rs:1004 ← library/alloc/src/vec/mod.rs:1045c2(branch1009): GAP view gap →scry_analyze_core::Interp::seq· br_if
inlined: library/alloc/src/vec/spec_from_iter_nested.rs:60 ← library/alloc/src/vec/spec_extend.rs:27 ← library/alloc/src/vec/mod.rs:4027 ← library/core/src/iter/traits/iterator.rs:889 ← library/core/src/iter/adapters/map.rs:128 ← library/core/src/iter/adapters/enumerate.rs:146c3(branch1012): GAP view gap →scry_analyze_core::Interp::seq· br_ifc4(branch1014): DEAD view gap →scry_analyze_core::Interp::seq· br_if
inlined: lib.rs:2741 ← library/alloc/src/vec/mod.rs:1004 ← library/alloc/src/vec/mod.rs:1045c5(branch1044): GAP view gap →scry_analyze_core::Interp::seq· br_if
inlined: lib.rs:4030 ← library/alloc/src/vec/mod.rs:1004 ← library/alloc/src/vec/mod.rs:1045c6(branch1045): GAP view gap →scry_analyze_core::Interp::seq· br_if
inlined: lib.rs:4030 ← library/alloc/src/vec/mod.rs:1004 ← library/alloc/src/vec/mod.rs:1045c7(branch1046): GAP view gap →scry_analyze_core::Interp::seq· br_if
inlined: lib.rs:4030 ← library/alloc/src/vec/mod.rs:1004 ← library/alloc/src/vec/mod.rs:1045