Decision #38 — library/alloc/src/collections/btree/node.rs:1262
Status: no_witness
Truth table
| row | c0 br 216 | c1 br 217 | outcome |
|---|---|---|---|
| 29377 | T | T | T |
| 29378 | T | T | T |
| 29379 | T | T | T |
| 29380 | T | T | T |
| 29381 | T | T | T |
| 29382 | T | T | T |
| 50232 | T | T | T |
| 50233 | T | T | T |
| 50234 | T | T | T |
| 50235 | T | T | T |
| 50236 | T | T | T |
| 50237 | T | T | T |
| 122846 | T | T | T |
| 122847 | T | T | T |
| 122848 | T | T | T |
| 122849 | T | T | T |
| 122850 | T | T | T |
| 122851 | T | T | T |
| 122852 | T | T | T |
| 122853 | T | T | T |
| 139565 | T | T | T |
| 139566 | T | T | T |
| 139567 | T | T | T |
| 139568 | T | T | T |
| 139569 | T | T | T |
| 139570 | T | T | T |
| 139571 | T | T | T |
| 139572 | T | T | T |
Independent-effect pairs
c0(branch216): 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(branch217): 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_if