This PR brings a good number of important changes to the symbolic execution code:

• It removes the concolic execution: this code should be moved to hevm directly, since it is too hard to maintain from our side, and we don´t know exactly when it is useful.
• It adds a new type of test result: unsolvable. This new value is used to signal that a symbolic exploration finished to review all possible states without any counter example to trigger an assertion failure.
• It improves the full symbolic execution of a single transaction, as this seems to be the best approach to explore the code using symbolic execution, some notable changes:
  • A corpus is shuffled before selecting a sequence for the symbolic exploration
  • Bitwulza is the new default smt solver, but other solvers can be selected
  • Support for handling symbolic block.number and block.timestamp
  • Support for avoiding doing symbolic exploration for useless (e.g. no arguments) or unsupported inputs (e.g. dynamic arguments)
  • Two modes for using symbolic execution: verification mode (stateless) and exploration (fuzzing+sym-exec)
  • Two strategies are used for introducing symbolic transactions in the exploration mode: (1) a random transaction is inserted at a random position and (2) the last transaction of a sequence is symbolized.
  • Support for RPC query when doing symbolic exploration (including cache that will be queried but not updated)
  • Added some more tests for symbolic execution (verification mode)
  • The symbolic execution mode is moved into its own directory

Some unrelated changes included in this PR:

• Removed etheno related code (obsolete)
• Removed tests related with gas usage (covered by hevm per opcode) and self-destruction (no longer relevant in the current fork)
• Removed usage of very old solc version in the tests

Known issues:

• UI needs to be adapted in verification mode since the symbolic worker is busy and it can block the refresh of the UI. Text mode is advised.
• There is a detection to some cases where hevm produces a counter example, but it is not reproduced correctly. This is a bug that will be eventually solved upstream, but if we manage to detect a counter example that does not increase coverage (e.g. reached an assertion), echidna will trigger a failure so it can be reported upstream. This detection is not perfect, and there cases where it does not properly work.