// 4 errors expected

class C {
  method M(x: int) returns (y: bool)
    requires 0 <= x;
    ensures y <==> x == 10;
  {
    y := true;
    if (x != 10) { y := !y; }
  }

  method Caller0()
  {
    var b: bool;
    call b := M(12);
    assert !b;
    call b := M(10);
    assert b;
  }
  method Caller1()
  {
    var b: bool;
    call b := M(11);
    assert b; // error (258)
  }

  var F: int;

  method P(n: int)
    requires acc(F);
    ensures F == old(F) + n;  // error
  {
    F := F + n;
  }
  method Caller2()
    requires acc(F);
  {
    var prev := F;
    call P(2);
    assert false; // succeeds because postcondition of P is not well-defined (i.e. we do not havoc this.F, so the verifier assumes the value is the same in pre and post) 
  }

  method Q(n: int)
    requires acc(F);
    ensures acc(F) && F == old(F) + n;
  {
    F := F + n;
  }
  method Caller3()
    requires acc(F);
    ensures acc(F);
  {
    var prev := F;
    call Q(2);
    assert F == prev + 2;
  }
}

class Consts {
  method M0() returns (z: int)
    ensures z == 5
  {
    const a := 5
    z := a
  }
  method M1() {
    ghost const a
    a := 5
  }
  method M2() {
    ghost const a
    a := 5
    a := 5  // error (569)
  }
  method M3(b: bool) {
    ghost const a
    if (b) { a := 5 }
    assert a < 10  // error (611)
  }
  method M4(b: bool) {
    ghost const a
    if (b) { a := 5 }
    ghost var x := a
    if (!b) { a := 7 }
    assert a < 10
    assert b ==> x == 5  // cool, huh?
  }
  method M5(b: bool) {
    ghost const a
    if (b) { a := 5 }
    assert assigned(a) ==> a == 5
  }
}