CBMC aborts with `l2_rename_rvalues case `struct' not handled` when a zero-sized closure is a loop_modifies target

[jrey8343]

Naming a zero-sized closure (a capture-free impl FnMut) as a #[kani::loop_modifies] target makes CBMC abort with l2_rename_rvalues case struct' not handled` (exit status 6) while applying the loop contract. The same message is tracked in #1257 / diffblue/cbmc#6911 for a different trigger (boxed fn items); this one comes from havocking a zero-sized struct-typed assigns target.

I tried this code (kani zst_closure.rs -Z loop-contracts):

#![feature(proc_macro_hygiene)]
#![feature(stmt_expr_attributes)]

fn count_kept(a: &mut [u8], mut keep: impl FnMut(&mut u8) -> bool) -> usize {
    let n = a.len();
    let mut i = 0;
    let mut kept = 0;
    #[kani::loop_invariant(i <= n && kept <= i)]
    #[kani::loop_modifies(&i, &kept, &keep, &raw mut *a)]
    while i < n {
        if keep(&mut a[i]) {
            kept += 1;
        }
        i += 1;
    }
    kept
}

#[kani::proof]
fn check() {
    let mut a: [u8; 8] = kani::any();
    let k = count_kept(&mut a, |x| { let keep: bool = kani::any(); if keep { *x = 0; } keep });
    assert!(k <= 8);
}

I expected to see this happen: verification succeeds (or Kani reports that a zero-sized target is not a valid loop_modifies target).

Instead, this happened:

Checking harness check...
l2_rename_rvalues case `struct' not handled

CBMC failed with status 6
VERIFICATION:- FAILED

Removing &keep from the loop_modifies list makes the harness verify. Listing the closure is natural when the loop calls a generic FnMut parameter (that is how VecDeque::retain_mut's loops look in model-checking/verify-rust-std#681, where I hit this), because a stateful closure would otherwise fail the assigns check.

Reproduced with Kani d4df833c (0.67.0-dev, 2026-01-18) and with current main (b07abe8, 2026-09-01), both with CBMC 6.8.0 on macOS/aarch64 (I could not test with the CBMC 6.11.0 that main pins).