Internal error when assigning to an argument

[fpoli]

The program

fn foo<'a>(mut x: &'a mut i32, y: &'a mut i32) {
    x = y;
}

fails with an internal fold-unfold error. The workaround is to declare a new local variable x.

fn foo<'a>(mut x: &'a mut i32, y: &'a mut i32) {
    let mut x = x;
    x = y;
}

The fold-unfold is not at fault; the error is that the Viper encoding ends with

    _old$pre$0 = _1.val_ref
    _old$pre$1 = _2.val_ref
    exhale i32(_old$pre$0) && i32(_old$pre$1)

when the encoding above is such that _1.val_ref == _2.val_ref. One way to fix the encoding is to use an old(..) expression around those _old$pre$..:

    _old$pre$0 = old(_1.val_ref)
    _old$pre$1 = old(_2.val_ref)
    exhale i32(_old$pre$0) && i32(_old$pre$1)