Test LB+addr+addrpx-poxp+VAR

RISCV LB+addr+addrpx-poxp+VAR
(*
   Test by Shaked Flur. On P1, assuming sc fails.
     The existence of an address dependency from initial read
     to "write conditional" and thus of ppo from initial read
     to last write depends on the existence of a specific
     "write -conditional-failed" event.
     At the moment Allow.
*)   
{
0:x6=x; 0:x9=y;
1:x6=y; 1:x8=z; 1:x13=x;
}
 P0            | P1                 ;
 lw x5,0(x6)   | lw x5,0(x6)        ;
 xor x7,x5,x5  | xor x7,x5,x5       ;
 ori x8,x0,1   | add x9,x8,x7       ;
 add x10,x9,x7 | ori x10,x0,1       ;
 sw x8,0(x10)  | sc.w x11,x10,0(x9) ;
               | ori x12,x0,1       ;
               | sw x12,0(x13)      ;

locations [1:x11;]
exists
(0:x5=1 /\ 1:x5=1)