Incorrect translation of heap accesses inside let-expressions in functions

[marcoeilers]

The FunctionRecorder is unaware that the same variable can refer to different expressions when let-expressions are used in functions.
This can lead to very incorrect behavior, for example:

field f: Int

function fn(x: Ref, y: Ref): Int
    requires acc(x.f)
    requires acc(y.f)
{
    (let z == (x) in z.f) +
    (let z == (y) in z.f)
}

method m(x: Ref, y: Ref)
    requires acc(x.f) && x.f == 3
    requires acc(y.f) && y.f == 4
{
    var tmp: Int
    tmp := fn(x, y)
    assert tmp == 7  // fails but shouldn't
}

method m2(x: Ref, y: Ref)
    requires acc(x.f) && x.f == 3
    requires acc(y.f) && y.f == 4
{
    var tmp: Int
    tmp := fn(x, y)
    assert tmp == 6  // passes but shouldn't 
}

[marcoeilers]

Fixed in #928.