// Description: One module. The module has two integer state variables. We initialize both to be equal, and then increment both in the next block. Check that the variables are equal using inline assertions after each line in the next block.

module main
{
  var x : integer;
  var y : integer;

  init {
    x=0;
    y=0;
  }
  next {
    x'=x+1;
    assert(x==y);
    y'=y+1;
    assert(x==y);

  }

  control {
    vobj = bmc(5);
    check;
    print_results;
  }
}
