[move-prover][interpreter] two bug fixes to re-enable disabled tests

[meng-xu-cs]

The first commit fixes two bugs to re-enable the failing test:

• collect pointers for write-backs even when the local slot is destroyed
• fix the indexing of the borrow edge in the write-back process.

The second commit picks the baseline version for callee with ghost type params

• This is a temporary solution until we have a better way to multiplex the spec evaluation against multiple universially quantified types.

Motivation

As title

Have you read the Contributing Guidelines on pull requests?

Yes

Test Plan

CI, with the re-enabled test.