Implement Implied Value Concretization

[feliam]

When a constraint such as x + 1 = 10 is added to the path condition, then the value of x has effectively become concrete along that path. This can be detected (in this case that x = 9) and the concrete value can be written back to the state (memory or storage or stack). This ensures that subsequent accesses of that value return a cheap constant expression. Potentially generating less solver queries.

This feature would need a little research. When such situation is detected we need a way to search or reference back to where the expression came from or it is used in the state.

• This should be configurable using config.py
• Overall symbolic execution performance gain should be measure/tested over a big test set (see Put together a large set of contract examples #1204)