Type limits for unsigned integer missing when using check_overflows = false

[Patrick-6]

#[requires(0 <= i)] generates a warning: [unused_comparisons] comparison is useless due to type limits., but removing it with check_overflows = false will cause the verification to fail:
[Prusti internal error] Prusti encountered an unexpected internal error
Details: unregistered verification error: [application.precondition:assertion.false; 0] Precondition of function lookup_pure__$TY$__Slice$i64$i64$Slice$i64$$int$$$int$ might not hold. Assertion 0 <= _3 might not hold. (@0.0).

Additionally, the error appears on line 1 column 1 in the lib.rs file, not in the file where the error happened.

use prusti_contracts::*;

// #[requires(0 <= i)]
#[requires(i < s.len())]
fn test(s: &[i64], i: usize) -> i64 {
    s[i]
}

[fpoli]

The [unused_comparisons] warning is wrong and should be suppressed in the macro expansion of prusti_contracts::requires.

The [Prusti internal error] is a bug in the backtranslation of verification errors. Either the expected error should be something like [Prusti verification error] Index of array access might be negative, or we should assume the type bounds of usize so that no error is reported. (Prusti was doing the latter at some point in the past, but we apparently lost that feature in a refactoring.)

[Patrick-6]

This might also be related to the backtranslation of verification errors:

#[ensures(s[s.len()] == 5)]
fn test_1(s: &[i64]) {}

This results in [Prusti: verification error] postcondition might not hold. on s[s.len()].
If you put the same code in the body of a function you get the correct error message:

fn test_2(s: &[i64]) -> i64 {
    s[s.len()]
}

[Prusti: verification error] the array or slice index may be out of bounds.

[Patrick-6]

I don't think this issue is completely resolved, if a user sets encode_unsigned_num_constraint = false, they will still get the unregistered verification error from the example code, or the unused comparisons warning after manually adding 0 <= i.