Well in this case it seems reasonable that they simply added a rule for the specific line:

    even = !even

and the line

    numberCompare++

resulting in

    even = (indvar & 1)
    numberCompare = indvar

You can then solve from the exit condition that number == numberCompare, which gives you the indvar which can then be substituted into 'even'.

I'm not saying it isn't magical, and certainly requires some symbolic solving, but it's doable.

Of course the real goal is to eventually get it to optimize

    while (number != 1) {
        if (number & 1)
            number = number * 3 + 1
        number >>= 1;
    }