Decision #81 — library/alloc/src/raw_vec/mod.rs:425
Status: no_witness
Truth table
| row | c0 br 444 | c1 br 445 | c2 br 446 | c3 br 454 | outcome |
|---|---|---|---|---|---|
| 29417 | F | * | * | * | F |
| 29418 | F | * | * | * | F |
| 29419 | F | * | * | * | F |
| 29420 | F | * | * | * | F |
| 29421 | F | * | * | * | F |
| 29422 | F | * | * | * | F |
| 50272 | F | * | * | * | F |
| 50273 | F | * | * | * | F |
| 50274 | F | * | * | * | F |
| 50275 | F | * | * | * | F |
| 50276 | F | * | * | * | F |
| 50277 | F | * | * | * | F |
| 122890 | F | * | * | * | F |
| 122891 | F | * | * | * | F |
| 122892 | F | * | * | * | F |
| 122893 | F | * | * | * | F |
| 122894 | F | * | * | * | F |
| 122895 | F | * | * | * | F |
| 122896 | F | * | * | * | F |
| 122897 | F | * | * | * | F |
| 139609 | F | * | * | * | F |
| 139610 | F | * | * | * | F |
| 139611 | F | * | * | * | F |
| 139612 | F | * | * | * | F |
| 139613 | F | * | * | * | F |
| 139614 | F | * | * | * | F |
| 139615 | F | * | * | * | F |
| 139616 | F | * | * | * | F |
Independent-effect pairs
c0(branch444): GAP view gap →<alloc::collections::btree::map::entry::OccupiedEntry<u32, alloc::collections::btree::set_val::SetValZST>>::remove_kv· br_if
inlined: lib.rs:6555 ← library/core/src/ptr/mod.rs:823 ← library/core/src/ptr/mod.rs:823c1(branch445): DEAD view gap →<alloc::collections::btree::map::entry::OccupiedEntry<u32, alloc::collections::btree::set_val::SetValZST>>::remove_kv· br_ifc2(branch446): DEAD view gap →<alloc::collections::btree::map::entry::OccupiedEntry<u32, alloc::collections::btree::set_val::SetValZST>>::remove_kv· br_ifc3(branch454): DEAD view gap →<alloc::collections::btree::map::entry::OccupiedEntry<u32, alloc::collections::btree::set_val::SetValZST>>::remove_kv· br_if