// Description: A module with a single variable that starts at 10 and decrements. The invariant is that the variable is always positive. We unroll for 21 steps.

module main {
    var y: integer;

    init {
        y = 10;
    }

    next {
        y' = y - 1;
    }

    invariant always_positive: y >= 0;

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