Loop invariant spuriously fails in `for x in a` syntax

[tautschnig]

For the following example we can always prove the .iter().enumerate() approach, but proving a loop invariant when the loop syntax is for x in a hinges on array field sensitivity in CBMC:

#![feature(proc_macro_hygiene)]
#![feature(stmt_expr_attributes)]
#[kani::proof]
fn forloop() {
    const SIZE: u32 = 100;
    let mut sum: u32 = 0;
    let a: [u8; SIZE as usize] = kani::any();
    kani::assume(kani::forall!(|i in (0,SIZE as usize)| a[i] <= 20));
    // The following loop invariant holds
    #[kani::loop_invariant(sum <= (kani::index as u32 * 20) )]
    for (i, j) in a.iter().enumerate() {
        sum = sum + (*j as u32) ;
    }
    assert!(sum <= 20 * SIZE);
    sum = 0;
    // Kani claims the following loop invariant doesn't hold when SIZE > 65, or really greater than
    // whatever value we have for CBMC's maximum array field sensitivity setting: it passes when N
    // >= SIZE in
    // --cbmc-args --max-field-sensitivity-array-size N
    // and fails whenever N is chosen to be less than SIZE.
    #[kani::loop_invariant(sum <= (kani::index as u32 * 20) )]
    for x in a {
        sum = sum + x as u32;
    }
    assert!(sum <= 20 * SIZE);
}