class Cell {
  var n : int;
}

class A {
  var x : int;

  predicate valid { 
    acc(x) && x >= 0 
  }

  function getX(): int requires valid 
  { 
    unfolding valid in x 
  }

  method init()
    requires acc(this.*);
    ensures valid;
  {
    x := 0;
    fold valid;
  }

  method inc()
    requires valid;
    ensures valid && getX() == old(getX()) + 1;
  {
    unfold valid;
    x := x + 1;
    fold valid;
  } 

  method dec()
    requires valid && getX() > 0;
    ensures valid;
  {    
    unfold valid;
    x := x - 1;
    fold valid;
  }

  method magic() returns (c: Cell) 
    requires valid;
    ensures valid;
  {
  }
}

class C {
  ghost var x : int;
  var y : Cell;
  var z : Cell;
  
  function getX() : int
    requires valid;
  { 
    unfolding valid in y.n - z.n 
  }

  predicate valid {
    acc(x) && acc(y) && acc(z) && acc(y.n) && acc(z.n) &&
    y != null && z != null && 
    y.n >= 0 && z.n >= 0 &&
    y.n - z.n == x &&
    x >= 0
  }
  
  method init()
    requires acc(this.*);
    ensures valid;
  {
    x := 0;
    //
    y := new Cell;
    z := new Cell;
    y.n := 0;
    z.n := 0;    
    fold valid;
  }

  method inc() 
    requires valid;
    ensures valid && getX() == old(getX()) + 1;
  {
    unfold valid;
    x := x + 1;
    //
    y.n := y.n + 1; 
    fold valid;
  }

  method dec()
    requires valid && getX() > 0;
    ensures valid;
  {
    unfold valid;
    x := x - 1;
    //
    z.n := z.n + 1;
    fold valid;
  }

  method magic() returns (c: Cell)
    requires valid;
    ensures valid;
  {
    unfold valid;
    c := y;
    fold valid;
  }
}

class Client {
  method main() 
  {
    // Abstract program
    var a := new A;    
    call a.init();
    call a.inc(); // problem is here
    call a.inc();
    call a.dec();
    call ac := a.magic();
    ac.n := 0; 
  
    // Concrete program
    var c := new C;
    call c.init();
    call c.inc();
    call c.inc();
    call c.dec();
    call cc := c.magic();
    cc.n := 0; 
  }
}