Issues with verifying the result is None about prusti-dev HOT 4 OPEN

#[pure]
    pub fn is_none(&self) -> bool;

#[pure]
    #[ensures(u <= 10 ==> result.is_none())]                   // this fails 
    pub fn filter(&self, u: u32) -> Option<u32> {
        if u > 10 {
            return Some(u)
    }  
        return None
    }

domain Snap$m_std$$option$$Option$_beg_$u32$_end_  {
  
  function discriminant$__$TY$__Snap$m_std$$option$$Option$_beg_$u32$_end_$Snap$m_std$$option$$Option$_beg_$u32$_end_$$int$(self: Snap$m_std$$option$$Option$_beg_$u32$_end_): Int 
  
  function cons$0$__$TY$__Snap$m_std$$option$$Option$_beg_$u32$_end_$Snap$m_std$$option$$Option$_beg_$u32$_end_(): Snap$m_std$$option$$Option$_beg_$u32$_end_ 
  
  axiom Snap$m_std$$option$$Option$_beg_$u32$_end_$1$injectivity {
    (forall _l_0: Int, _r_0: Int ::
      { cons$1$__$TY$__Snap$m_std$$option$$Option$_beg_$u32$_end_$$int$$Snap$m_std$$option$$Option$_beg_$u32$_end_(_l_0),
      cons$1$__$TY$__Snap$m_std$$option$$Option$_beg_$u32$_end_$$int$$Snap$m_std$$option$$Option$_beg_$u32$_end_(_r_0) }
      cons$1$__$TY$__Snap$m_std$$option$$Option$_beg_$u32$_end_$$int$$Snap$m_std$$option$$Option$_beg_$u32$_end_(_l_0) ==
      cons$1$__$TY$__Snap$m_std$$option$$Option$_beg_$u32$_end_$$int$$Snap$m_std$$option$$Option$_beg_$u32$_end_(_r_0) ==>
      _l_0 == _r_0)
  }
}

    #[pure]
    pub fn some_obj(&self) -> Option<usize> {
        Some(10)
    }

    #[pure]                                                     // does not affect results
    #[ensures(result <==> self.some_obj().is_some())]      
    pub fn is_true(&self) -> bool {
        let _: Option<usize> = None;                           
        true
    }

    #[pure]
    pub fn some_obj(&self) -> Option<usize> {
        let obj: Option<usize> = Some(10);
        obj
    }