Revert 'Eliminate top level existentials in side-condtions'

[goodlyrottenapple]

This PR fixes #3605
The bug was introduced by #3202, which eliminated top level existentials in side-conditions. However, this was incorrect because when translated to Z3, these variables would get a universal quantification, which is what was happening in #3605

[goodlyrottenapple]

this didn't end up being the issue, but it's not correct and should be changed nonetheless.

[jberthold]

LGTM, but the RPC integration tests need to be adapted.

[jberthold]

As it turns out, one of the RPC server implies tests is using a term that hits an error call now.
We probably just want to use a different test but it would be interesting to understand the restriction in detail.

[goodlyrottenapple]

As it turns out, one of the RPC server implies tests is using a term that hits an error call now. We probably just want to use a different test but it would be interesting to understand the restriction in detail.

Does the test make sense in the first place? X and Z are not booleans but rather of sort K, so the back-end infers that Z is the term and #Not (X #Equals Z) is the predicate, hence the error.

[jberthold]

As it turns out, one of the RPC server implies tests is using a term that hits an error call now. We probably just want to use a different test but it would be interesting to understand the restriction in detail.

Does the test make sense in the first place? X and Z are not booleans but rather of sort K, so the back-end infers that Z is the term and #Not (X #Equals Z) is the predicate, hence the error.

Yes, that's what happens. Just not sure why it would be such a bad thing to have an existential quantification over both term and predicate...
But I was meaning to suggest that we modify the test and move on.

Foundry proofs showed problems

[jberthold]

Unfortunately, the "error somewhere else" is triggered by foundry proofs (I tested GasTest.testInfiniteGas which introduces an existential gas value).
bug-report-stripped.tar.gz is an RPC interaction log for this proof, failing in request 6.
EDIT: actually any proof in tests/foundry is failing, on the initial implies request. The consequent of that request contains an array of existentials that quantify free variables in the target state.