Quantifier failure for arbitrary range

[thanhnguyen-aws]

I tried this code:

#[kani::proof]
#[kani::solver(cvc5)]
fn test_quantifier1() {
    let a: [u8; 32] = kani::any();
    let slice = kani::slice::any_slice_of_array(&a);
    let len = slice.len();
    kani::assume(kani::forall!(|i in (0,len)| unsafe {*slice.as_ptr().wrapping_add(i)} != 0));
    assert!(kani::forall!(|i in (0,len)| unsafe {*slice.as_ptr().wrapping_add(i)} != 0));
} 

#[kani::proof]
#[kani::solver(cvc5)]
fn test_quantifier2() {
    let a: [u8; 32] = kani::any();
    let slice = a.as_slice();
    let len: usize = kani::any_where(|x| *x > 0 && *x < 32);
    kani::assume(kani::forall!(|i in (0,len)| unsafe {*slice.as_ptr().wrapping_add(i)} != 0));
    assert!(kani::forall!(|i in (0,len)| unsafe {*slice.as_ptr().wrapping_add(i)} != 0));
} 

using the following command line invocation:

kani main.rs -Z quantifiers

with Kani version: 0.65.0

I expected to see this happen: VERIFICATION:- SUCCESSFUL

Instead, this happened:

thread '<unnamed>' (11829129) panicked at kani-driver/src/cbmc_output_parser.rs:470:25:
called `Result::unwrap()` on an `Err` value: Error("unknown variant `ERROR`, expected one of `FAILURE`, `COVERED`, `SATISFIED`, `SUCCESS`, `UNDETERMINED`, `UNKNOWN`, `UNREACHABLE`, `UNCOVERED`, `UNSATISFIABLE`", line: 12, column: 25)

I tried cvc4, z3, and bitwuzla.

[tautschnig]

https://github.com/diffblue/cbmc/pull/8703 fixes this problem for Z3, but it seems we may have to extend this workaround (on the CBMC side) to also cover other solvers. Also, the fix itself requires more work as the proposed solution does not currently work for nested quantifiers.