Properties of HashMap wrapper structs specified in predicate fails to get verified

[nokunish]

There seems to be some issues with verifying properties of wrapper structs for HashMap, specifically when a predicate is used as a restriction. For instance, when we impose wrapper_predicate(..)

struct MapWrapper 
{
    map: HashMap<usize, usize>
}

predicate! {
    fn wrapper_predicate(w: &MapWrapper) -> bool
    {
        forall( |u: &usize| w.map.contains_key(u) ==> 0 < *u ) 
    }}

the assertion fails unless the second pre-condition is provided.

#[requires(wrapper_predicate(w))]
/* #[requires(forall( |u: &usize| w.map.contains_key(u) ==> 0 < *u ))] */

fn test_map_wrapper(w: &MapWrapper, u: &usize)
{
    prusti_assert!(w.map.contains_key(u) ==> 0 < *u );
}

The same issue does not occur when we don't use wrapper structs, i.e.,

predicate! {
    fn map_predicate(map: &HashMap<usize, usize>) -> bool
    {
        forall( |u: &usize| map.contains_key(u) ==> 0 < *u )
    }}

#[requires(map_predicate(hm))]
fn test_map(hm: &HashMap<usize, usize>, u: &usize)
{
    prusti_assert!(hm.contains_key(u) ==> 0 < *u );
}

the assertion passes with no error in this example.