prusti-dev
prusti-dev copied to clipboard
Unexpected internal error using HashMap.get()
I'm having the following error
error: [Prusti internal error] Prusti encountered an unexpected internal error
--> /src/test.rs:8:13
|
8 | let a = h.get(i).unwrap()-1;
| ^^^^^^^^
|
with this code:
#![feature(box_patterns)]
use prusti_contracts::*;
use std::collections::HashMap;
#[ensures(true)]
fn test(h: HashMap<u64, u64>, i: &u64) {
let a = h.get(i).unwrap();
}
fn main(){}
and this version (I also tried the latest nightly build):
Prusti version: commit 164fa35 2022-03-15 20:32:24 UTC, built on 2022-03-15 21:59:32 UTC rustc 1.61.0-nightly (285fa7ecd 2022-03-14)
Reference-typed fields are not yet supported (get returns Option<&u64>).