Find bottlenecks in analysis of large counterexamples.
Matthias: The bottleneck for the LDV examples seems to be the array quantifier elimination during the computation of WP for summaries (resp. the return statements).
The array quantifier elimination can be improved significantly (note for MH: explicit index-value comparison instead of simplifyDDA postprocessing).
Compute WP without explicit summaries (note for MH: use symbolic summary for return, compute preliminary WP up to call, instanciate symbolic summary, obtain final WP via post-processing).
Find bottlenecks in analysis of large counterexamples. Matthias: The bottleneck for the LDV examples seems to be the array quantifier elimination during the computation of WP for summaries (resp. the return statements).