The predicate in adequacy is currently only able to talk about the return value of the main thread. After this change, it is also able to talk about the final state.
We make use of this in https://iris-project.org/pdfs/2018-iron.pdf (which is build on top of normal Iris weakest preconditions) to ensure via adequacy that all memory has been freed.