Inconsistency in the encoding of Rust addresses as Viper Ref types

[fpoli]

An example to be fixed in the the ongoing Prusti rewrite:

use prusti_contracts::*;

#[requires(*x == a && a != b)]
//#[after_expiry(*x == before_expiry(*result))] // Does not verify, but it should
#[after_expiry(*x == a)] // Verifies, but it shouldn't
pub fn foo<T: Eq + Copy>(x: &mut T, a: T, b: T) -> &mut T {
    *x = b;
    x
}

#[requires(*x == a && a != b)]
pub fn bug(x: &mut u32, a: u32, b: u32) {
    let _ = foo(x, a, b);
    assert!(*x == a); // Verifies, but fails at runtime
}