Hi Dave,

> On 21 Mar 2023, at 00:30, David Malcolm via Gcc <gcc@gcc.gnu.org> wrote:
> 
> I implemented my own approach, with a "widening_svalue" subclass of
> symbolic value.  This is widening in the Abstract Interpretation sense,
> (as opposed to the bitwise operations sense): if I see multiple values
> on successive iterations, the widening_svalue tries to simulate that we
> know the start value and the direction the variable is moving in.

I forgot to mention there is a relevant section “path selection” in the paper I mentioned several times (https://users.ece.cmu.edu/~aavgerin/papers/Oakland10.pdf).