3280#line 246
3281 tmp___1 = __VERIFIER_nondet_int();
3282 }
3283#line 246
3284 if (tmp___1 != 0) {
3285#line 247
3286 goto ldv_19791;
3287 } else {
3288#line 249
3289 goto ldv_19793;
3290 }
3291 ldv_19793: ;
3292 {
3293#line 282
3294 twinhan_exit();
3295 }
3296 ldv_final:
3297 {
3298#line 285
3299 ldv_check_final_state();
3300 }
3301#line 288
3302 return;
3303}
3304}
3305#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4864/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3306void ldv_blast_assert(void)
3307{
3308
3309 {
3310 ERROR: ;
3311#line 6
3312 goto ERROR;
3313}
3314}
3315#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4864/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3316extern int __VERIFIER_nondet_int(void) ;
3317#line 309 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4864/dscv_tempdir/dscv/ri/43_1a/drivers/hid/hid-twinhan.c.p"
3318int ldv_spin = 0;
3319#line 313 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4864/dscv_tempdir/dscv/ri/43_1a/drivers/hid/hid-twinhan.c.p"
3320void ldv_check_alloc_flags(gfp_t flags )