Permissions in function precondition not correctly checked when using --enableMoreCompleteExhale

[mschwerhoff]

@niomaster reported that the following snippet unsoundly verifies when using the experimental option --enableMoreCompleteExhale:

field f: Int

function req(x: Ref): Bool
  requires acc(x.f, 2/1)
{ true }

method test(x: Ref) {
  inhale acc(x.f)
  assert req(x) // Fails only without --enableMoreCompleteExhale (and should fail)
  assert false  // Fails even with --enableMoreCompleteExhale (and should fail)
}

[marcoeilers]

This was fixed in #682