Move prover returns: exiting with verification errors
error: global memory invariant does not hold
   ┌─ tests/sources/functional/disable_inv_friends.move:25:10
   │
25 │          invariant [global, suspendable] forall addr: address: exists<M3::R3>(addr) <==> exists<M2::R2>(addr);
   │          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   │
   =     at tests/sources/functional/disable_inv_friends.move:85: f5_incorrect
   =     at tests/sources/functional/disable_inv_friends.move:91: f5_incorrect (spec)
   =     at tests/sources/functional/disable_inv_friends.move:92: f5_incorrect (spec)
   =     at tests/sources/functional/disable_inv_friends.move:85: f5_incorrect
   =         s = <redacted>
   =     at tests/sources/functional/disable_inv_friends.move:86: f5_incorrect
   =     at tests/sources/functional/disable_inv_friends.move:55: f3
   =         s = <redacted>
   =     at tests/sources/functional/disable_inv_friends.move:56: f3
   =     at tests/sources/functional/disable_inv_friends.move:57: f3
   =     at tests/sources/functional/disable_inv_friends.move:25