Symex: clean up quantifier rewriting

[smowton]

1. Don't use the sharing-breaking rewrite_quantifiers routine unless there is a forall-quantifier
   in the expression.
2. Comment to explain why we look for existential quantifiers, even though the rewrite routine
   doesn't actually directly handle them.

[tautschnig]

Hmm, there is #3925, which invalidates some of what is being done here. I don't mind rebasing #3925 on top of this one, but it would amount to a revert of sorts.

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: 495ac02).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102857597

[smowton]

@tautschnig reverted the move and rename accordingly; kept sparing sharing when the simplify does not introduce a forall-expr, which will still apply even after #3925.

[tautschnig]

Hmm, I quite liked the text move actually, although it will cause some conflicts that I'll need to resolve. And this still needs a rebase.

[allredj]

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 9891174).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103044562
Status will be re-evaluated on next push.
Common spurious failures:

• the cbmc commit has disappeared in the mean time (e.g. in a force-push)

• the author is not in the list of contributors (e.g. first-time contributors).

• the compatibility was already broken by an earlier merge.