Separate Errors for Integer Under- and Overflows

[Patrick-6]

Currently, all three of the following functions fail verification with the same message:

use prusti_contracts::*;

fn underflow(x: i32) -> i32 {
    x + (-1)
}

fn overflow(x: i32) -> i32 {
    x + 1
}

fn both(x: i32, y: i32) -> i32 {
    x + y
}

Error message:

[Prusti: verification error] assertion might fail with "attempt to add with overflow"

It would be useful to have a way to distinguish between (integer) over- and underflows (for example with a feature flag).

When combined with extra_verifier_args = ["--numberOfErrorsToReport=0"] (after #1213), it could provide more helpful error messages to the user.