fn copy2arr(src: &[u8], dst: &mut [u8]) -> usize {
    let mut index = 0;
    let l = dst.len();
    #[kani::loop_invariant( index <=l )]
    while (index < dst.len()) && (index < src.len()) {
        dst[index] = src[index];
        index += 1;
    }
    index
}

#[kani::proof]
#[kani::unwind(11)]
fn check_copy2arr() {
    let src: [u8; 10] = kani::any();
    let mut dst: [u8; 10] = kani::any();
    let i1: usize = kani::any_where(|i| *i <= src.len());
    let i2: usize = kani::any_where(|i| *i <= dst.len());
    let len = copy2arr(&src, &mut dst);
}