[intuitiveness] Minimize the need for background knowledge

[Stevengre]

As we discussed in #743, I believe we need to reduce the background knowledge required for better understanding and easier verification. While our input specification is quite straightforward, the results are not easy to interpret and require knowledge of K, EVM semantics, and Kontrol's encoding algorithms. Therefore, we should develop a way to analyze the results and present information that can be understood without needing knowledge beyond Solidity. I'm not yet sure how to design this, but it might look something like this:

VERIFICATION PASSED
Verification Target: …
Precondition: …
Postcondition: …

VERIFICATION OUT-OF-TIME
A call graph with solidity expressions to split.

VERIFICATION FAILED
Location of the failed solidity program.
Reason for this failure.

The structure should be designed by experienced verification personnel to ensure that the information provided is sufficient to adjust assumptions and assertions or to identify issues in the verification target.

[palinatolmach]

This has been partially addressed by improved Solidity source maps, but it can be further improved. I'll move it to Backlog for now.