I’m putting these plans on hold, because I got bogged down with the technical details of implementing the widening/invalidation.
On the other hand, I implemented a suppression hack for ArrayBoundV2 which eliminates lots of loop-related false positives: [analyzer] Suppress out of bounds reports after weak loop assumptions by NagyDonat · Pull Request #109804 · llvm/llvm-project · GitHub
There is a chance that I’ll return to loop handling improvements somewhen in the future, but before that I want to finish the stabilization of ArrayBoundV2.
By the way, this suppression hack does not suppress the false positive mentioned by steakhal in his previous comment 