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

int cstrcmp(char s1[], char s2[]) {
     int uc1, uc2;
     int i = 0, j = 0;
     while (s1[i] != 0 && s1[i] == s2[j]) {
         i++;
         j++;
     }
     uc1 = s1[i];
     uc2 = s2[j];
     return ((uc1 < uc2) ? -1 : (uc1 > uc2));
 }

int main(int length1, int length2, char nondetString1[], char nondetString2[]) {
    nondetString1[length1-1] = 0;
    nondetString2[length2-1] = 0;
    return cstrcmp(nondetString1,nondetString2);
}

constraint: [length1 >= 1 /\ length2 >= 1 /\ size(nondetString1) = length1 /\ size(nondetString2) = length2]

