Internal Error with `counterexample = true`

[Patrick-6]

Attempting to verify the following code with the counterexample = true flag set, Prusti will panic:

use prusti_contracts::*;

pub struct List {
    head: Link,
}

enum Link {
    Empty,
    More(Box<Node>),
}

struct Node {
    elem: i32,
    next: Link,
}

//// \/ Without these lines, Prusti will not panic \/
impl List {
    #[pure]
    pub fn len(&self) -> usize {
        self.head.len()
    }
}
//// /\ Without these lines, Prusti will not panic /\

impl Link {
    #[pure]
    fn len(&self) -> usize {
        match self {
            Link::Empty => 0,
            Link::More(node) => 1 + node.next.len(), // <== Error should be shown here
        }
    }
}

Error:

thread 'rustc' panicked at 'called `Option::unwrap()` on a `None` value', prusti-viper\src\encoder\counterexamples\counterexample_translation.rs:257:22
stack backtrace:
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

error: internal compiler error: unexpected panic

note: Prusti or the compiler unexpectedly panicked. This is a bug.

note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new

note: Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:36:11 UTC

With counterexample = false or after removing the marked lines in the code, Prusti will correctly give the potential overflow in Link::len as an error.