Add vacuity test for contradictory requires clause

[celinval]

Requested feature: Contract verification should fail if the requires clause can never be satisfied
Use case: Detect user mistakes when writing contracts
Link to relevant documentation (Rust reference, Nomicon, RFC):

Test case:

#[kani::requires(a > 5)]
#[kani::requires(a < 4)]
#[kani::ensures(result == a)]
fn buggy(a: u32) -> u32 {
    panic!("This code is never tested")
}

Without vacuity test, this contract verification will pass.

[celinval]

Thank you for the suggestion @camshaft

[JustusAdam]

I'm impressed with how fast people are picking up contracts.