Poor performance scaling for string comparison function

[zhassan-aws]

I tried this code:

fn cmp_case_insensitive(s1: &str, s2: &str) -> bool {
    let chars1: Vec<char> = s1.chars().collect();
    let chars2: Vec<char> = s2.chars().collect();
    if chars1.len() != chars2.len() {
        return false;
    }
    for i in 0..chars1.len() {
        let c1 = chars1[i].to_ascii_lowercase();
        let c2 = chars2[i].to_ascii_lowercase();
        if c1 != c2 {
            return false;
        }
    }
    true
}


#[kani::proof]
#[kani::unwind(2)]
#[kani::solver(cadical)]
fn check_eq() {
    const N: usize = 1;
    let mut s1 = String::new();
    let mut s2 = String::new();
    for i in 0..N {
        let c: char = kani::any();
        s1.push(c);
        //let c1 = if kani::any() { c.to_ascii_uppercase() } else { c };
        let c1 = c.to_ascii_uppercase();
        s2.push(c1);
    }
    assert!(cmp_case_insensitive(&s1, &s2));
}

using the following command line invocation:

kani case_cmp.rs

with Kani version: 11ee9a1

This completes in ~23 seconds and the peak memory usage is ~1.3 GB.

If I bump N to 2 (which requires bumping the unwind to 3), it runs out of memory after exceeding 26 GB.

[zhassan-aws]

Performance scales much better (but is still poor) if I rewrite the string comparison function to avoid the usage of vectors as follows:

fn cmp_case_insensitive(s1: &str, s2: &str) -> bool {
    let mut chars1 = s1.chars();
    let mut chars2 = s2.chars();
    loop {
        let c1 = chars1.next();
        let c2 = chars2.next();
        match (c1, c2) {
            (Some(c1), Some(c2)) => {
                if c1.to_ascii_lowercase() != c2.to_ascii_lowercase() {
                    return false;
                }
            }
            (None, None) => break,
            _ => return false,
        }
    }
    true
}

N	Time (s)	Mem (GB)
1	4.2	0.2
2	46	1.2
3	205	3.8
4	707	9.2
5	2435	19.1