Incorrect usage of old when it is not

[mario-bucev]

In the following snippet, Stainless complains that the old in inner1 may only occur in postcondition, even though that's the case:

import stainless.lang.*

object OldInInnerFn {
  case class A(var i: BigInt)

  def outer1(a: A): Unit = {
    def inner1(a: A): Unit = {
      ()
    }.ensuring(_ => a.i == old(a).i) // "Stainless `old` can only occur in postconditions"
  }

  // This is ok
  def outer2(a: A): Unit = {
    def inner2(): Unit = {
    }.ensuring(_ => a.i == old(a).i)
  }
}

It seems to happen in the particular case where the variables are untouched.