// Description: A simple module with 1 variable. The variable is initialised to 0. The next block havocs the variable, and then uses an inline assertion to check that the variable is still equal to 0. We use bounded model checking with an unrolling of 1 to check that this assertion passes on the first unrolling.

module main
{
    var i : integer;

    init {
        i = 0;
    }

    next {
        havoc i;
        assert (i == 0);
    }

    control {
        // print_module;
        v = unroll(1);
        check;
        print_results;
    }
}
