<div dir="ltr"><br><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"><span class=""><br></span>
Yes, that is what I had in mind.  Moreover, in<br>
<br>
func()<br>
{<br>
  int k = load a, invariant.load !1<br>
  print(k);<br>
  store a, 5<br>
}<br>
<br>
k can be optimized to 5, in a form of "time traveling store<br>
forwarding" :).  The store (at least if non-atomic and non-volatile)<br>
is also trivially dead.<br><br></blockquote><div><br></div><div>Only if we know that print() returns, right?</div><div><br></div><div>Otherwise, we have the usual trouble with things like:<br></div><div>void print(int i) {</div><div>  if (k != 5) abort();</div><div>  ...  </div><div>} </div></div><br></div></div>