Decision #610 — library/alloc/src/raw_vec/mod.rs:424
Status: partial
Truth table
| row | c0 br 4010 | c1 br 4013 | c2 br 4014 | c3 br 4028 | outcome |
|---|---|---|---|---|---|
| 16747 | T | * | * | * | T |
| 16748 | F | * | * | F | F |
| 16749 | T | * | * | * | T |
| 16750 | F | * | * | F | F |
| 26227 | T | * | * | * | T |
| 26228 | F | * | * | F | F |
| 26229 | T | * | * | * | T |
| 26230 | F | * | * | F | F |
| 35891 | * | F | F | * | F |
| 35892 | * | F | F | * | F |
| 35893 | * | F | F | * | F |
| 35894 | F | F | F | F | F |
| 35895 | * | F | F | * | F |
| 35896 | * | F | F | * | F |
| 35897 | * | F | F | * | F |
| 35898 | F | F | F | F | F |
| 42104 | * | F | F | * | F |
| 42105 | * | F | F | * | F |
| 42106 | * | F | F | * | F |
| 42107 | F | F | F | F | F |
| 42108 | * | F | F | * | F |
| 42109 | * | F | F | * | F |
| 42110 | * | F | F | * | F |
| 42111 | F | F | F | F | F |
| 65361 | T | F | F | * | F |
| 65362 | T | * | * | * | T |
| 65363 | F | * | * | F | F |
| 65364 | T | F | F | * | F |
| 65365 | T | * | * | * | T |
| 65366 | F | * | * | F | F |
| 76874 | T | F | F | * | F |
| 76875 | T | * | * | * | T |
| 76876 | F | * | * | F | F |
| 76877 | T | F | F | * | F |
| 76878 | T | * | * | * | T |
| 76879 | F | * | * | F | F |
| 118935 | * | F | F | * | F |
| 118936 | * | F | F | * | F |
| 118937 | * | F | F | * | F |
| 118938 | * | F | F | * | F |
| 118939 | * | F | F | * | F |
| 118940 | T | F | F | * | F |
| 118941 | F | * | * | F | F |
| 118942 | * | F | F | F | F |
| 118943 | * | F | F | * | F |
| 118944 | * | F | F | * | F |
| 118945 | * | F | F | * | F |
| 118946 | * | F | F | * | F |
| 118947 | T | F | F | * | F |
| 118948 | F | * | * | F | F |
| 118949 | * | * | * | F | F |
| 141871 | * | F | F | * | F |
| 141872 | * | F | F | * | F |
| 141873 | * | F | F | * | F |
| 141874 | * | F | F | * | F |
| 141875 | * | F | F | * | F |
| 141876 | T | F | F | * | F |
| 141877 | F | * | * | F | F |
| 141878 | * | F | F | F | F |
| 141879 | * | F | F | * | F |
| 141880 | * | F | F | * | F |
| 141881 | * | F | F | * | F |
| 141882 | * | F | F | * | F |
| 141883 | T | F | F | * | F |
| 141884 | F | * | * | F | F |
| 141885 | * | * | * | F | F |
Independent-effect pairs
c0(branch4010): PROVED — pair rows16747,16748(masking)<scry_analyze_core::Interp>::loop_region· br_if
inlined: lib.rs:4179 ← library/core/src/ptr/mod.rs:825 ← library/core/src/ptr/mod.rs:825c1(branch4013): GAP view gap →<scry_analyze_core::Interp>::loop_region· br_if
inlined: lib.rs:4185 ← library/core/src/ptr/mod.rs:825 ← library/core/src/ptr/mod.rs:825 ← library/core/src/ptr/mod.rs:825 ← library/core/src/ptr/mod.rs:825 ← library/core/src/ptr/mod.rs:825c2(branch4014): GAP view gap →<scry_analyze_core::Interp>::loop_region· br_if
inlined: lib.rs:4185 ← library/core/src/ptr/mod.rs:825 ← library/core/src/ptr/mod.rs:825 ← library/core/src/ptr/mod.rs:825 ← library/core/src/ptr/mod.rs:825 ← library/core/src/ptr/mod.rs:825c3(branch4028): GAP view gap →<scry_analyze_core::Interp>::loop_region· br_if
inlined: lib.rs:4206 ← library/core/src/ptr/mod.rs:825 ← library/core/src/ptr/mod.rs:825