class Program {
  var x: int;
  
  method a(a: seq<A>)
    requires |a| > 2;
    requires rd(a[*].f);
    requires forall i in [0..|a|-1] :: a[i] != null;
    requires a[0].f == 1;
    ensures rd(a[*].f);
  {
    assert rd(a[*].f);
    call b(a);
  }
  
  method b(a: seq<A>)
    requires |a| > 2;
    requires rd(a[*].f);
    requires forall i in [0..|a|-1] :: a[i] != null;
    requires a[0].f == 1;
    ensures rd(a[*].f);
  {
    assert rd(a[*].f);
  }
  
  method c(a: seq<A>)
    requires |a| > 2;
    requires rd(a[*].f);
    requires forall i in [0..|a|-1] :: a[i] != null;
    requires a[0].f == 1;
    ensures rd(a[*].f);
  {
    call void(a[1]);
    call void(a[0]);
  }
  
  method c1(a: seq<A>) // ERROR: should fail to verify postcondition
    requires |a| > 2;
    requires rd(a[*].f);
    requires forall i in [0..|a|-1] :: a[i] != null;
    requires a[0].f == 1;
    ensures rd(a[*].f);
  {
    call dispose(a[1]);
  }
  
  method d(a: seq<A>)
    requires |a| > 2;
    requires rd(a[*].f);
    requires forall i in [0..|a|-1] :: a[i] != null;
    requires a[0].f == 1;
    ensures rd*(a[*].f);
  {
    call dispose(a[1]); // we don't give away all the permission, thus verification succeeds
    
    var x: int;
    call x := some_number();
    call dispose(a[x]); // slighly more interesting, but still clearly ok
  }
  
  method e(a: seq<A>) // ERROR: should fail to verify postcondition
    requires |a| > 2;
    requires acc(a[*].f,10);
    requires forall i in [0..|a|-1] :: a[i] != null;
    requires a[0].f == 1;
    ensures rd*(a[*].f);
  {
    var x: int;
    call x := some_number();
    call dispose2(a[x]);
  }
  
  method some_number() returns (a: int)
    ensures 0 <= a && a < 3;
  {
    a := 1;
  }
  
  method dispose(a: A) requires rd(a.f); {}
  method dispose2(a: A) requires acc(a.f,10); {}
  method void(a: A) requires rd(a.f); ensures rd(a.f); {}
}

class A {
  var f: int;
}