Formally check custom Solidity assertions

[leonardoalt]

This PR contains my initial code to verify any Solidity assertion. Currently assert is represented by the opcode 0xfe, which might change in the next compiler's version. What this code does is consider 0xfe as ASSERTFAIL, and whenever a path hits this instruction this means an assertion fails.
I do hope assert gets its own opcode (as require has 0xfd) because there are cases where
0xfe is used (as INVALID) without being connected to any assertion (as a generic INVALID).

I did rule out some of those cases that would lead to false positives (INVALIDs that are not assertion failures), but there might be others, so do not consider this code error-free and final. In order to keep Oyente's functionalities the way they are, the assertion checks are considered only if the option -a is used.

If the assertion is indeed not true, the model given by z3 is printed. In the future I hope to somehow trace the model back to Solidity variables.

[CLAassistant]

All committers have signed the CLA.

[loiluu]

This is awesome. Thanks a lot @leonardoalt . @inian and @luongnt95 please check this PR and merge.