// Description: A module with a single variable, intializing variable to 1, a transition relation that increments the variable by 1, an invariant that says that the variable is always one greater than 3, and a bmc check.

module main {
    var x: integer;

    init {
        x = 1
    }
    next {
        x' = x + 1;
    }

    invariant future: x < 3;

    control {
        bmc(2);
        check;
        print_results;
    }
}
