/* VERIFY_OPTS: --symbolic --sequential */ /* TAGS: sym inf big c todo */ #include extern void __VERIFIER_assert(int); extern bool __VERIFIER_nondet_bool(void); int main(){ int a[5]; int len=0; int i; while(__VERIFIER_nondet_bool()){ if (len==4) len =0; a[len]=0; len++; } __VERIFIER_assert(len>=0 && len<5); return 0; }