// Description: A module with a single bitvector variable x. The variable x increases by 1 in each transition. There is an invariant saying that x is never 0 and we are attempting a proof by induction.

module main {
    var x: bv32;

    next {
        x' = x + 1bv32;
    }

    invariant never_zero: x != 0bv32;

    control {
        v = induction;
        check;
        v.print_cex();
    }
}
