Loop invariant does not work properly for `slice` type

[thanhnguyen-aws]

I tried this code:

fn main() {
    let mut a: [u8; 10] = kani::any();
    let mut s = a.as_slice();
    let mut bytes = s;
    let mut index = 0;
    let mut l = bytes.len();

    #[kani::loop_invariant( bytes.len() == l )]
    while index < s.len() {
        bytes = &s[index..];
        index += 1;
        l = bytes.len();
    }
} 

using the following command line invocation:

kani main.rs -Zloop-contracts

with Kani version: 0.64.0

I expected to see this happen: VERIFICATION:- SUCCESSFUL

Instead, this happened:
Failed Checks: Check invariant after step for loop main2.0
VERIFICATION:- FAILED

[thanhnguyen-aws]

I figured out where the problem is and am trying to fix it. It is blocking the implementation of while let loop.