// Purpose: check that assuming false in a procedure that is not called does not affect the verification result
// Description: A module with a single procedure that assumes false. A trivially false invariant and a bmc check.
// Expectation: All checks should fail
// Validation: Inserting a bug into how procedure assume statements are handled should cause this verification to pass.

module main {
    procedure p() {
        assume false;
    }

    invariant trivial: false;

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