extern void __VERIFIER_error(void); extern void __VERIFIER_assume(int); void __VERIFIER_assert(int cond) { if (!(cond)) { ERROR: __VERIFIER_error(); } return; } int __VERIFIER_nondet_int(); int __BLAST_NONDET; int main() { int i,j,k,n,l,m; n = __VERIFIER_nondet_int(); m = __VERIFIER_nondet_int(); l = __VERIFIER_nondet_int(); if (!(-1000000 < n && n < 1000000)) return 0; if (!(-1000000 < m && m < 1000000)) return 0; if (!(-1000000 < l && l < 1000000)) return 0; if(3*n<=m+l); else goto END; for (i=0;i