class Cell {
  var x: int;
  
  invariant rd(x);
  
  method t1()
    requires acc(x);
    ensures rd(x) && rd(x);
  {
  }
  
  method t2()
    requires acc(x,1);
    ensures rd(x);
  {
    call void();
  }
  
  method t3()
    requires rd(x);
  {
    call t3helper();
  }
  
  method t3helper()
    requires rd(x) && rd(x);
    ensures rd(x) && rd(x);
  {}
  
  method t4()
    requires rd(x);
  {
    call dispose();
    call void(); // call succeeds, even though the precondition is also rd(x), and the next assertion fails
    assert(rd(x)); // ERROR: fails, as this check is done exactly (as it would in a postcondition)
  }
  
  method t5(n: int)
    requires acc(x);
  {
    var i: int := 0;
    call req99();
    while (i < n)
      invariant rd*(x);
    {
      call dispose();
      i := i+1
    }
  }
    
  method dispose() requires rd(x); {}
  method void() requires rd(x); ensures rd(x); {}
  method req99() requires acc(x,99); {}

}