Predicate overflow not reported correctly

[jthomme1]

The following program fails to verify:

use prusti_contracts::*;

predicate!{fn magic(i: i64) -> i64 {
   i+1
}}

#[ensures(magic(1) == 2)]
fn main() {
}

with the following error message:

error: [Prusti: verification error] postcondition might not hold.
 --> path_to_file.rs:7:11
  |
7 | #[ensures(magic(1) == 2)]
  |           ^^^^^^^^^^^^^
  |
note: the error originates here
 --> path_to_file.rs:8:1
  |
8 | / fn main() {
9 | | }
  | |_^

Verification failed
error: aborting due to previous error

Changing the predicate to a pure function, gives a more precise error message:

use prusti_contracts::*;

#[pure]
fn magic(i: i64) -> i64 {
   i+1
}

#[ensures(magic(1) == 2)]
fn main() {
}

error: [Prusti: verification error] assertion might fail with "attempt to add with overflow"
 --> path_to_file.rs:5:4
  |
5 |    i+1
  |    ^^^

error: [Prusti: verification error] postcondition might not hold.
  --> path_to_file.rs:8:11
   |
8  | #[ensures(magic(1) == 2)]
   |           ^^^^^^^^^^^^^
   |
note: the error originates here
  --> path_to_file.rs:9:1
   |
9  | / fn main() {
10 | | }
   | |_^

Verification failed
error: aborting due to 2 previous errors

The error message for the version using a predicate should also indicate the overflow.