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

void cstrcat(char s1[], char s2[]) {
    int s = 0, j = 0;
    while (s1[s] != '\0')
        s++;
    // while ((s1[s++] = s2[j++]) != 0) {}
    while (s2[j] != 0) {
      s1[s] = s2[j];
      s++;
      j++;
    }
    s1[s] = s2[j];
}

int main(int length1, int length2, int length3, char nondetString1[], char nondetString2[]) {
    if (length2 - length3 < length1 || length3 > length2) return 0;
    nondetString1[length1-1] = 0;
    nondetString2[length3-1] = 0;
    cstrcat(nondetString2,nondetString1);
    return 0;
}

[length1 >= 1 /\ length2 >= 2 /\ length3 >= 1 /\ size(nondetString1) = length1 /\ size(nondetString2) = length2]
