ApplyLetRec arguments are not properly mapped in postconditions

[jad-hamza]

The inside function is accepted by Stainless.

import stainless.lang._

object Test {

  def foo(): Unit = {
    var i = 0
    def isZero = i == 0

    def inside: Unit = {
      require(i <= 10)
      i += 1
    }.ensuring(_ =>
      isZero
    )

    inside
  }

}

The call isZero is transformed to isZero(i) where i refers to the initial value of i instead of the new value.