Unimplemented: Inhale the predicate rooted at dst_field about prusti-dev HOT 4 CLOSED

error: [Prusti: unsupported feature] the encoding of this reference copy has not been implemented
  --> tmp/program.rs:34:16
   |
34 |     set.remove(&3);
   |                ^^

error: [Prusti internal error] generating fold-unfold Viper statements failed (FailedToObtain(Pred(Local(_2: Ref(__TYPARAM__$T$__), Position { line: 18, column: 15, id: 168 }), read)))
  --> tmp/program.rs:19:5
   |
19 | /     pub fn insert(&mut self, value: T) {
20 | |         self.set.insert(value);
21 | |     }
   | |_____^

error: [Prusti: verification error] postcondition might not hold.
  --> tmp/program.rs:23:15
   |
23 |     #[ensures(!self.contains(&value))]
   |               ^^^^^^^^^^^^^^^^^^^^^^
   |
note: the error originates here
  --> tmp/program.rs:24:5
   |
24 | /     pub fn remove(&mut self, value: &T) -> bool {
25 | |         self.set.remove(value)
26 | |     }
   | |_____^