Quantifier panic when array size is greater than 64

[thanhnguyen-aws]

I tried this code:

const fn memchr_naive(x: u8, text: &[u8]) -> Option<usize> {
    let mut i = 0;
    #[kani::loop_invariant( i <= text.len() &&
        kani::forall!(|j in (0,i)| unsafe {*text.as_ptr().wrapping_add(j)} != x)
    )]
    while i < text.len() {
        if text[i] == x {
            return Some(i);
        }

        i += 1;
    }

    None
}

#[kani::proof]
#[kani::solver(cvc5)]
fn check_memchr_naive() {
    let x: u8 = kani::any();
    let text: [u8; 65] = kani::any();
    let _result = memchr_naive(x, &text);
}

using the following command line invocation:

kani src/main.rs -Zloop-contracts -Zquantifiers -Zmem-predicates 

with Kani version 0.64.0:

I expected to see this happen: VERIFICATION:- SUCCESSFUL

Instead, this happened: thread '' panicked at kani-driver/src/cbmc_output_parser.rs:470:25:

It will show "VERIFICATION:- SUCCESSFUL" for any array size <= 64, but will panic otherwise.

[zhassan-aws]

Most likely related to https://github.com/model-checking/kani/issues/2416

[tautschnig]

Just noting that this problem is actually different from the one in #2416. Further investigation required.