Slightly more complete more complete exhale

[marcoeilers]

MCE introduces a fresh symbol for the result of a lookup or the snapshot returned by a consume. Sometimes, this causes trouble if the definition of the fresh symbol is, for example, hidden inside a quantifier, and thus the definition is needed to get the quantifier instantiation that contains the definition.

The MCE code (in summarise) already checks if it can syntactically find a chunk that definitely aliases the receiver we're looking for, and in that case, does not introduce a new symbol, but instead returns and additionally constrains the value of that chunk.

Additionally, when consuming, MCE already uses the greedy algorithm (including SMT checks if needed) to check for known aliases. However, if one is found here, it is not used by the summarisation code mentioned above.

This PR makes two changes:

• summarise gets an additional parameter; if a client has already used the solver to check for known aliases, it can pass along the result here.
• summarise uses the passed symbol instead of the fresh one in case one is passed.
• If clients of summarise indicate that they have not used the solver to check for an alias before calling it, and summarise cannot find an alias syntactically using the existing check, then summarise itself will use the solver to check for a definite alias, and use its value if one is found.

So an additional prover query is performed only for lookups (not for consumes, which already used the solver) without syntactic aliases, and only if no value is found in the cache.

This fixes an MCE incompleteness that @JonasAlaif mentioned in #387, and also fixes the last remaining MCE incompleteness mentioned in #557 (quantifiedpermissions/sequences/mergesort.vpr).

[mschwerhoff]

LGTM