Separation of concrete and symbolic execution

Disentangling concrete and symbolic representation and execution has a potential to significantly improve runtime performance while simultaneously making the codebase less complex and easier to maintain.

For example

- all the gas related computations could be removed from symbolic exploration
- concrete execution could use only concrete representation, without the need to deal with `Exprs`.
