AWZ算法的例子依旧来自于RKS的这篇文章《Detecting Equalities of Variables: Combining Efficiency with Precision》。

上面两个图，进行的是如下图所示的循环结构的等价类计算。


为什么得到的结果不是上图而是下图呢？这里其实是因为用到的AWZ的算法也是optimistic的，否则就无法发现x2和y2，x1和y1之间的等价性。有点类似于计算机中的死锁，两个互相依赖，都判断不了。