Quantifier failure in loop invariant

[thanhnguyen-aws]

I tried this code:

#[kani::proof]
fn main() {
    let a: [usize; 60] = kani::any();
    kani::assume(kani::forall!(|i in (0,60)| a[i] <= 20));
    let mut b: [usize; 60] = a.clone();
    let mut i = 0;
    #[kani::loop_invariant( i<= 60 && kani::forall!(|j in (0, i)| b[j] == a[j]+ 1))]
    while i < 60 {
        b[i] = a[i] + 1;
        i += 1;
    }
} 

using the following command line invocation:

kani main.rs -Z loop-contracts -Z quantifiers

with Kani version: 0.64.0

I expected to see this happen: VERIFICATION:- SUCCESSFUL

Instead, this happened:

warning: ignoring forall
  * type: bool
  0: tuple
... (very long)

Failed Checks: Check invariant after step for loop main2.0

When I try to add #[kani::solver(cvc5)]

The output is:

Running SMT2 ALL (with FPA) using CVC5
SMT2 solver returned "unknown"
Runtime Solver: 0.216097s
Runtime decision procedure: 0.222155s

thread '<unnamed>' 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)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

[tautschnig]

What about Z3 instead of cvc5?

[thanhnguyen-aws]

Here is Z3's result:

Checking harness main3...
CBMC 6.7.1 (cbmc-6.7.1)
CBMC version 6.7.1 (cbmc-6.7.1) 64-bit arm64 macos
Reading GOTO program from file /Users/ntson/kanitest/src/main__RNvCs9wCRUdekRrZ_4main5main3.out
Generating GOTO Program
Adding CPROVER library (arm64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 16 object bits, 48 offset bits (user-specified)
Starting Bounded Model Checking
Unwinding loop _RNvCs9wCRUdekRrZ_4main5main3.0 iteration 1 file src/main.rs line 283 column 5 function main3 thread 0
aborting path on assume(false) at file src/main.rs line 283 column 5 function main3 thread 0
Runtime Symex: 0.0672837s
size of program expression: 1931 steps
slicing removed 676 assignments
Generated 247 VCC(s), 28 remaining after simplification
Runtime Postprocess Equation: 0.000421292s
Passing problem to SMT2 QF_AUFBV using Z3
converting SSA
Runtime Convert SSA: 0.00556333s
Running SMT2 QF_AUFBV using Z3
SMT2 solver returned non-constant value for variable B237
Runtime Solver: 1.1154s
Runtime decision procedure: 1.1211s

thread '<unnamed>' (13113089) 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)
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

[tautschnig]

We'll need a Z3 release that includes the fix for Z3Prover/z3#7743 or the workaround in CBMC in diffblue/cbmc#8703 to be merged. Bitwuzla usually works fine in such situations, but it might take a lot longer to complete.