Wand Packaging Fails when a field is used alongside a function that requires it

[dewert99]

The following example fails:

field f: Int

function get_f(r: Ref): Int
requires acc(r.f) {
    r.f
}

method test0(x: Ref)
{
  package acc(x.f) && get_f(x) == x.f --* true
}

Looking at the generated Boogie:

...
// -- Check definedness of get_f(x) == x.f
            if (*) {
              // Exhale precondition of function application
              // Phase 1: pure assertions and fixed permissions
              perm := NoPerm;
              perm := perm + FullPerm;
              if (perm != NoPerm) {
                assert {:msg "  Precondition of function get_f might not hold. There might be insufficient permission to access x.f ([email protected]) [37]"}
                  perm <= Ops_1Mask[x, f_7];
              }
              Ops_1Mask[x, f_7] := Ops_1Mask[x, f_7] - perm;
              // Finish exhale
              havoc ExhaleHeap;
              b_1_1 := b_1_1 && IdenticalOnKnownLocations(Ops_1Heap, ExhaleHeap, Ops_1Mask);
              Ops_1Heap := ExhaleHeap;
              // Stop execution
              b_1_1 := false;
            }
            assert {:msg "  Packaging wand might fail. There might be insufficient permission to access x.f ([email protected]) [38]"}
              HasDirectPerm(Ops_1Mask, x, f_7);
            b_1_1 := b_1_1 && state(Ops_1Heap, Ops_1Mask);
...

It seems like instead of assuming false when we exhale the preconditions of get_f we just set b_1_1 to false. This does nothing to stop execution so we continue to assert access to x.f which we no longer have since we exhaled it.