Kani bounded proofs of the deployed Gate (tests/kani_gate_proofs.rs)
date: 2026-07-06T16:05:46Z  host: Linux 6.8.0-134-generic
cargo-kani 0.67.0
harnesses run against the real src/lib.rs Gate (submit/decide/cancel/close_run):
======================================================================
== bounded_ops_keep_state_consistent ==
Kani Rust Verifier 0.67.0 (cargo plugin)
    Finished `test` profile [unoptimized + debuginfo] target(s) in 0.12s
    Finished `test` profile [unoptimized + debuginfo] target(s) in 0.12s
    Finished `test` profile [unoptimized + debuginfo] target(s) in 0.11s
warning: Found the following unsupported constructs:
             - caller_location (1)
             - foreign function (2)
         
         Verification will fail if one or more of these constructs is reachable.
         See https://model-checking.github.io/kani/rust-feature-support.html for more details.

    Finished `test` profile [unoptimized + debuginfo] target(s) in 0.11s
    Finished `test` profile [unoptimized + debuginfo] target(s) in 0.12s
    Finished `test` profile [unoptimized + debuginfo] target(s) in 0.11s
Checking harness bounded_ops_keep_state_consistent...
CBMC 6.8.0 (cbmc-6.8.0)
CBMC version 6.8.0 (cbmc-6.8.0) 64-bit x86_64 linux
Reading GOTO program from file /home/neo/RustroverProjects/soundgate-paper/soundgate/target/kani/x86_64-unknown-linux-gnu/debug/deps/kani_gate_proofs-33f5835e847d7fcf__RNvCs49aLVd49DnG_16kani_gate_proofs33bounded_ops_keep_state_consistent.out
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 16 object bits, 48 offset bits (user-specified)
Starting Bounded Model Checking
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/node.rs line 670 column 9 function alloc::collections::btree::node::NodeRef::<alloc::collections::btree::node::marker::Mut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Leaf>::push_with_handle::<'_> thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/node.rs line 670 column 9 function alloc::collections::btree::node::NodeRef::<alloc::collections::btree::node::marker::Mut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Leaf>::push_with_handle::<'_> thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/node.rs line 670 column 9 function alloc::collections::btree::node::NodeRef::<alloc::collections::btree::node::marker::Mut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Leaf>::push_with_handle::<'_> thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/node.rs line 670 column 9 function alloc::collections::btree::node::NodeRef::<alloc::collections::btree::node::marker::Mut<'_>, (std::string::String, std::string::String), soundgate::Effect, alloc::collections::btree::node::marker::Leaf>::push_with_handle::<'_> thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/node.rs line 670 column 9 function alloc::collections::btree::node::NodeRef::<alloc::collections::btree::node::marker::Mut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Leaf>::push_with_handle::<'_> thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/map.rs line 2514 column 5 function std::collections::BTreeMap::<(std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST>::iter thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 635 column 19 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
Unwinding loop _RNvMsn_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree8navigateINtNtB7_4node7NodeRefNtNtB10_6marker5ImmutTNtNtBb_6string6StringB1E_ENtNtB7_7set_val9SetValZSTNtB1k_14LeafOrInternalE15first_leaf_edgeCs1VzAqnqXFcf_9soundgate.0 iteration 1 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 634 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 635 column 19 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
Unwinding loop _RNvMsn_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree8navigateINtNtB7_4node7NodeRefNtNtB10_6marker5ImmutTNtNtBb_6string6StringB1E_ENtNtB7_7set_val9SetValZSTNtB1k_14LeafOrInternalE15first_leaf_edgeCs1VzAqnqXFcf_9soundgate.0 iteration 2 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 634 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 635 column 19 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
Not unwinding loop _RNvMsn_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree8navigateINtNtB7_4node7NodeRefNtNtB10_6marker5ImmutTNtNtBb_6string6StringB1E_ENtNtB7_7set_val9SetValZSTNtB1k_14LeafOrInternalE15first_leaf_edgeCs1VzAqnqXFcf_9soundgate.0 iteration 3 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 634 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 227 column 15 function alloc::collections::btree::navigate::LazyLeafRange::<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST>::init_front thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/hint.rs line 111 column 14 function std::hint::unreachable_unchecked thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 231 column 55 function alloc::collections::btree::navigate::LazyLeafRange::<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST>::init_front thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 1014 column 15 function std::option::Option::<&mut alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Leaf>, alloc::collections::btree::node::marker::Edge>>::unwrap thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 2175 column 5 function std::option::unwrap_failed thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 1016 column 21 function std::option::Option::<&mut alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Leaf>, alloc::collections::btree::node::marker::Edge>>::unwrap thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 745 column 15 function std::option::Option::<std::ptr::NonNull<alloc::collections::btree::node::InternalNode<(std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST>>>::as_ref thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 1164 column 15 function std::option::Option::<&std::ptr::NonNull<alloc::collections::btree::node::InternalNode<(std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST>>>::map::<alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Internal>, alloc::collections::btree::node::marker::Edge>, {closure@alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>::ascend::{closure#0}}> thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 1338 column 15 function std::option::Option::<alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Internal>, alloc::collections::btree::node::marker::Edge>>::ok_or::<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>> thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Leaf>, alloc::collections::btree::node::marker::Edge>>::next_kv thread 0
Unwinding loop _RNvMsh_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree8navigateINtNtB7_4node6HandleINtB10_7NodeRefNtNtB10_6marker5ImmutTNtNtBb_6string6StringB1S_ENtNtB7_7set_val9SetValZSTNtB1y_4LeafENtB1y_4EdgeE7next_kvCs1VzAqnqXFcf_9soundgate.0 iteration 1 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 387 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Leaf>, alloc::collections::btree::node::marker::Edge>>::next_kv thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 745 column 15 function std::option::Option::<std::ptr::NonNull<alloc::collections::btree::node::InternalNode<(std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST>>>::as_ref thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 1164 column 15 function std::option::Option::<&std::ptr::NonNull<alloc::collections::btree::node::InternalNode<(std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST>>>::map::<alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Internal>, alloc::collections::btree::node::marker::Edge>, {closure@alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>::ascend::{closure#0}}> thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 1338 column 15 function std::option::Option::<alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Internal>, alloc::collections::btree::node::marker::Edge>>::ok_or::<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>> thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Leaf>, alloc::collections::btree::node::marker::Edge>>::next_kv thread 0
Unwinding loop _RNvMsh_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree8navigateINtNtB7_4node6HandleINtB10_7NodeRefNtNtB10_6marker5ImmutTNtNtBb_6string6StringB1S_ENtNtB7_7set_val9SetValZSTNtB1y_4LeafENtB1y_4EdgeE7next_kvCs1VzAqnqXFcf_9soundgate.0 iteration 2 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 387 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Leaf>, alloc::collections::btree::node::marker::Edge>>::next_kv thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 745 column 15 function std::option::Option::<std::ptr::NonNull<alloc::collections::btree::node::InternalNode<(std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST>>>::as_ref thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 1164 column 15 function std::option::Option::<&std::ptr::NonNull<alloc::collections::btree::node::InternalNode<(std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST>>>::map::<alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Internal>, alloc::collections::btree::node::marker::Edge>, {closure@alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>::ascend::{closure#0}}> thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 1338 column 15 function std::option::Option::<alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Internal>, alloc::collections::btree::node::marker::Edge>>::ok_or::<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>> thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Leaf>, alloc::collections::btree::node::marker::Edge>>::next_kv thread 0
Not unwinding loop _RNvMsh_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree8navigateINtNtB7_4node6HandleINtB10_7NodeRefNtNtB10_6marker5ImmutTNtNtBb_6string6StringB1S_ENtNtB7_7set_val9SetValZSTNtB1y_4LeafENtB1y_4EdgeE7next_kvCs1VzAqnqXFcf_9soundgate.0 iteration 3 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 387 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Leaf>, alloc::collections::btree::node::marker::Edge>>::next_kv thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/result.rs line 713 column 15 function std::result::Result::<alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>, alloc::collections::btree::node::marker::KV>, alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::ok thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 1014 column 15 function std::option::Option::<alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>, alloc::collections::btree::node::marker::KV>>::unwrap thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 2175 column 5 function std::option::unwrap_failed thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 1016 column 21 function std::option::Option::<alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>, alloc::collections::btree::node::marker::KV>>::unwrap thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/node.rs line 1687 column 15 function alloc::collections::btree::node::Handle::<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>, alloc::collections::btree::node::marker::KV>::force thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 718 column 15 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>, alloc::collections::btree::node::marker::KV>>::next_leaf_edge thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 635 column 19 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
Unwinding loop _RNvMsn_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree8navigateINtNtB7_4node7NodeRefNtNtB10_6marker5ImmutTNtNtBb_6string6StringB1E_ENtNtB7_7set_val9SetValZSTNtB1k_14LeafOrInternalE15first_leaf_edgeCs1VzAqnqXFcf_9soundgate.0 iteration 1 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 634 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 635 column 19 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
Unwinding loop _RNvMsn_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree8navigateINtNtB7_4node7NodeRefNtNtB10_6marker5ImmutTNtNtBb_6string6StringB1E_ENtNtB7_7set_val9SetValZSTNtB1k_14LeafOrInternalE15first_leaf_edgeCs1VzAqnqXFcf_9soundgate.0 iteration 2 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 634 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 635 column 19 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
Not unwinding loop _RNvMsn_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree8navigateINtNtB7_4node7NodeRefNtNtB10_6marker5ImmutTNtNtBb_6string6StringB1E_ENtNtB7_7set_val9SetValZSTNtB1k_14LeafOrInternalE15first_leaf_edgeCs1VzAqnqXFcf_9soundgate.0 iteration 3 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 634 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 1164 column 15 function std::option::Option::<(&(std::string::String, std::string::String), &alloc::collections::btree::set_val::SetValZST)>::map::<&(std::string::String, std::string::String), {closure@<std::collections::btree_map::Keys<'_, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST> as std::iter::Iterator>::next::{closure#0}}> thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 745 column 15 function std::option::Option::<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Owned, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::as_ref thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 2666 column 15 function <std::option::Option<&alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Owned, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>> as std::ops::Try>::branch thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani_core/src/models.rs line 176 column 17 function <usize as kani::rustc_intrinsics::ToISize>::to_isize thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function <usize as kani::rustc_intrinsics::ToISize>::to_isize thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function <usize as kani::rustc_intrinsics::ToISize>::to_isize thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function kani::mem::cbmc::same_allocation thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function kani::mem::cbmc::same_allocation thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 2666 column 15 function <std::option::Option<&(std::string::String, std::string::String)> as std::ops::Try>::branch thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/enumerate.rs line 80 column 17 function <std::iter::Enumerate<std::slice::Iter<'_, (std::string::String, std::string::String)>> as std::iter::Iterator>::next thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Not unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Not unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<(std::string::String, std::string::String)> thread 0
Unwinding loop _RINvMs0_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree6searchINtNtB8_4node7NodeRefNtNtBZ_6marker5ImmutTNtNtBc_6string6StringB1C_ENtNtB8_7set_val9SetValZSTNtB1j_14LeafOrInternalE14find_key_indexB1B_ECs1VzAqnqXFcf_9soundgate.0 iteration 1 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 225 column 9 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<(std::string::String, std::string::String)> thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function kani::mem::cbmc::same_allocation thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 2666 column 15 function <std::option::Option<&(std::string::String, std::string::String)> as std::ops::Try>::branch thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/enumerate.rs line 80 column 17 function <std::iter::Enumerate<std::slice::Iter<'_, (std::string::String, std::string::String)>> as std::iter::Iterator>::next thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Not unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Not unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<(std::string::String, std::string::String)> thread 0
Unwinding loop _RINvMs0_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree6searchINtNtB8_4node7NodeRefNtNtBZ_6marker5ImmutTNtNtBc_6string6StringB1C_ENtNtB8_7set_val9SetValZSTNtB1j_14LeafOrInternalE14find_key_indexB1B_ECs1VzAqnqXFcf_9soundgate.0 iteration 2 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 225 column 9 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<(std::string::String, std::string::String)> thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function kani::mem::cbmc::same_allocation thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 2666 column 15 function <std::option::Option<&(std::string::String, std::string::String)> as std::ops::Try>::branch thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/enumerate.rs line 80 column 17 function <std::iter::Enumerate<std::slice::Iter<'_, (std::string::String, std::string::String)>> as std::iter::Iterator>::next thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Not unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Not unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<(std::string::String, std::string::String)> thread 0
Not unwinding loop _RINvMs0_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree6searchINtNtB8_4node7NodeRefNtNtBZ_6marker5ImmutTNtNtBc_6string6StringB1C_ENtNtB8_7set_val9SetValZSTNtB1j_14LeafOrInternalE14find_key_indexB1B_ECs1VzAqnqXFcf_9soundgate.0 iteration 3 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 225 column 9 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<(std::string::String, std::string::String)> thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 203 column 15 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::search_node::<(std::string::String, std::string::String)> thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/node.rs line 1687 column 15 function alloc::collections::btree::node::Handle::<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>, alloc::collections::btree::node::marker::Edge>::force thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::search_tree::<(std::string::String, std::string::String)> thread 0
Unwinding loop _RINvMs_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree6searchINtNtB7_4node7NodeRefNtNtBY_6marker5ImmutTNtNtBb_6string6StringB1B_ENtNtB7_7set_val9SetValZSTNtB1i_14LeafOrInternalE11search_treeB1A_ECs1VzAqnqXFcf_9soundgate.0 iteration 1 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 57 column 9 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::search_tree::<(std::string::String, std::string::String)> thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani_core/src/models.rs line 176 column 17 function <usize as kani::rustc_intrinsics::ToISize>::to_isize thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function <usize as kani::rustc_intrinsics::ToISize>::to_isize thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function <usize as kani::rustc_intrinsics::ToISize>::to_isize thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function kani::mem::cbmc::same_allocation thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function kani::mem::cbmc::same_allocation thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 2666 column 15 function <std::option::Option<&(std::string::String, std::string::String)> as std::ops::Try>::branch thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/enumerate.rs line 80 column 17 function <std::iter::Enumerate<std::slice::Iter<'_, (std::string::String, std::string::String)>> as std::iter::Iterator>::next thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Not unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Not unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<(std::string::String, std::string::String)> thread 0
Unwinding loop _RINvMs0_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree6searchINtNtB8_4node7NodeRefNtNtBZ_6marker5ImmutTNtNtBc_6string6StringB1C_ENtNtB8_7set_val9SetValZSTNtB1j_14LeafOrInternalE14find_key_indexB1B_ECs1VzAqnqXFcf_9soundgate.0 iteration 1 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 225 column 9 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<(std::string::String, std::string::String)> thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function kani::mem::cbmc::same_allocation thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 2666 column 15 function <std::option::Option<&(std::string::String, std::string::String)> as std::ops::Try>::branch thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/enumerate.rs line 80 column 17 function <std::iter::Enumerate<std::slice::Iter<'_, (std::string::String, std::string::String)>> as std::iter::Iterator>::next thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Not unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Not unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<(std::string::String, std::string::String)> thread 0
Unwinding loop _RINvMs0_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree6searchINtNtB8_4node7NodeRefNtNtBZ_6marker5ImmutTNtNtBc_6string6StringB1C_ENtNtB8_7set_val9SetValZSTNtB1j_14LeafOrInternalE14find_key_indexB1B_ECs1VzAqnqXFcf_9soundgate.0 iteration 2 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 225 column 9 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<(std::string::String, std::string::String)> thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function kani::mem::cbmc::same_allocation thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 2666 column 15 function <std::option::Option<&(std::string::String, std::string::String)> as std::ops::Try>::branch thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/enumerate.rs line 80 column 17 function <std::iter::Enumerate<std::slice::Iter<'_, (std::string::String, std::string::String)>> as std::iter::Iterator>::next thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Not unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Not unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<(std::string::String, std::string::String)> thread 0
Not unwinding loop _RINvMs0_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree6searchINtNtB8_4node7NodeRefNtNtBZ_6marker5ImmutTNtNtBc_6string6StringB1C_ENtNtB8_7set_val9SetValZSTNtB1j_14LeafOrInternalE14find_key_indexB1B_ECs1VzAqnqXFcf_9soundgate.0 iteration 3 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 225 column 9 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<(std::string::String, std::string::String)> thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 203 column 15 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::search_node::<(std::string::String, std::string::String)> thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/node.rs line 1687 column 15 function alloc::collections::btree::node::Handle::<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>, alloc::collections::btree::node::marker::Edge>::force thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::search_tree::<(std::string::String, std::string::String)> thread 0
Unwinding loop _RINvMs_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree6searchINtNtB7_4node7NodeRefNtNtBY_6marker5ImmutTNtNtBb_6string6StringB1B_ENtNtB7_7set_val9SetValZSTNtB1i_14LeafOrInternalE11search_treeB1A_ECs1VzAqnqXFcf_9soundgate.0 iteration 2 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 57 column 9 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::search_tree::<(std::string::String, std::string::String)> thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani_core/src/models.rs line 176 column 17 function <usize as kani::rustc_intrinsics::ToISize>::to_isize thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function <usize as kani::rustc_intrinsics::ToISize>::to_isize thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function <usize as kani::rustc_intrinsics::ToISize>::to_isize thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function kani::mem::cbmc::same_allocation thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function kani::mem::cbmc::same_allocation thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 2666 column 15 function <std::option::Option<&(std::string::String, std::string::String)> as std::ops::Try>::branch thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/enumerate.rs line 80 column 17 function <std::iter::Enumerate<std::slice::Iter<'_, (std::string::String, std::string::String)>> as std::iter::Iterator>::next thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Not unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Not unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<(std::string::String, std::string::String)> thread 0
Unwinding loop _RINvMs0_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree6searchINtNtB8_4node7NodeRefNtNtBZ_6marker5ImmutTNtNtBc_6string6StringB1C_ENtNtB8_7set_val9SetValZSTNtB1j_14LeafOrInternalE14find_key_indexB1B_ECs1VzAqnqXFcf_9soundgate.0 iteration 1 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 225 column 9 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<(std::string::String, std::string::String)> thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function kani::mem::cbmc::same_allocation thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 2666 column 15 function <std::option::Option<&(std::string::String, std::string::String)> as std::ops::Try>::branch thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/enumerate.rs line 80 column 17 function <std::iter::Enumerate<std::slice::Iter<'_, (std::string::String, std::string::String)>> as std::iter::Iterator>::next thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Not unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Not unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<(std::string::String, std::string::String)> thread 0
Unwinding loop _RINvMs0_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree6searchINtNtB8_4node7NodeRefNtNtBZ_6marker5ImmutTNtNtBc_6string6StringB1C_ENtNtB8_7set_val9SetValZSTNtB1j_14LeafOrInternalE14find_key_indexB1B_ECs1VzAqnqXFcf_9soundgate.0 iteration 2 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 225 column 9 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<(std::string::String, std::string::String)> thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function kani::mem::cbmc::same_allocation thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 2666 column 15 function <std::option::Option<&(std::string::String, std::string::String)> as std::ops::Try>::branch thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/enumerate.rs line 80 column 17 function <std::iter::Enumerate<std::slice::Iter<'_, (std::string::String, std::string::String)>> as std::iter::Iterator>::next thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Not unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Not unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<(std::string::String, std::string::String)> thread 0
Not unwinding loop _RINvMs0_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree6searchINtNtB8_4node7NodeRefNtNtBZ_6marker5ImmutTNtNtBc_6string6StringB1C_ENtNtB8_7set_val9SetValZSTNtB1j_14LeafOrInternalE14find_key_indexB1B_ECs1VzAqnqXFcf_9soundgate.0 iteration 3 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 225 column 9 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<(std::string::String, std::string::String)> thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 203 column 15 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::search_node::<(std::string::String, std::string::String)> thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/node.rs line 1687 column 15 function alloc::collections::btree::node::Handle::<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>, alloc::collections::btree::node::marker::Edge>::force thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::search_tree::<(std::string::String, std::string::String)> thread 0
Not unwinding loop _RINvMs_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree6searchINtNtB7_4node7NodeRefNtNtBY_6marker5ImmutTNtNtBb_6string6StringB1B_ENtNtB7_7set_val9SetValZSTNtB1i_14LeafOrInternalE11search_treeB1A_ECs1VzAqnqXFcf_9soundgate.0 iteration 3 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 57 column 9 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::search_tree::<(std::string::String, std::string::String)> thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function std::collections::BTreeMap::<(std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST>::get::<(std::string::String, std::string::String)> thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 745 column 15 function std::option::Option::<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Owned, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::as_ref thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 2666 column 15 function <std::option::Option<&alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Owned, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>> as std::ops::Try>::branch thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani_core/src/models.rs line 176 column 17 function <usize as kani::rustc_intrinsics::ToISize>::to_isize thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function <usize as kani::rustc_intrinsics::ToISize>::to_isize thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function <usize as kani::rustc_intrinsics::ToISize>::to_isize thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function kani::mem::cbmc::same_allocation thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function kani::mem::cbmc::same_allocation thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 2666 column 15 function <std::option::Option<&std::string::String> as std::ops::Try>::branch thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/enumerate.rs line 80 column 17 function <std::iter::Enumerate<std::slice::Iter<'_, std::string::String>> as std::iter::Iterator>::next thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Not unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<str> thread 0
Unwinding loop _RINvMs0_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree6searchINtNtB8_4node7NodeRefNtNtBZ_6marker5ImmutNtNtBc_6string6StringNtNtB8_7set_val9SetValZSTNtB1j_14LeafOrInternalE14find_key_indexeECs1VzAqnqXFcf_9soundgate.0 iteration 1 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 225 column 9 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<str> thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function kani::mem::cbmc::same_allocation thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 2666 column 15 function <std::option::Option<&std::string::String> as std::ops::Try>::branch thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/enumerate.rs line 80 column 17 function <std::iter::Enumerate<std::slice::Iter<'_, std::string::String>> as std::iter::Iterator>::next thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Not unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<str> thread 0
Unwinding loop _RINvMs0_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree6searchINtNtB8_4node7NodeRefNtNtBZ_6marker5ImmutNtNtBc_6string6StringNtNtB8_7set_val9SetValZSTNtB1j_14LeafOrInternalE14find_key_indexeECs1VzAqnqXFcf_9soundgate.0 iteration 2 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 225 column 9 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<str> thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function kani::mem::cbmc::same_allocation thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 2666 column 15 function <std::option::Option<&std::string::String> as std::ops::Try>::branch thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/enumerate.rs line 80 column 17 function <std::iter::Enumerate<std::slice::Iter<'_, std::string::String>> as std::iter::Iterator>::next thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Not unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<str> thread 0
Not unwinding loop _RINvMs0_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree6searchINtNtB8_4node7NodeRefNtNtBZ_6marker5ImmutNtNtBc_6string6StringNtNtB8_7set_val9SetValZSTNtB1j_14LeafOrInternalE14find_key_indexeECs1VzAqnqXFcf_9soundgate.0 iteration 3 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 225 column 9 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<str> thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 203 column 15 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::search_node::<str> thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/node.rs line 1687 column 15 function alloc::collections::btree::node::Handle::<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>, alloc::collections::btree::node::marker::Edge>::force thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::search_tree::<str> thread 0
Unwinding loop _RINvMs_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree6searchINtNtB7_4node7NodeRefNtNtBY_6marker5ImmutNtNtBb_6string6StringNtNtB7_7set_val9SetValZSTNtB1i_14LeafOrInternalE11search_treeeECs1VzAqnqXFcf_9soundgate.0 iteration 1 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 57 column 9 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::search_tree::<str> thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani_core/src/models.rs line 176 column 17 function <usize as kani::rustc_intrinsics::ToISize>::to_isize thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function <usize as kani::rustc_intrinsics::ToISize>::to_isize thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function <usize as kani::rustc_intrinsics::ToISize>::to_isize thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function kani::mem::cbmc::same_allocation thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function kani::mem::cbmc::same_allocation thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 2666 column 15 function <std::option::Option<&std::string::String> as std::ops::Try>::branch thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/enumerate.rs line 80 column 17 function <std::iter::Enumerate<std::slice::Iter<'_, std::string::String>> as std::iter::Iterator>::next thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Not unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<str> thread 0
Unwinding loop _RINvMs0_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree6searchINtNtB8_4node7NodeRefNtNtBZ_6marker5ImmutNtNtBc_6string6StringNtNtB8_7set_val9SetValZSTNtB1j_14LeafOrInternalE14find_key_indexeECs1VzAqnqXFcf_9soundgate.0 iteration 1 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 225 column 9 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<str> thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function kani::mem::cbmc::same_allocation thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 2666 column 15 function <std::option::Option<&std::string::String> as std::ops::Try>::branch thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/enumerate.rs line 80 column 17 function <std::iter::Enumerate<std::slice::Iter<'_, std::string::String>> as std::iter::Iterator>::next thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Not unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<str> thread 0
Unwinding loop _RINvMs0_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree6searchINtNtB8_4node7NodeRefNtNtBZ_6marker5ImmutNtNtBc_6string6StringNtNtB8_7set_val9SetValZSTNtB1j_14LeafOrInternalE14find_key_indexeECs1VzAqnqXFcf_9soundgate.0 iteration 2 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 225 column 9 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<str> thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function kani::mem::cbmc::same_allocation thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 2666 column 15 function <std::option::Option<&std::string::String> as std::ops::Try>::branch thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/enumerate.rs line 80 column 17 function <std::iter::Enumerate<std::slice::Iter<'_, std::string::String>> as std::iter::Iterator>::next thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Not unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<str> thread 0
Not unwinding loop _RINvMs0_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree6searchINtNtB8_4node7NodeRefNtNtBZ_6marker5ImmutNtNtBc_6string6StringNtNtB8_7set_val9SetValZSTNtB1j_14LeafOrInternalE14find_key_indexeECs1VzAqnqXFcf_9soundgate.0 iteration 3 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 225 column 9 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<str> thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 203 column 15 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::search_node::<str> thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/node.rs line 1687 column 15 function alloc::collections::btree::node::Handle::<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>, alloc::collections::btree::node::marker::Edge>::force thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::search_tree::<str> thread 0
Unwinding loop _RINvMs_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree6searchINtNtB7_4node7NodeRefNtNtBY_6marker5ImmutNtNtBb_6string6StringNtNtB7_7set_val9SetValZSTNtB1i_14LeafOrInternalE11search_treeeECs1VzAqnqXFcf_9soundgate.0 iteration 2 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 57 column 9 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::search_tree::<str> thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani_core/src/models.rs line 176 column 17 function <usize as kani::rustc_intrinsics::ToISize>::to_isize thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function <usize as kani::rustc_intrinsics::ToISize>::to_isize thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function <usize as kani::rustc_intrinsics::ToISize>::to_isize thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function kani::mem::cbmc::same_allocation thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function kani::mem::cbmc::same_allocation thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 2666 column 15 function <std::option::Option<&std::string::String> as std::ops::Try>::branch thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/enumerate.rs line 80 column 17 function <std::iter::Enumerate<std::slice::Iter<'_, std::string::String>> as std::iter::Iterator>::next thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Not unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<str> thread 0
Unwinding loop _RINvMs0_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree6searchINtNtB8_4node7NodeRefNtNtBZ_6marker5ImmutNtNtBc_6string6StringNtNtB8_7set_val9SetValZSTNtB1j_14LeafOrInternalE14find_key_indexeECs1VzAqnqXFcf_9soundgate.0 iteration 1 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 225 column 9 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<str> thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function kani::mem::cbmc::same_allocation thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 2666 column 15 function <std::option::Option<&std::string::String> as std::ops::Try>::branch thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/enumerate.rs line 80 column 17 function <std::iter::Enumerate<std::slice::Iter<'_, std::string::String>> as std::iter::Iterator>::next thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Not unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<str> thread 0
Unwinding loop _RINvMs0_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree6searchINtNtB8_4node7NodeRefNtNtBZ_6marker5ImmutNtNtBc_6string6StringNtNtB8_7set_val9SetValZSTNtB1j_14LeafOrInternalE14find_key_indexeECs1VzAqnqXFcf_9soundgate.0 iteration 2 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 225 column 9 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<str> thread 0
aborting path on assume(false) at file /home/runner/work/kani/kani/library/kani/src/lib.rs line 57 column 1 function kani::mem::cbmc::same_allocation thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 2666 column 15 function <std::option::Option<&std::string::String> as std::ops::Try>::branch thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/enumerate.rs line 80 column 17 function <std::iter::Enumerate<std::slice::Iter<'_, std::string::String>> as std::iter::Iterator>::next thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Not unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<str> thread 0
Not unwinding loop _RINvMs0_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree6searchINtNtB8_4node7NodeRefNtNtBZ_6marker5ImmutNtNtBc_6string6StringNtNtB8_7set_val9SetValZSTNtB1j_14LeafOrInternalE14find_key_indexeECs1VzAqnqXFcf_9soundgate.0 iteration 3 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 225 column 9 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::find_key_index::<str> thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 203 column 15 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::search_node::<str> thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/node.rs line 1687 column 15 function alloc::collections::btree::node::Handle::<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>, alloc::collections::btree::node::marker::Edge>::force thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::search_tree::<str> thread 0
Not unwinding loop _RINvMs_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree6searchINtNtB7_4node7NodeRefNtNtBY_6marker5ImmutNtNtBb_6string6StringNtNtB7_7set_val9SetValZSTNtB1i_14LeafOrInternalE11search_treeeECs1VzAqnqXFcf_9soundgate.0 iteration 3 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/search.rs line 57 column 9 function alloc::collections::btree::search::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, std::string::String, alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::search_tree::<str> thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function std::collections::BTreeMap::<std::string::String, alloc::collections::btree::set_val::SetValZST>::get::<str> thread 0
Unwinding loop _RNvMs_Cs1VzAqnqXFcf_9soundgateNtB4_4Gate20kani_invariants_hold.0 iteration 1 file /home/neo/RustroverProjects/soundgate-paper/soundgate/src/lib.rs line 320 column 9 function soundgate::Gate::kani_invariants_hold thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 635 column 19 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
Unwinding loop _RNvMsn_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree8navigateINtNtB7_4node7NodeRefNtNtB10_6marker5ImmutTNtNtBb_6string6StringB1E_ENtNtB7_7set_val9SetValZSTNtB1k_14LeafOrInternalE15first_leaf_edgeCs1VzAqnqXFcf_9soundgate.0 iteration 1 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 634 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 635 column 19 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
Unwinding loop _RNvMsn_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree8navigateINtNtB7_4node7NodeRefNtNtB10_6marker5ImmutTNtNtBb_6string6StringB1E_ENtNtB7_7set_val9SetValZSTNtB1k_14LeafOrInternalE15first_leaf_edgeCs1VzAqnqXFcf_9soundgate.0 iteration 2 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 634 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 635 column 19 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
Not unwinding loop _RNvMsn_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree8navigateINtNtB7_4node7NodeRefNtNtB10_6marker5ImmutTNtNtBb_6string6StringB1E_ENtNtB7_7set_val9SetValZSTNtB1k_14LeafOrInternalE15first_leaf_edgeCs1VzAqnqXFcf_9soundgate.0 iteration 3 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 634 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 227 column 15 function alloc::collections::btree::navigate::LazyLeafRange::<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST>::init_front thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/hint.rs line 111 column 14 function std::hint::unreachable_unchecked thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 231 column 55 function alloc::collections::btree::navigate::LazyLeafRange::<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST>::init_front thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 1014 column 15 function std::option::Option::<&mut alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Leaf>, alloc::collections::btree::node::marker::Edge>>::unwrap thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 2175 column 5 function std::option::unwrap_failed thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 1016 column 21 function std::option::Option::<&mut alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Leaf>, alloc::collections::btree::node::marker::Edge>>::unwrap thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 745 column 15 function std::option::Option::<std::ptr::NonNull<alloc::collections::btree::node::InternalNode<(std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST>>>::as_ref thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 1164 column 15 function std::option::Option::<&std::ptr::NonNull<alloc::collections::btree::node::InternalNode<(std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST>>>::map::<alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Internal>, alloc::collections::btree::node::marker::Edge>, {closure@alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>::ascend::{closure#0}}> thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 1338 column 15 function std::option::Option::<alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Internal>, alloc::collections::btree::node::marker::Edge>>::ok_or::<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>> thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Leaf>, alloc::collections::btree::node::marker::Edge>>::next_kv thread 0
Unwinding loop _RNvMsh_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree8navigateINtNtB7_4node6HandleINtB10_7NodeRefNtNtB10_6marker5ImmutTNtNtBb_6string6StringB1S_ENtNtB7_7set_val9SetValZSTNtB1y_4LeafENtB1y_4EdgeE7next_kvCs1VzAqnqXFcf_9soundgate.0 iteration 1 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 387 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Leaf>, alloc::collections::btree::node::marker::Edge>>::next_kv thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 745 column 15 function std::option::Option::<std::ptr::NonNull<alloc::collections::btree::node::InternalNode<(std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST>>>::as_ref thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 1164 column 15 function std::option::Option::<&std::ptr::NonNull<alloc::collections::btree::node::InternalNode<(std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST>>>::map::<alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Internal>, alloc::collections::btree::node::marker::Edge>, {closure@alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>::ascend::{closure#0}}> thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 1338 column 15 function std::option::Option::<alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Internal>, alloc::collections::btree::node::marker::Edge>>::ok_or::<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>> thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Leaf>, alloc::collections::btree::node::marker::Edge>>::next_kv thread 0
Unwinding loop _RNvMsh_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree8navigateINtNtB7_4node6HandleINtB10_7NodeRefNtNtB10_6marker5ImmutTNtNtBb_6string6StringB1S_ENtNtB7_7set_val9SetValZSTNtB1y_4LeafENtB1y_4EdgeE7next_kvCs1VzAqnqXFcf_9soundgate.0 iteration 2 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 387 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Leaf>, alloc::collections::btree::node::marker::Edge>>::next_kv thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 745 column 15 function std::option::Option::<std::ptr::NonNull<alloc::collections::btree::node::InternalNode<(std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST>>>::as_ref thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 1164 column 15 function std::option::Option::<&std::ptr::NonNull<alloc::collections::btree::node::InternalNode<(std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST>>>::map::<alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Internal>, alloc::collections::btree::node::marker::Edge>, {closure@alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>::ascend::{closure#0}}> thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 1338 column 15 function std::option::Option::<alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Internal>, alloc::collections::btree::node::marker::Edge>>::ok_or::<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>> thread 0
aborting path on assume(false) at file tests/kani_gate_proofs.rs line 0 column 0 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Leaf>, alloc::collections::btree::node::marker::Edge>>::next_kv thread 0
Not unwinding loop _RNvMsh_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree8navigateINtNtB7_4node6HandleINtB10_7NodeRefNtNtB10_6marker5ImmutTNtNtBb_6string6StringB1S_ENtNtB7_7set_val9SetValZSTNtB1y_4LeafENtB1y_4EdgeE7next_kvCs1VzAqnqXFcf_9soundgate.0 iteration 3 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 387 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::Leaf>, alloc::collections::btree::node::marker::Edge>>::next_kv thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/result.rs line 713 column 15 function std::result::Result::<alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>, alloc::collections::btree::node::marker::KV>, alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::ok thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 1014 column 15 function std::option::Option::<alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>, alloc::collections::btree::node::marker::KV>>::unwrap thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 2175 column 5 function std::option::unwrap_failed thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 1016 column 21 function std::option::Option::<alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>, alloc::collections::btree::node::marker::KV>>::unwrap thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/node.rs line 1687 column 15 function alloc::collections::btree::node::Handle::<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>, alloc::collections::btree::node::marker::KV>::force thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 718 column 15 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>, alloc::collections::btree::node::marker::KV>>::next_leaf_edge thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 635 column 19 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
Unwinding loop _RNvMsn_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree8navigateINtNtB7_4node7NodeRefNtNtB10_6marker5ImmutTNtNtBb_6string6StringB1E_ENtNtB7_7set_val9SetValZSTNtB1k_14LeafOrInternalE15first_leaf_edgeCs1VzAqnqXFcf_9soundgate.0 iteration 1 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 634 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 635 column 19 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
Unwinding loop _RNvMsn_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree8navigateINtNtB7_4node7NodeRefNtNtB10_6marker5ImmutTNtNtBb_6string6StringB1E_ENtNtB7_7set_val9SetValZSTNtB1k_14LeafOrInternalE15first_leaf_edgeCs1VzAqnqXFcf_9soundgate.0 iteration 2 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 634 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 635 column 19 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
Not unwinding loop _RNvMsn_NtNtNtCs6NSMbdZCE7r_5alloc11collections5btree8navigateINtNtB7_4node7NodeRefNtNtB10_6marker5ImmutTNtNtBb_6string6StringB1E_ENtNtB7_7set_val9SetValZSTNtB1k_14LeafOrInternalE15first_leaf_edgeCs1VzAqnqXFcf_9soundgate.0 iteration 3 file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 634 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Immut<'_>, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
aborting path on assume(false) at file /home/runner/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 1164 column 15 function std::option::Option::<(&(std::string::String, std::string::String), &alloc::collections::btree::set_val::SetValZST)>::map::<&(std::string::String, std::string::String), {closure@<std::collections::btree_map::Keys<'_, (std::string::String, std::string::String), alloc::collections::btree::set_val::SetValZST> as std::iter::Iterator>::next::{closure#0}}> thread 0
