Unexpected behaviour difference function application vs. asserting precondition

[mschwerhoff]

The example below illustrates a difference in behaviour between invoking a function — which entails asserting its precondition — and explicitly asserting the function's precondition: in the former case, the precondition is not assumed to hold afterwards.

field f: Int

function foo(x: Ref): Bool 
  requires acc(x.f)

method test(x: Ref) {
  inhale acc(x.f) && x.f == 1
  var y: Ref
  
  assert foo(y)    // Error: insuff. permissions
  assert acc(y.f)  // Error: insuff. permissions
  
  assert y.f == 1 // No error, thanks to assert
}