Decision #41 — library/alloc/src/collections/btree/node.rs:1876
Status: no_witness
Truth table
| row | c0 br 229 | c1 br 230 | outcome |
|---|---|---|---|
| 29383 | T | * | T |
| 29384 | T | * | T |
| 29385 | T | * | T |
| 29386 | T | * | T |
| 29387 | T | * | T |
| 29388 | T | * | T |
| 50238 | T | * | T |
| 50239 | T | * | T |
| 50240 | T | * | T |
| 50241 | T | * | T |
| 50242 | T | * | T |
| 50243 | T | * | T |
| 122854 | T | * | T |
| 122855 | T | * | T |
| 122856 | T | * | T |
| 122857 | T | * | T |
| 122858 | T | * | T |
| 122859 | T | * | T |
| 122860 | T | * | T |
| 122861 | T | * | T |
| 139573 | T | * | T |
| 139574 | T | * | T |
| 139575 | T | * | T |
| 139576 | T | * | T |
| 139577 | T | * | T |
| 139578 | T | * | T |
| 139579 | T | * | T |
| 139580 | T | * | T |
Independent-effect pairs
c0(branch229): GAP view gap →<alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Mut, u32, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Leaf>, alloc::collections::btree::node::marker::KV>>::remove_leaf_kv::<<alloc::collections::btree::map::entry::OccupiedEntry<u32, alloc::collections::btree::set_val::SetValZST>>::remove_kv::{closure#0}, alloc::alloc::Global>· br_ifc1(branch230): DEAD view gap →<alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Mut, u32, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Leaf>, alloc::collections::btree::node::marker::KV>>::remove_leaf_kv::<<alloc::collections::btree::map::entry::OccupiedEntry<u32, alloc::collections::btree::set_val::SetValZST>>::remove_kv::{closure#0}, alloc::alloc::Global>· br_if