Reborrowing with enums and box results in Consistency error

[JonasAlaif]

The following example:

use prusti_contracts::*;
fn main(){}

fn id(x: &mut i32) -> &mut i32 { x }

fn get_mut(root: &mut Option<Box<i32>>) -> &mut i32 {
  if let Some(left) = root {
    id(left)
  } else { panic!() }
}

Runs into the error:

thread 'rustc' panicked at 'Consistency error: state has
pred _1.val_ref[enum_Some].f$0.val_ref, but not
acc _1.val_ref[enum_Some].f$0.val_ref', prusti-viper/src/encoder/foldunfold/state.rs:69:21