class C {
  var f: int;
  
  method t1(ch: C1)
    requires ch != null && rd(f);
    ensures true;
  {
    send ch(this) // ERROR
  }
  
  method t2(ch: C1)
    requires ch != null && acc(f);
    ensures true;
  {
    send ch(this)
  }
  
  method t3(ch: C2)
    requires ch != null && rd(f);
    ensures rd(f);
  {
    send ch(this)
    // ERROR: should fail to verify postcondition
  }
  
  method t4(ch: C1, a: C) returns (b: C)
    requires ch != null && credit(ch, 1) && rd(ch.mu) && waitlevel << ch;
    ensures rd*(b.f);
  {
    receive b := ch
  }
  
  method t5(ch: C1)
    requires ch != null && acc(f,1);
    ensures true;
  {
    send ch(this)
    send ch(this)
    send ch(this)
  }
  
}

channel C1(x: C) where rd(x.f);
channel C2(x: C) where rd*(x.f);