// Description: a module with a local variable x, and a next state relation that declares a local variable x and then assigns to x prime. Finally, a trivially false invariant and a check by induction.

module main {
    var x : integer;

    next {
        var x : integer;
       x' = x;
    }

    invariant trivially_false : false;

    control {
        induction;
        check;
        print_results;
    }
}
