// Purpose: check that mutually recursive functions are not allowed
// Description: an empty module with two mutually recursive functions
// Expectation: There should be a compilation error saying that mutually recursive functions are not allowed
// Validation: removing the recursive function check should result in an error on the solver side

module main {
    define f(x: integer): integer =
        if (x <= 0) then 0 else g(x - 1) + 1;

    define g(x: integer): integer =
        if (x <= 0) then 0 else f(x - 1) + 1;

    invariant base_case: f(0) == 0;

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