// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
// RUN: %diff %s.n.expect %t
// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
// RUN: %diff %s.p.expect %t
// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
// RUN: %diff %s.a.expect %t


type Field a, Heap = <a>[ref, Field a]a;

function IsHeap(Heap) returns (bool);
const alloc : Field bool;

axiom (forall H:Heap, o:ref, f:Field ref ::
       IsHeap(H) && H[o,alloc] ==> H[H[o,f], alloc]);

procedure P() returns () {
  var h : Heap, o : ref, g : Field ref, i : Field ref, o2 : ref;
  assume IsHeap(h) && h[o, alloc];

  o2 := h[o, g];
  assert h[o2, alloc];

  o2 := h[o2, g];
  assert h[o2, alloc];

  h[o2, alloc] := false;

  o2 := h[o2, g];
  assert h[o2, alloc];      // should not be provable
}

type ref;