-- This file tests array uses with prior knowledge PROC p(INT x, y, z) INT i,j: [10]INT a: %% : PROC m() SKIP : %PASS Distinct variables SEQ i, j := 1,2 PAR a[i] := 0 a[j] := 0 %FAIL Same variable SEQ i, j := 1, 1 PAR a[i] := 0 a[j] := 0 %PASS Distinct variable based on earlier equality SEQ i := j PAR a[i] := 0 a[j + 1] := 0 %PASS Distinct variables due to bounds SEQ k = 0 FOR 4 PAR a[4] := 0 a[k] := 0 %FAIL Non-distinct variables due to bounds SEQ k = 0 FOR 4 PAR a[3] := 0 a[k] := 0 %PASS Distinct due to IF IF i = 3 PAR a[i] := 0 a[4] := 0 %