Feature: Collecting solving statistics for diagonstics

[ThomasHaas]

We should have a (toggable) feature in the Refinement procedure that allows us to collect (dynamic) information about all observed executions and check that against our statically derived information. This would allow us to more easily find weak spots and/or places for optimizations.

We should collect at least:

• The events that were executed (+ frequency maybe?). Never-executed events show a possibility to improve dead code elimination.
• The addresses/aliases of memory events. We can check the dynamic aliases against our alias analysis to see how (in)accurate we are and maybe get ideas to improve the analysis.
• The values of memory events and local events. The values are helpful to understand if we could reduce the width of bitvectors (i.e., if a value-range analysis would be good to have).
• The edges of base relations like co and rf. This could show weaknesses in our relation analysis.