// This file is meant as a test for Chalice's smoke testing feature (command line switch -smoke)
class Cell {
  var f: int;
  
  invariant acc(this.f) && f == 1
  invariant f == 2 // SMOKE: contradiction
  
  method a1()
    requires false // SMOKE: precondition is false
  {}
  
  method a2()
    requires acc(this.f,-2) // SMOKE: precondition is equivalent to false
  {}
  
  method a3()
    requires acc(this.f)
  {
    if (this.f > 0) {
      this.f := 0;
    }
  }
  
  method a4()
    requires acc(this.f)
  {
    if (false) {
      this.f := 0; // SMOKE: unreachable
    }
  }
  
  method a5()
    requires acc(this.f)
  {
    if (true) {
      this.f := 0;
    }
  }
  
  method a6()
    requires acc(this.f)
  {
    if (false) {
      this.f := 0; // SMOKE: unreachable
    } else {
      this.f := 1;
    }
  }
  
  method a7(i: int, j: int)
    requires i != j;
  {
    assume i == j; // SMOKE: introduces contradiction
  }
  
  method a8()
    requires acc(this.f)
  {
    while (true)
      invariant acc(this.f)
    {
      this.f := this.f + 1
    }
    // SMOKE: unreachable, loop does not terminate
  }
  
  method a9()
    requires acc(this.f)
  {
    call a8()
  }
  
  method a10()
    requires acc(this.f)
  {
    if (true) {
      this.f := 0;
    } else {
      this.f := 1; // SMOKE: unreachable
    }
  }
  
  function f1(): int
    requires false // SMOKE: precondition is false
  { 1 }
  
  method a11()
  {
    var i: int := 0
    if (false) {
      // SMOKE: unreachable
    } else {
      if (true) { assume false } // SMOKE: introduces contradiction
      else { assume i == 1 } // SMOKE: introduces contradiction
    }
  }
  
  method a12()
  {
    assume false // SMOKE: introduces contradiction
    while (false) {
    
    }
  }
  
  method a13()
    ensures false // ERROR: cannot prove false
  {
  }
  
  method a14()
  {
    call a13(); // SMOKE: statements afterwards not reachable anymore
  }
  
  predicate valid {
    1 == 2 // SMOKE: contradiction
  }
}

channel C(msg: bool) where msg && !msg // SMOKE: contradiction