Proper SMT CHC tests

[leonardoalt]

Depends on https://github.com/ethereum/solidity/pull/11421

This PR adds proper SMTChecker tests. Currently, the SMTChecker tests are actually broken, many tests are ignored, and the smtlib version of the SMTCheckre encoding is not being tests at all.

The main smtCheckerTests in this code are mainly used by the Solidity t_ems_solcjs job, which copies the smtCheckerTests into the solc-js tests and runs test/smtcallback.js from this repo. It now requires soljson version >=0.7.2 because of the warning format.

If soljson < 0.8.5, it runs the static z3 inside soljson and compares that to the test expectation. Else, it runs /\ plus a local z3 binary using Solidity's smtlib2 encoding, and compares all of them. The comparison now is much more precise than before: it compares each output location, which represents a property.

Note that safe properties are not reported, so if one solver reports a location and another doesn't, there's an inconsistency. The exception to this is when this inconsistency happens for the BMC engine, where one solver probably solved it safe with CHC, and another solver couldn't prove it safe with CHC, and reports an unsafe false positive via BMC.

The test only fails if there's a real inconsistency, as opposed to the stronger soltest. I think that's fair since the JS/smtlib2 environment might give more nondeterministic answers compared to the embedded C++ z3.

[coveralls]

Coverage decreased (-5.6%) to 80.252% when pulling 91068be5f91d4d7c9f0f1a02e82466fe90b6201a on smt_proper_tests into 1a457d500d2020c103feda2c46a401c5c6bd6c16 on master.

[leonardoalt]

I really don't understand this coverage tool.

[cameel]

@leonardoalt Is this still work in progress or is it just waiting to be reviewed?

[leonardoalt]

Waiting to be reviewed

[axic]

I suppose #565 needs to be merged first?

[leonardoalt]

Ah yes, this branch is all over the place. Will need to rethink it after the other one gets merged

[leonardoalt]

Closing cus need to rewrite it anyway.