// Purpose: tests that unsat axioms do affect the inductive step of a proof by induction.
// Description: A module with an axiom false, 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.
// Expectation: The base case and the inductive step should pass.
// Validation: making axioms be local would cause the inductive step to pass.

module main {
    var x: boolean;

    axiom false;

    next {
        havoc x;
    }

    invariant falsifiable: x;

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