Incomplete boogie translation

[mattulbrich]

The following cannot be proved by boogie:

### project:
class C { var f : int; }

### decls:
o : C
a : array<int>

### sequent:
|- o.f == o.f@$heap[a[0] := 0]

### result:
prove

The translation is incomplete since the array-index 0 may alias with C$$f in the boogie translation.