Internal Error from matching on generic `enum` in pure function

[Patrick-6]

Using any of these 3 pure test_* functions in another function causes an error:

use prusti_contracts::*;

enum Opt<T> {
    Nil,
    Some(T)
}

impl<T> Opt<T> {
    #[pure]
    fn test_0(&self) {
        prusti_assert!(matches!(self, Opt::Nil));
    }

    #[pure]
    fn test_1(&self) {
        prusti_assert!(match self {Opt::Nil => true, _ => false});
    }

    #[pure]
    fn test_2(&self) {
        prusti_assert!(match self {Opt::Some(_) => true, _ => false});
    }
}

fn bug_trigger(x: Opt<i64>) {
    x.test_0();
    // x.test_1();
    // x.test_2();
}

Error:

thread 'rustc' panicked at 'called `Result::unwrap()` on an `Err` value:
FailedToObtain(Pred(Field(FieldExpr { base: Field(FieldExpr { base: Field(FieldExpr { base: Local(Local { variable: self:
Ref(closure$m_uncategorized_problems$$prusti_panic$$Opt$$$openang$T$closeang$$$test_0$$$opencur$closure$sharp$0$closecur$),
  position: Position { line: 0, column: 0, id: 0 } }), field: closure_0:
Ref(ref$ref$m_uncategorized_problems$$prusti_panic$$Opt$_beg_$__TYPARAM__$_T$0$__$_end_),
  position: Position { line: 0, column: 0, id: 0 } }),
field: val_ref: Ref(ref$m_uncategorized_problems$$prusti_panic$$Opt$_beg_$__TYPARAM__$_T$0$__$_end_),
  position: Position { line: 0, column: 0, id: 0 } }),
field: val_ref: Ref(m_uncategorized_problems$$prusti_panic$$Opt$_beg_$__TYPARAM__$_T$0$__$_end_),
  position: Position { line: 0, column: 0, id: 0 } }), read))',
prusti-viper\src\encoder\snapshot\encoder.rs:1917:10

error: internal compiler error: unexpected panic
note: Prusti version: 0.2.1, commit 52cb249 2023-03-23 13:11:26 UTC, built on 2023-03-23 13:22:15 UTC

The error is triggered from here.

Required conditions for this error:

• test_* must be #[pure]
• enum Opt must be generic; changing it to store an explicit type like i64 or struct TestStruct {} will not trigger the error

Manually expanding the matches macro still triggers the error (test_1 and test_2). Matching on either of the enum variants trigger the error.