Consistency error: Labelled-old expressions are not allowed in postconditions.

[Pointerbender]

The following Rust program:

use prusti_contracts::*;

#[derive(Clone, Copy)]
pub struct A;

#[derive(Clone, Copy, PartialEq, Eq)]
pub struct B(usize);

impl A {
    #[pure]
    #[trusted]
    #[ensures(b == old(b))]
    pub fn foo(a: &A, b: B) {}

    pub fn bar(&self) {
        let b = B(1);
        Self::foo(self, b);
    }
}

Results in a Viper error:

error: [Prusti internal error] Prusti encountered an unexpected internal error
  |
  = note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
  = note: Details: consistency error in prusti_example::A::bar: Consistency error: No matching identifier pre found of type Label. (@26.20)

error: [Prusti internal error] Prusti encountered an unexpected internal error
  |
  = note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
  = note: Details: consistency error in prusti_example::A::bar: Consistency error: Labelled-old expressions are not allowed in postconditions. (@26.15)

The offending Viper code in the program for A::bar is:

function m_foo__$TY$__(_1: Snap$struct$m_A, _2: Snap$struct$m_B): Snap$tuple0$
  requires true
  requires true
  ensures _2 == old[pre](_2)

Here it looks like an old[pre] is retained from the post-condition of A::foo that should not be retained because A::foo is a pure function (or a user-friendly warning would also be nice if this is not supported intentionally). The MIR for A::bar is:

[vakaras]

Pure functions are not allowed to mutate observable state, so we should forbid old in the postconditions of pure functions.