// Description: One module. The module has a boolean state variable, x, which is initialised as false in the init block, after which there is an assume(false). The module has an invariant that checks that x is globally true, and is checked with bmc.

module main
{
  var x : boolean;

  init {
    x=false;
    assume(false);
  }
  next {
    x'=false;

  }

  property p1: x;

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