AArch64 coRR-pte13 { int x=1; int y=2; 0:X2=x; 1:X4=pte_x; 1:X6=pte_y; } P0 | P1 ; LDR W0,[X2] | LDR X0,[X6] ; LDR W1,[X2] | STR X0,[X4] ; exists (0:X0=2 /\ 0:X1=1)