2985#line 564
2986 tmp___1 = __VERIFIER_nondet_int();
2987 }
2988#line 564
2989 if (tmp___1 != 0) {
2990#line 565
2991 goto ldv_20710;
2992 } else {
2993#line 567
2994 goto ldv_20712;
2995 }
2996 ldv_20712: ;
2997 {
2998#line 622
2999 nettel_cleanup();
3000 }
3001 ldv_final:
3002 {
3003#line 625
3004 ldv_check_final_state();
3005 }
3006#line 628
3007 return;
3008}
3009}
3010#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11639/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3011void ldv_blast_assert(void)
3012{
3013
3014 {
3015 ERROR: ;
3016#line 6
3017 goto ERROR;
3018}
3019}
3020#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11639/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3021extern int __VERIFIER_nondet_int(void) ;
3022#line 649 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11639/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/maps/nettel.c.p"
3023int ldv_spin = 0;
3024#line 653 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11639/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/maps/nettel.c.p"
3025void ldv_check_alloc_flags(gfp_t flags )