Incorrect verification results when using quantifiers with arbitrary range #4226
Description
I tried this code:
#[kani::proof]
fn main() {
const N: usize = 100;
let a: [i32; N] = kani::any();
let i = kani::any();
kani::assume(i<N-1);
kani::assume(kani::forall!(|j in (1, i)| a[j] < 10));
kani::assume(a[i] < 10);
assert!(kani::forall!(|j in (1, i+1)| a[j] < 10));
}using the following command line invocation:
kani main.ra -Z quantifiers
with Kani version: 0.64.0
I expected to see this happen: VERIFICATION:- SUCCESSFUL
Instead, this happened: VERIFICATION:- FAILED
However, when I tried this code:
#[kani::proof]
fn main() {
const N: usize = 100;
let a: [i32; N] = kani::any();
let i = 20;
kani::assume(i<N-1);
kani::assume(kani::forall!(|j in (1, i)| a[j] < 10));
kani::assume(a[i] < 10);
assert!(kani::forall!(|j in (1, i+1)| a[j] < 10));
}Kani returns: VERIFICATION:- SUCCESSFUL
I suspect it is a bug from CBMC side. This bug is blocking using quantifiers in loop-invariants.