Different verification behavior with `counterexample = true` vs `false`

[Patrick-6]

Prusti can verify the following code with check_overflows = false and counterexample = false. By using check_overflows = false and counterexample = true, an error will be shown on the marked line:

use prusti_contracts::*;

pub struct List {
    head: Link,
}

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

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

impl List {
    #[pure]
    pub fn len(&self) -> usize {
        self.head.len()
    }
}

impl Link {
    #[pure]
    #[requires(index < self.len())]
    pub fn lookup(&self, index: usize) -> i32 {
        match self {
            Link::More(node) => {
                if index == 0 {
                    node.elem
                } else {
                    node.next.lookup(index - 1) // <== The error is shown here
                }
            }
            Link::Empty => unreachable!(),
        }
    }

    #[pure]
    fn len(&self) -> usize {
        match self {
            Link::Empty => 0,
            Link::More(node) => 1 + node.next.len(),
        }
    }
}

Error with counterexample = true:

[Prusti: verification error] precondition might not hold.
test_crate.rs(26, 16): the failing assertion is here
test_crate.rs(27, 19): counterexample for "self"
  initial value: ref(test_crate::Link::More(
    ?,
  ))
  final value: ref(test_crate::Link::More(
    ?,
  ))
test_crate.rs(27, 26): counterexample for "index"
  initial value: 1
  final value: 1
test_crate.rs(29, 24): counterexample for "node"
  final value: ref(box(Node {
    elem: ?,
    next: ?,
  }))
test_crate.rs(27, 43): counterexample for result
  final value: 0