Invariant mask analysis too strict

[wies]

The invariant mask analysis does not allow invariants to be allocated and discarded within the same scope. Example:

field f: Ref

inv p(x: Ref) {
  exists v: Ref :: own(x.f, v)
}

proc create() 
  returns (x: Ref)
  ensures p(x)
{
  x := new (f: null);
  fold p(x);
}

proc foo() 
{
  val x := create();
}

This leads to:

16 | {
      ^
Verification Error: Cannot call create. The invariant p required by create is not available in the current mask.