Test LB+addr+addrpx-poxp+VAR2

RISCV LB+addr+addrpx-poxp+VAR2
(*
   Variation on a test by Shaked Flur.

   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.
   This test illustrates the two possibilities of the sc
   succeeding or failling.
*)   
{
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)  | lr.w x4,0(x8)      ;
               | sc.w x11,x10,0(x9) ;
               | ori x12,x0,1       ;
               | sw x12,0(x13)      ;
               
locations [1:x11;]
exists
(0:x5=1 /\ 1:x5=1 /\ not(1:x11=0))