Decision #47 — library/alloc/src/collections/btree/node.rs:558
Status: no_witness
Truth table
| row | c0 br 255 | c1 br 260 | outcome |
|---|---|---|---|
| 55 | F | * | F |
| 56 | F | * | F |
| 57 | F | * | F |
| 58 | F | * | F |
| 59 | F | * | F |
| 7015 | F | * | F |
| 7016 | F | * | F |
| 7017 | F | * | F |
| 7018 | F | * | F |
| 7019 | F | * | F |
| 13753 | F | * | F |
| 13754 | F | * | F |
| 13755 | F | * | F |
| 13756 | F | * | F |
| 13757 | F | * | F |
| 21189 | F | * | F |
| 21190 | F | * | F |
| 23932 | F | * | F |
| 23933 | F | * | F |
| 26575 | F | * | F |
| 26576 | F | * | F |
| 29407 | F | * | F |
| 29408 | F | * | F |
| 29409 | F | * | F |
| 29410 | F | * | F |
| 29411 | F | * | F |
| 29412 | F | * | F |
| 29413 | F | * | F |
| 29414 | F | * | F |
| 29415 | F | * | F |
| 50262 | F | * | F |
| 50263 | F | * | F |
| 50264 | F | * | F |
| 50265 | F | * | F |
| 50266 | F | * | F |
| 50267 | F | * | F |
| 50268 | F | * | F |
| 50269 | F | * | F |
| 50270 | F | * | F |
| 70958 | F | * | F |
| 70959 | F | * | F |
| 70960 | F | * | F |
| 70961 | F | * | F |
| 70962 | F | * | F |
| 70963 | F | * | F |
| 70964 | F | * | F |
| 70965 | F | * | F |
| 70966 | F | * | F |
| 80841 | F | * | F |
| 80842 | F | * | F |
| 80843 | F | * | F |
| 80844 | F | * | F |
| 80845 | F | * | F |
| 80846 | F | * | F |
| 80847 | F | * | F |
| 80848 | F | * | F |
| 80849 | F | * | F |
| 90696 | F | * | F |
| 90697 | F | * | F |
| 90698 | F | * | F |
| 90699 | F | * | F |
| 90700 | F | * | F |
| 90701 | F | * | F |
| 90702 | F | * | F |
| 90703 | F | * | F |
| 90704 | F | * | F |
| 98470 | F | * | F |
| 98471 | F | * | F |
| 98472 | F | * | F |
| 98473 | F | * | F |
| 98474 | F | * | F |
| 98475 | F | * | F |
| 98476 | F | * | F |
| 98477 | F | * | F |
| 98478 | F | * | F |
| 106964 | F | * | F |
| 106965 | F | * | F |
| 106966 | F | * | F |
| 106967 | F | * | F |
| 106968 | F | * | F |
| 106969 | F | * | F |
| 106970 | F | * | F |
| 106971 | F | * | F |
| 106972 | F | * | F |
| 115040 | F | * | F |
| 115041 | F | * | F |
| 115042 | F | * | F |
| 115043 | F | * | F |
| 115044 | F | * | F |
| 115045 | F | * | F |
| 115046 | F | * | F |
| 115047 | F | * | F |
| 115048 | F | * | F |
| 122880 | F | * | F |
| 122881 | F | * | F |
| 122882 | F | * | F |
| 122883 | F | * | F |
| 122884 | F | * | F |
| 122885 | F | * | F |
| 122886 | F | * | F |
| 122887 | F | * | F |
| 122888 | F | * | F |
| 139599 | F | * | F |
| 139600 | F | * | F |
| 139601 | F | * | F |
| 139602 | F | * | F |
| 139603 | F | * | F |
| 139604 | F | * | F |
| 139605 | F | * | F |
| 139606 | F | * | F |
| 139607 | F | * | F |
| 156287 | F | * | F |
| 156288 | F | * | F |
| 156289 | F | * | F |
| 156290 | F | * | F |
| 156291 | F | * | F |
| 156292 | F | * | F |
| 156293 | F | * | F |
| 156294 | F | * | F |
| 156295 | F | * | F |
| 156296 | F | * | F |
| 166145 | F | * | F |
| 166146 | F | * | F |
| 166147 | F | * | F |
| 166148 | F | * | F |
| 166149 | F | * | F |
| 166150 | F | * | F |
| 166151 | F | * | F |
| 166152 | F | * | F |
| 166153 | F | * | F |
| 166154 | F | * | F |
| 175941 | F | * | F |
| 175942 | F | * | F |
| 175943 | F | * | F |
| 175944 | F | * | F |
| 180745 | F | * | F |
| 180746 | F | * | F |
| 184065 | F | * | F |
| 184066 | F | * | F |
| 187172 | F | * | F |
| 187173 | F | * | F |
| 190504 | F | * | F |
| 190505 | F | * | F |
| 190506 | F | * | F |
| 190507 | F | * | F |
| 194728 | F | * | F |
| 194729 | F | * | F |
| 194730 | F | * | F |
| 194731 | F | * | F |
| 194732 | F | * | F |
| 194733 | F | * | F |
| 194734 | F | * | F |
| 194735 | F | * | F |
| 194736 | F | * | F |
| 194737 | F | * | F |
| 194738 | F | * | F |
| 194739 | F | * | F |
| 194740 | F | * | F |
| 194741 | F | * | F |
| 202838 | F | * | F |
| 202839 | F | * | F |
| 202840 | F | * | F |
| 202841 | F | * | F |
| 206076 | F | * | F |
| 206077 | F | * | F |
| 206078 | F | * | F |
| 206079 | F | * | F |
| 206080 | F | * | F |
| 206081 | F | * | F |
| 206082 | F | * | F |
| 206083 | F | * | F |
| 206084 | F | * | F |
| 206085 | F | * | F |
| 206086 | F | * | F |
| 214448 | F | * | F |
| 214449 | F | * | F |
| 214450 | F | * | F |
| 214451 | F | * | F |
| 214452 | F | * | F |
| 214453 | F | * | F |
| 214454 | F | * | F |
| 214455 | F | * | F |
| 214456 | F | * | F |
| 214457 | F | * | F |
| 214458 | F | * | F |
| 222027 | F | * | F |
| 222028 | F | * | F |
| 222029 | F | * | F |
| 222030 | F | * | F |
| 222031 | F | * | F |
| 222032 | F | * | F |
| 222033 | F | * | F |
| 222034 | F | * | F |
| 222035 | F | * | F |
| 299404 | F | * | F |
| 299405 | F | * | F |
| 299406 | F | * | F |
| 299407 | F | * | F |
| 299408 | F | * | F |
| 299409 | F | * | F |
| 299410 | F | * | F |
| 299411 | F | * | F |
| 299412 | F | * | F |
| 376701 | F | * | F |
| 376702 | F | * | F |
| 376703 | F | * | F |
| 379338 | F | * | F |
| 379339 | F | * | F |
| 379340 | F | * | F |
| 382222 | F | * | F |
| 382223 | F | * | F |
| 382224 | F | * | F |
Independent-effect pairs
c0(branch255): GAP view gap →<alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Mut, alloc::string::String, u32, alloc::collections::btree::node::marker::Leaf>, alloc::collections::btree::node::marker::Edge>>::insert::<alloc::alloc::Global>· br_if
inlined: library/alloc/src/collections/btree/node.rs:1030 ← library/alloc/src/collections/btree/node.rs:1013c1(branch260): DEAD view gap →<alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Mut, alloc::string::String, u32, alloc::collections::btree::node::marker::Leaf>, alloc::collections::btree::node::marker::Edge>>::insert::<alloc::alloc::Global>· br_if
inlined: library/alloc/src/collections/btree/node.rs:1030 ← library/alloc/src/collections/btree/node.rs:1013