RISCV PPOLDSTLD01 "Fence.w.wdWW Rfe DpDatadW Rfi DpAddrdR Fre" (* Test for ppo rule ld->st->ld, or (addr|data);rfi Forbid *) { 0:x6=x; 0:x8=y; 1:x6=y; 1:x8=z; 1:x12=x; } P0 | P1 ; ori x5,x0,1 | lw x5,0(x6) ; sw x5,0(x6) | andi x7,x5,128 ; fence w,w | ori x7,x7,1 ; ori x7,x0,1 | sw x7,0(x8) ; sw x7,0(x8) | lw x9,0(x8) ; | andi x10,x9,128 ; | add x13,x12,x10 ; | lw x11,0(x13) ; exists (1:x5=1 /\ 1:x9=1 /\ 1:x11=0)