Decision #46 — library/alloc/src/collections/btree/node.rs:1827
Status: no_witness
Truth table
| row | c0 br 250 | c1 br 251 | outcome |
|---|---|---|---|
| 47 | T | * | T |
| 48 | T | * | T |
| 49 | T | * | T |
| 50 | T | * | T |
| 51 | T | * | T |
| 52 | T | * | T |
| 53 | T | * | T |
| 54 | T | * | T |
| 7007 | T | * | T |
| 7008 | T | * | T |
| 7009 | T | * | T |
| 7010 | T | * | T |
| 7011 | T | * | T |
| 7012 | T | * | T |
| 7013 | T | * | T |
| 7014 | T | * | T |
| 13745 | T | * | T |
| 13746 | T | * | T |
| 13747 | T | * | T |
| 13748 | T | * | T |
| 13749 | T | * | T |
| 13750 | T | * | T |
| 13751 | T | * | T |
| 13752 | T | * | T |
| 21186 | T | * | T |
| 21187 | T | * | T |
| 21188 | T | * | T |
| 23929 | T | * | T |
| 23930 | T | * | T |
| 23931 | T | * | T |
| 26572 | T | * | T |
| 26573 | T | * | T |
| 26574 | T | * | T |
| 29395 | T | * | T |
| 29396 | T | * | T |
| 29397 | T | * | T |
| 29398 | T | * | T |
| 29399 | T | * | T |
| 29400 | T | * | T |
| 29401 | T | * | T |
| 29402 | T | * | T |
| 29403 | T | * | T |
| 29404 | T | * | T |
| 29405 | T | * | T |
| 29406 | T | * | T |
| 50250 | T | * | T |
| 50251 | T | * | T |
| 50252 | T | * | T |
| 50253 | T | * | T |
| 50254 | T | * | T |
| 50255 | T | * | T |
| 50256 | T | * | T |
| 50257 | T | * | T |
| 50258 | T | * | T |
| 50259 | T | * | T |
| 50260 | T | * | T |
| 50261 | T | * | T |
| 70948 | T | * | T |
| 70949 | T | * | T |
| 70950 | T | * | T |
| 70951 | T | * | T |
| 70952 | T | * | T |
| 70953 | T | * | T |
| 70954 | T | * | T |
| 70955 | T | * | T |
| 70956 | T | * | T |
| 70957 | T | * | T |
| 80831 | T | * | T |
| 80832 | T | * | T |
| 80833 | T | * | T |
| 80834 | T | * | T |
| 80835 | T | * | T |
| 80836 | T | * | T |
| 80837 | T | * | T |
| 80838 | T | * | T |
| 80839 | T | * | T |
| 80840 | T | * | T |
| 90684 | T | * | T |
| 90685 | T | * | T |
| 90686 | T | * | T |
| 90687 | T | * | T |
| 90688 | T | * | T |
| 90689 | T | * | T |
| 90690 | T | * | T |
| 90691 | T | * | T |
| 90692 | T | * | T |
| 90693 | T | * | T |
| 90694 | T | * | T |
| 90695 | T | * | T |
| 98458 | T | * | T |
| 98459 | T | * | T |
| 98460 | T | * | T |
| 98461 | T | * | T |
| 98462 | T | * | T |
| 98463 | T | * | T |
| 98464 | T | * | T |
| 98465 | T | * | T |
| 98466 | T | * | T |
| 98467 | T | * | T |
| 98468 | T | * | T |
| 98469 | T | * | T |
| 106952 | T | * | T |
| 106953 | T | * | T |
| 106954 | T | * | T |
| 106955 | T | * | T |
| 106956 | T | * | T |
| 106957 | T | * | T |
| 106958 | T | * | T |
| 106959 | T | * | T |
| 106960 | T | * | T |
| 106961 | T | * | T |
| 106962 | T | * | T |
| 106963 | T | * | T |
| 115028 | T | * | T |
| 115029 | T | * | T |
| 115030 | T | * | T |
| 115031 | T | * | T |
| 115032 | T | * | T |
| 115033 | T | * | T |
| 115034 | T | * | T |
| 115035 | T | * | T |
| 115036 | T | * | T |
| 115037 | T | * | T |
| 115038 | T | * | T |
| 115039 | T | * | T |
| 122870 | T | * | T |
| 122871 | T | * | T |
| 122872 | T | * | T |
| 122873 | T | * | T |
| 122874 | T | * | T |
| 122875 | T | * | T |
| 122876 | T | * | T |
| 122877 | T | * | T |
| 122878 | T | * | T |
| 122879 | T | * | T |
| 139589 | T | * | T |
| 139590 | T | * | T |
| 139591 | T | * | T |
| 139592 | T | * | T |
| 139593 | T | * | T |
| 139594 | T | * | T |
| 139595 | T | * | T |
| 139596 | T | * | T |
| 139597 | T | * | T |
| 139598 | T | * | T |
| 156270 | T | * | T |
| 156271 | T | * | T |
| 156272 | T | * | T |
| 156273 | T | * | T |
| 156274 | T | * | T |
| 156275 | T | * | T |
| 156276 | T | * | T |
| 156277 | T | * | T |
| 156278 | T | * | T |
| 156279 | T | * | T |
| 156280 | T | * | T |
| 156281 | T | * | T |
| 156282 | T | * | T |
| 156283 | T | * | T |
| 156284 | T | * | T |
| 156285 | T | * | T |
| 156286 | T | * | T |
| 166128 | T | * | T |
| 166129 | T | * | T |
| 166130 | T | * | T |
| 166131 | T | * | T |
| 166132 | T | * | T |
| 166133 | T | * | T |
| 166134 | T | * | T |
| 166135 | T | * | T |
| 166136 | T | * | T |
| 166137 | T | * | T |
| 166138 | T | * | T |
| 166139 | T | * | T |
| 166140 | T | * | T |
| 166141 | T | * | T |
| 166142 | T | * | T |
| 166143 | T | * | T |
| 166144 | T | * | T |
| 175936 | T | * | T |
| 175937 | T | * | T |
| 175938 | T | * | T |
| 175939 | T | * | T |
| 175940 | T | * | T |
| 180742 | T | * | T |
| 180743 | T | * | T |
| 180744 | T | * | T |
| 184062 | T | * | T |
| 184063 | T | * | T |
| 184064 | T | * | T |
| 187169 | T | * | T |
| 187170 | T | * | T |
| 187171 | T | * | T |
| 190499 | T | * | T |
| 190500 | T | * | T |
| 190501 | T | * | T |
| 190502 | T | * | T |
| 190503 | T | * | T |
| 194709 | T | * | T |
| 194710 | T | * | T |
| 194711 | T | * | T |
| 194712 | T | * | T |
| 194713 | T | * | T |
| 194714 | T | * | T |
| 194715 | T | * | T |
| 194716 | T | * | T |
| 194717 | T | * | T |
| 194718 | T | * | T |
| 194719 | T | * | T |
| 194720 | T | * | T |
| 194721 | T | * | T |
| 194722 | T | * | T |
| 194723 | T | * | T |
| 194724 | T | * | T |
| 194725 | T | * | T |
| 194726 | T | * | T |
| 194727 | T | * | T |
| 202833 | T | * | T |
| 202834 | T | * | T |
| 202835 | T | * | T |
| 202836 | T | * | T |
| 202837 | T | * | T |
| 206060 | T | * | T |
| 206061 | T | * | T |
| 206062 | T | * | T |
| 206063 | T | * | T |
| 206064 | T | * | T |
| 206065 | T | * | T |
| 206066 | T | * | T |
| 206067 | T | * | T |
| 206068 | T | * | T |
| 206069 | T | * | T |
| 206070 | T | * | T |
| 206071 | T | * | T |
| 206072 | T | * | T |
| 206073 | T | * | T |
| 206074 | T | * | T |
| 206075 | T | * | T |
| 214435 | T | * | T |
| 214436 | T | * | T |
| 214437 | T | * | T |
| 214438 | T | * | T |
| 214439 | T | * | T |
| 214440 | T | * | T |
| 214441 | T | * | T |
| 214442 | T | * | T |
| 214443 | T | * | T |
| 214444 | T | * | T |
| 214445 | T | * | T |
| 214446 | T | * | T |
| 214447 | T | * | T |
| 222015 | T | * | T |
| 222016 | T | * | T |
| 222017 | T | * | T |
| 222018 | T | * | T |
| 222019 | T | * | T |
| 222020 | T | * | T |
| 222021 | T | * | T |
| 222022 | T | * | T |
| 222023 | T | * | T |
| 222024 | T | * | T |
| 222025 | T | * | T |
| 222026 | T | * | T |
| 299392 | T | * | T |
| 299393 | T | * | T |
| 299394 | T | * | T |
| 299395 | T | * | T |
| 299396 | T | * | T |
| 299397 | T | * | T |
| 299398 | T | * | T |
| 299399 | T | * | T |
| 299400 | T | * | T |
| 299401 | T | * | T |
| 299402 | T | * | T |
| 299403 | T | * | T |
| 376698 | T | * | T |
| 376699 | T | * | T |
| 376700 | T | * | T |
| 379335 | T | * | T |
| 379336 | T | * | T |
| 379337 | T | * | T |
| 382219 | T | * | T |
| 382220 | T | * | T |
| 382221 | T | * | T |
Independent-effect pairs
c0(branch250): 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:1009c1(branch251): 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:1009