#include extern int __VERIFIER_nondet_int(void); extern char __VERIFIER_nondet_char(void); int main() { int i, j, tmp; int length = __VERIFIER_nondet_int(); if (length < 1) length = 1; // make sure that length is odd if (length % 2 == 0) length++; int *arr = alloca(length); for(int i = 0; i < length; i++) { arr[i] = __VERIFIER_nondet_int(); } // make sure the marker occurs only once for (i=0; i