// Description: A module with an assume false in the init, a transition relation that havocs a variable, and a property that is false in the inductive step. Also a call to induction in the control block.

module main {
    var x: boolean;

    init {
        assume false;
    }

    next {
        havoc x;
    }

    invariant falsifiable: x;

    control {
        induction;
        check;
        print_results();
    }
}
