Aeneas Problem Case ( https://github.com/AeneasVerif/aeneas/issues/1223 )

main.rs

pub fn f(a: &mut i32, b: &mut i32, c: &mut i32, cond: bool) {
    let y;
    let z;
    if cond {
        y = &mut *a;
        z = &mut *b;
    } else {
        y = &mut *b;
        z = &mut *c;
    }
    *a += 1;
    *z += 1;
}

fn main() {
    let mut a = 3;
    let mut b = 4;
    let mut c = 5;
    f(&mut a, &mut b, &mut c, true);
    assert_eq!(a, 4);
    assert_eq!(b, 5);
    assert_eq!(c, 5);
}