// Purpose: tests axioms about primed variables are not allowed.
// Description: A module with an axiom saying that x primed is always greater than zero. An init block that sets x to 1 and a next block that decrements x. Bounded model checking for 5 steps.
// Expectation: UCLID5 should say that primed variables are not allowed in axioms
// Validation: Removing this check should make the verification pass.

module main {
    var x: integer;

    axiom x' > 0;

    init {
        x = 1;
    }

    next {
        x' = x - 1;
    }

    invariant falsifiable: x > 0;

    control {
        bmc(5);
        check;
        print_results();
    }
}
