extern void __VERIFIER_error() __attribute__ ((__noreturn__)); extern void __VERIFIER_assume(int); void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } extern int __VERIFIER_nondet_int(void); int SIZE; int main() { SIZE = __VERIFIER_nondet_int(); if(SIZE > 1) { long long i; long long a[SIZE]; for(i=0; i