Witness invariants for widened variables #1219
Description
We have a heuristic for outputting witness invariants at loop heads, which more-or-less should match with widening points, but it outputs invariants for all variables, not just those that required widening at any iteration. It would be much better to only output invariants for those variables whose values were ever widened.
There's also a heuristic for invariants for only accessed variables, but that doesn't work with the loop invariant heuristic because the variable modification is in the loop body, not at the loop head. So often this wouldn't output the desired invariants.
The biggest technical challenge is coming up with a reasonably clean implementation. Widening in IntDomain doesn't know about which variable it is for in the base analysis (nor should it), but these associations must be made somewhere and also stored somewhere. Maybe CPA/base analysis can track an extra set of widened variables? That wouldn't work for Apron though and I'm not sure how to even get that information from Apron.