Repository navigation
Quantifier failure for arbitrary range #4310
Description
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.
Activity
tautschnig commentedon Aug 20, 2025
diffblue/cbmc#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.
feat(quantifiers): Support pointer arithmetic in quantifier predicates
feat(quantifiers): Support pointer arithmetic in quantifier predicates