Description
To ease the explaination and debugging of what the analysis does, we should add:

• an accumulating fixpoint that stores all states produced on each program point, as in to explain what happens inside loops
• a fixpoint trace, showing which functions and statements were analyzed in which order
• an interpretation trace, enriching the fixpoint trace with what symbolic expressions are processed by the analysis
• an evaluation trace, enriching the interpretation trace by dumping the analysis states at some key points (maybe using a predicate?)