Forgive me if this is naive: I was trying out aeneas on some rust code, and hit internal errors. I've managed to minimize the example to the following:

pub fn get<T>(v: &Vec<Option<T>>, i: u32) -> Option<&T> {
    if i == u32::MAX {
        return None;
    }
    let i_usize = usize::try_from(i).ok()?;
    v.get(i_usize)?.as_ref()
}

This results in:

Error] Internal error, please file an issue Source: '/rustc/library/core/src/option.rs', lines 2546:4-2546:64