When doing equivalence checking, CALL to unknown code can be approximated in a different way

As @charles-cooper mentioned on the chat, for equivalence checking -- and only for equivalence checking -- one can do a different kind of overapproximation for call to unknown code via `CALL`. If codeA and codeB both call contract C with the _same prestate and same calldata_ then and only then, the post-state after the call can be assumed to be symbolic, _but_ equivalent. Which obviously does not work for regular symbolic execution, which e.g. the #658 does allow us to perform. However, this kind of `CALL` does not necessitate `--promise-no-reent`, i.e. the system may actually be non-reentrant.

NOTE: It may be important to think though things related to this. When code-A has a function "mess_me_up()" and code-B does not have that function, then even though the two codes have the same prestate and the same calldata, the end state may be different -- in one case, a malicious contract could have called `mess_me_up()`, while in the other, it could not. However, the `mess_me_up()` public will be detected as a difference anyway...

Read this proposal alongside issue #658 and trace the existing equivalence-checking treatment of CALL. Clarify the same-prestate and same-calldata rule, the non-reentrancy caveat, and the missing-public-function case; completion should include agreed behavior and tests for these cases.

Written by the indexing model from the issue text.