text: extern void __VERIFIER_error() __attribute__ ((__noreturn__));
  
  void __VERIFIER_assert(int cond) {
    if (!(cond)) {
      ERROR: __VERIFIER_error();
    }
    return;
  }
  unsigned int __VERIFIER_nondet_uint();
  int main() {
     unsigned int SIZE=__VERIFIER_nondet_uint();
     int i, j, k, key;
     int v[SIZE];   
     for (j=1;j<SIZE;j++) {	  
        key = v[j];
        i = j - 1;
        while((i>=0) && (v[i]>key)) {
           if (i<2)
           v[i+1] = v[i];
           i = i - 1;
        }
        v[i+1] = key;	        
    }      
    for (k=1;k<SIZE;k++)
      __VERIFIER_assert(v[k-1]<=v[k]);  
     return 0;
  }
  