class C {
  method m() {
    assert 4 + (a * 5) + (2 + 3) * (a + a);
    a := a + 3;
    b := a - b - c + 4 * d + 20 + --25;
    b := ((((a - b) - c) + 4 * d) + 20) + --25;
    c := a - (b - (c + (4 * d + (20 + 25))));
    assert (X ==> Y) ==> Z <==> A ==> B ==> C;
    assume A && B && (C || D || E) && F;
    var x;
    var y := 12 + !(x.f.g).h - (!x).f + (!x.f);
    var z := new C;
    y := new D;
    o.f := 5;
    (a + b).y := new T;
    reorder (2 ==(O != 3)) != O between a,b,c and x,y,z;
    reorder X ==> Y below x+5;
    reorder o.f above this, null;
    share o;
    unshare o;
    acquire o;
    release o;
    rd acquire o;
    rd release o;
    downgrade o;
    var tok: token<C.m>;
    fork tok := o.m();
    join tok;
    assert rd(x) + acc(y) + acc(z, 1/4) + old(old(k)) + null.f;
    x := this.f;
    call m(2,3,4);
    call this.m(2,3,4);
    call a,b,c := o.m();
    call x := m(200);
    reorder o above waitlevel;
  }
  method p(a,b,c) returns (x,y,z)
    requires 8 + 2 == 10;
    ensures 8 + 5 > 10;
    requires x == y+1;
    ensures old(x) < x;
  {
    if (x == 7) {
      y := y + 1;  z := z + 2;
    } else if (x == 8) {
      y := 2;
    } else {
      z := 10;
    }
    {  // empty block
    }
    if (x == 9) { }
    if (x == 10) { x := 10; } else { }
    var n := 0;
    while (n < 100) { n := n - 1; }
    while (n != 0)
      invariant n % 2 == 0;
      invariant sqrt2 * sqrt2 == 2;
    {
      n := n - 2;
    }
    call v,x := s.M(65);
  }
}
class D { }

// ----- tests specifically of implicit locals in CALL and RECEIVE statements

class ImplicitC {
  var k: int;

  method MyMethod() returns (x: int, y: ImplicitC)
    requires acc(k)
    ensures acc(y.k) && x < y.k
  {
    x := k - 15;
    y := this;
  }

  method B0() {
    var c := new ImplicitC;
    call a, b := c.MyMethodX();  // error: method not found (so what is done with a,b?)
    assert a < b.k;
  }

  method B1() {
    var c := new ImplicitC;
    call a, a := c.MyMethod();  // error: a occurs twice
    assert a < b.k;
  }

  method D0() {
    var ch := new Ch;
    var c := new ImplicitC;
    send ch(c.k - 15, c);  // give ourselves some credit
    receive a, b := chX;  // error: channel not found (so what is done with a,b?)
    assert a < b.k;
  }

  method D1() {
    var ch := new Ch;
    var c := new ImplicitC;
    send ch(c.k - 15, c);  // give ourselves some credit
    receive a, a := ch;  // error: a occurs twice
    assert a < b.k;
  }
}

channel Ch(x: int, y: ImplicitC) where acc(y.k) && x < y.k;