unsupported feature: determining the region of a dereferentiation is not supported

[nishanthkarthik]

extern crate prusti_contracts;
use prusti_contracts::*;

fn external<'a>(t: &'a mut u32, r: &'a mut u32) -> &'a mut u32 {
    if *t == *r { t } else { r }
}

fn main() {
    let mut x = 1u32;
    let mut y = 1u32;
    let r: &mut u32 = external(&mut x, &mut y);
    *r += 0; // error
    x += *r - *r;
}

Prusti version: 0.2.2, commit 0d4a8d4 2024-03-26 13:08:03 UTC, built on 2024-03-26 13:20:57 UTC