// Description: a module with a variable named __ucld_1_block_rename. The variable starts at 0 and increments by 1 each step. We check a simple invariant that it is always >= 0.

module main {
    var __ucld_1_block_rename: integer;

    init {
        __ucld_1_block_rename = 0;
    }

    next {
        __ucld_1_block_rename' = __ucld_1_block_rename + 1;
    }

    invariant should_hold: __ucld_1_block_rename >= 0;

    control {
        induction;
        check;
        print_results;
    }
}
