// Purpose: check that multiple next blocks are allowed and handled correctly
// Description: a module with a single variable x, and two next blocks. The first next block does nothing. The second next block increments x. A check by induction that x is always 1.
// Expectation: The invariant x == 1 should not hold. The check should fail.
// Validation: adding a bug to UCLID5 in which only the first next block for each module is used, would cause this verification to pass.


module main {
    var x: integer;

    init {
        x = 1;
    }

    next{}

    next {
        x' = x + 1;
    }

    invariant x_eq_y: x == 1;

    control {
        v = induction;
        check;
        print_results;
    }
}
