Closure spec causes the variable to be incorrectly captured

[arnaudgolfouse]

The following code:

#[requires(p.0@ == 1)]
#[ensures(result@ == 2)]
fn disjoint_captures(mut p: (i32, i32)) -> i32 {
    let p0 = &p.0;
    let mut clos = #[ensures(p.1@ == 1)] || {
        p.1 = 1;
    };
    clos();
    *p0 + p.1
}

When using edition 2021, should at least compile (it does without the specifications), but the closure's spec causes a borrow error:

error[E0502]: cannot borrow `p` as mutable because it is also borrowed as immutable
  --> /.../test.rs:5:42
   |
4  |     let p0 = &p.0;
   |              ---- immutable borrow occurs here
5  |     let mut clos = #[ensures(p.1@ == 1)] || {
   |                              ---         ^^ mutable borrow occurs here
   |                              |
   |                              second borrow occurs due to use of `p` in closure
6  |         p.1 = 1;
   |         --- capture is mutable because of use here
...
10 |     *p0 + p.1
   |     --- immutable borrow later used here