Branching re-borrow causes permission error

[frececroka]

This can be verified:

extern crate prusti_contracts;

struct Point { x: u32, y: u32 }

fn f1<'a>(p: &'a mut Point) -> &'a mut u32 {
	if p.x == 0 {
		&mut p.x
	} else {
		&mut p.x
	}
}

This fails with an internal encoding error:

extern crate prusti_contracts;

struct Point { x: u32, y: u32 }

fn f1<'a>(p: &'a mut Point) -> &'a mut u32 {
	if p.x == 0 {
		&mut p.y
	} else {
		&mut p.x
	}
}

The error is internal encoding error - unregistered verification error: [unfold.failed:insufficient.permission] Unfolding u32(old[post](_1.val_ref).f$x) might fail. There might be insufficient permission to access old[post](_1.val_ref).f$x. (<no position>)

The problem seems to be that the predicates are not folded/unfolded correctly. I managed to get it to work by inserting/removing some folds/unfolds manually. The file main-fail.rs.vpr is the Viper encoding generated by Prusti and the file main-succeed.rs.vpr contains my modifications.