Strange handling of calling an impure function from a predicate

[dewert99]

The following code verifies successfully even though it calls an impure function from a predicate:

use prusti_contracts::*;


fn impure() -> u32 {
    5
}

predicate! {
    fn pred(x: u32) -> bool {
        x == impure()
    }
}

Adding:

#[requires(pred(x))]
fn test(x: u32)  {}

causes it to fail with two errors:

error: [Prusti: invalid specification] use of impure function "broken1::impure" in pure code is not allowed                                                                            
  --> src\broken1.rs:12:14
   |
12 |         x == impure()
   |              ^^^^^^^^

error: [Prusti: verification error] precondition of pure function call might not hold.                                                                                                 
  --> src\broken1.rs:16:12
   |
16 | #[requires(pred(x))]
   |            ^^^^^^^

The first one makes sense but probably should happen even if the predicate is not used. The second one seems strange since pred doesn't have a precondition.

Also making impure pure causes everything to verify so this is more an issue about error reporting than anything else