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.
In the following snippet, Stainless complains that the
old
ininner1
may only occur in postcondition, even though that's the case:It seems to happen in the particular case where the variables are untouched.