// Description: a module with a state var, and a local var declared in the next block, both with the same name. In the next block, the state var is updated to be equal to the local var, and an invariant that fails.

module main {
    var x : integer;
    init {
    }

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

    invariant trivially_false : false;

    control {
        induction;
        check;
        print_results;
    }
}
