2999#line 184
3000 tmp___1 = __VERIFIER_nondet_int();
3001 }
3002#line 184
3003 if (tmp___1 != 0) {
3004#line 185
3005 goto ldv_19768;
3006 } else {
3007#line 187
3008 goto ldv_19770;
3009 }
3010 ldv_19770: ;
3011 {
3012#line 220
3013 ch_exit();
3014 }
3015 ldv_final:
3016 {
3017#line 223
3018 ldv_check_final_state();
3019 }
3020#line 226
3021 return;
3022}
3023}
3024#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4821/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3025void ldv_blast_assert(void)
3026{
3027
3028 {
3029 ERROR: ;
3030#line 6
3031 goto ERROR;
3032}
3033}
3034#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4821/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3035extern int __VERIFIER_nondet_int(void) ;
3036#line 247 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4821/dscv_tempdir/dscv/ri/43_1a/drivers/hid/hid-chicony.c.p"
3037int ldv_spin = 0;
3038#line 251 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4821/dscv_tempdir/dscv/ri/43_1a/drivers/hid/hid-chicony.c.p"
3039void ldv_check_alloc_flags(gfp_t flags )