Extra incorrect fold generated on non-trivial write to reborrowed field

[JonasAlaif]

The following snippet:

use prusti_contracts::*;
fn main() {}

fn foo(x: &mut (usize, usize)) {
    let f = &mut x.0;
    *f = 1 + 1; // *f = (1, 1).0; also fails
}

fails with the following error:

Folding usize(_1.val_ref.tuple_0) might fail. There might be insufficient permission to access self.val_int (@6.1)
[fold.failed:insufficient.permission] AssertMethodPostconditionTypeInvariants

The error is caused by an unnecessary fold after the update:

// Fold predicates for &mut args and transfer borrow permissions to old
fold acc(usize(_1.val_ref.tuple_0), write)

Thank you fold-unfold. Hopefully PCS fixes this soon and I don't have to dig around.