<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><div><br></div><div>The real reason is because it got closer to the maximal fixpoint than the original version.</div></div></div></div></blockquote><div><br></div><div>this should be "original call" not "original version", since it's about whether the cached version gets different answers depending on the order in which you ask it answers and invalidate.</div><div><br></div><div>(I clarify because it is *also* true that the original, non-cached, version will get the same answer no matter order you ask it since it never stores any answers, and thus never gets any closer to the maximal fixpoint then where it starts)</div><div><br></div><div>Note that it is pretty much impossible to fix this issue on demand without  removing the depth limits.</div><div>IE If you wanted it to always give the same answers, at a minimum, you'd have to invalidate with knowledge of the depth limits and whatever, and be able to compute what would have changed had it been able to go deeper.  This is equivalent to actually computing it.</div><div><br></div><div>Worse, for most of these problems (it is definitely true for the known bits problem in general, i just haven't started at the code long enough to be comfortable saying it is true here) you can prove that proper visitation order also is required to achieve maximal fixpoint in the presence of loops and phis, so even removing depth limits would not be enough for making sure edge cases come out the same when you store answers.</div><div><br></div><div>Or you can give up on verification.</div><div><br></div><div>Historically we:<br><br></div><div>A. give up on verification, </div><div>B. slowly increase the limits to try to get closer to maximal fixpoint, until we are really just computing the problem for everything, in the wrong order.</div><div><br></div><div>(i'm not trying to be snarky, that is literally the approach we have taken :P)</div><div><br></div><div><br></div></div></div></div>