// Description: One module. The module has an integer state variable, x. The init block makes a series of sequential assignments to x, using inline assertions to check that each assignment happened. If the assignments happen in sequence, the assertions should pass.

module main
{
  var x : integer;

  init {
    x=0;
    assert(x==0);
    x=1;
    assert(x==1);
    x=2;
    assume(x==2);
  }
  next {

  }

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