LISA LISA-ppo-weakness2 (* ppo sequences shouldn't need to end with an Alpha-strong-ppo link. This example's cycle is: strong-prop, rd-addr, obs. Same as LISA-ppo-weakness, with lderef read changed into rb_dep fence. *) { x=v; 1:r0=u; } P0 | P1 | P2 ; r[once] r0 x | w[once] y 2 | w[once] u 1 ; f[rb_dep] | | ; r[once] r1 r0 | f[mb] | f[wmb] ; r[once] r2 y | w[once] x r0 | w[once] y 1 ; Observed y=2; 0:r2=2; 0:r1=0; 0:r0=u; and y=2; 0:r2=0; 0:r1=0; 0:r0=u;