SMTChecker: Bring back assertions in "external_calls" SMTChecker tests

[blishko]

Several assertions were commented out because of nondeterminism we observed in Spacer, which made these tests brittle. Spacer can now solve some of them, others we can now solve with Eldarica.

In order to run Eldarica, we need to set up CompilerStack in SMTCheckerTest with SMT callback.

Note that running Eldarica seems to come with significant overhead, because it starts a new Eldarica process (which starts new JVM) for every query.

[blishko]

Should this have a changelog entry?

The only visible change from the outside is the need for the users to have Eldarica installed if all smt tests should pass. Should we document that?

[nikola-matic]

Should this have a changelog entry?

The only visible change from the outside is the need for the users to have Eldarica installed if all smt tests should pass. Should we document that?

If there's a visible change, I'd say yes.

[blishko]

OK, I'll add a changelog entry.

[blishko]

I am converting back to draft, until we decide if we are really going to require Eldarica, or give user the option to either manually or automatically to skip tests with Eldarica if they do not have it set up.

[cameel]

I am converting back to draft, until we decide if we are really going to require Eldarica, or give user the option to either manually or automatically to skip tests with Eldarica if they do not have it set up.

I think it would be fine to merge the PR without it. Let's just make sure that we also add a flag for Eldarica before the next release.

[blishko]

@nikola-matic , @cameel , I removed the changelog entry and updated the docs to mention Eldarica.

[blishko]

@cameel, the EVMVersion parameter update I'll do in a separate PR. It looks like it changes messages in quite a number of tests. The other comments have been addressed.