// Purpose: tests that functions cant refer to primed variables
// Description: A module with a single variable, a function that returns the value of that variable but primed, a transition relation that increments the variable by 1, an invariant that says that the function is always one greater than the variable, and a bmc check.
// Expectation: UCLID5 should return an error saying that primed variables cannot be used in functions
// Validation: Removing the check in UCLID5 should cause the verification to pass.

module main {
    var x: integer;

    next {
        x' = x + 1;
    }

    define f(): integer = x';

    invariant future: x == f() - 1;

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