Patricio Inzaghi

I tried the [last nightly release](https://github.com/viperproject/prusti-dev/releases/tag/v-2022-03-15-2318) without luck. What I am doing is unzipping the binaries for Ubuntu, giving execution permissions to all binaries and executing: `./prusti-rustc --edition=2021 list.rs` The...

Exactly, I have two errors. If I consider the whole example, I have even more errors (5 to be exact). Thanks for confirming this. ``` #![feature(box_patterns)] use prusti_contracts::*; use std::mem;...

@fpoli should it be harmful to use the `check_overflows=false` flag? I am not interested in checking overflows for now. I see that the postconditions are still checked and the code...

It's a little difficult for me to slice a minimal example because they are several things working together, this is the repo with the problem: https://github.com/pinzaghi/rusty-raft It only has 2...

I tried to obtain a minimal example: ``` #![feature(allocator_api)] use std::hash::Hash; use std::hash::BuildHasher; use std::collections::{HashSet, HashMap}; use std::borrow::Borrow; use core::alloc::Allocator; use fxhash::{FxHashSet, FxHashMap, FxHasher}; use prusti_contracts::*; #[extern_spec] impl HashMap {...

Thanks for your feedback. I updated the code like this: ``` #![feature(allocator_api)] use std::hash::Hash; use std::hash::BuildHasher; use std::collections::{HashSet, HashMap}; use std::borrow::Borrow; use core::alloc::Allocator; use fxhash::{FxHashSet, FxHashMap, FxHasher}; use prusti_contracts::*; #[extern_spec]...

Following up with this @Aurel300, I don't want to bother, but maybe this last error is something simple for you to see. Thanks again.