Performance drastically differs across two string indexing operations

[zhassan-aws]

For the following program:

#[kani::proof]
#[kani::unwind(5)]
fn main() {
    let buf: [u8; 4] = kani::any();
    if let Ok(s) = std::str::from_utf8(&buf) {
        let c: char = kani::any();
        if let Some(index) = s.find(c) {
            let slice = &s[index..];
            //let slice = s.get(index..).unwrap();
            assert!(slice.chars().next() == Some(c));
        }
    }
}

CBMC's memory usage exceeds 24 GB after running for 2 minutes. These are the last few lines it prints before running out of memory:

Runtime Symex: 44.498s
size of program expression: 889131 steps
slicing removed 550833 assignments
Generated 63496 VCC(s), 27179 remaining after simplification
Runtime Postprocess Equation: 0.942692s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 22.1197s

For the commented-out version of the slice indexing operation (which is supposedly equivalent), verification is successful in ~26 seconds with less than 1 GB of memory usage:

$ kani str_slice_perf.rs
...
Runtime Symex: 2.71987s
size of program expression: 73171 steps
slicing removed 55203 assignments
Generated 3677 VCC(s), 2301 remaining after simplification
Runtime Postprocess Equation: 0.0965727s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.708747s
...
SUMMARY:
 ** 0 of 581 failed (16 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 25.568632s

[zhassan-aws]

To double check that the two versions are equivalent, I wrote this harness:

#[kani::proof]
#[kani::unwind(4)]
fn main() {
    let buf: [u8; 3] = kani::any();
    if let Ok(s) = std::str::from_utf8(&buf) {
        let index = kani::any_where(|i| *i <= s.len() && s.is_char_boundary(*i));
        let slice1 = &s[index..];
        let slice2 = s.get(index..).unwrap();
        assert!(slice1 == slice2);
    }
}

which successfully verifies (up to 3 bytes). Beyond 3 bytes, it runs out of memory.