`#[kani::loop_decreases]` combined with `#[kani::loop_modifies]` causes verification failure

[feliperodri]

When #[kani::loop_decreases] and #[kani::loop_modifies] are both applied to the same loop, CBMC's goto-instrument produces incorrect instrumentation, causing spurious verification failures. Each attribute works correctly in isolation.

Steps to reproduce

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

#[kani::proof]
fn check_decreases_with_modifies() {
    let mut x: u32 = 10;
    #[kani::loop_invariant(x <= 10)]
    #[kani::loop_modifies(&x)]
    #[kani::loop_decreases(x)]
    while x > 0 {
        x -= 1;
    }
    assert!(x == 0);
}

Expected behavior

Verification succeeds — the loop terminates (decreases x) and only modifies x.

Actual behavior

Verification fails with assigns clause or decreases check failures.

Root cause

The with_loop_decreases and with_loop_modifies builders in stmt.rs each clone the other's field when constructing the annotated Goto statement. However, the order in which goto-instrument processes these annotations may cause conflicts in the instrumented code.

Workaround

Use loop_decreases without loop_modifies, or vice versa. For termination proofs, loop_decreases + loop_invariant (without loop_modifies) is sufficient.