/* SOURCE: https://github.com/sosy-lab/sv-benchmarks/blob/master/c/array-memsafety/diff-alloca_true-valid-memsafety.c */

void diff(int A[], int Alen, int B[], int Blen, int D[]) {
    int k = 0;
    int i = 0;
    int l1 = Alen;
    int l2 = Blen;
    int found;

    while (i < l1) {
        int j = 0;
        found = 0;
        while (j < l2 && !found) {
            if(A[i] == B[j]) {
                found = 1;
            } else {
                j++;
            }
        }
        if (!found) {
            D[k] = A[i];
            k++;
        }
        i++;
    }
}

int main(int Alen, int Blen, int A[], int B[], int D[]) {
  diff(A, Alen, B, Blen, D);
  return 0;
}


[alen >= 1 /\ Alen < 2147483647 /\ Blen >= 1 /\ Blen < 2147483647 /\ size(A) = Alen /\ size(B) = Blen /\ size(D) = Alen]

