3018#line 191
3019 tmp___1 = __VERIFIER_nondet_int();
3020 }
3021#line 191
3022 if (tmp___1 != 0) {
3023#line 192
3024 goto ldv_19771;
3025 } else {
3026#line 194
3027 goto ldv_19773;
3028 }
3029 ldv_19773: ;
3030 {
3031#line 227
3032 ts_exit();
3033 }
3034 ldv_final:
3035 {
3036#line 230
3037 ldv_check_final_state();
3038 }
3039#line 233
3040 return;
3041}
3042}
3043#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4863/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3044void ldv_blast_assert(void)
3045{
3046
3047 {
3048 ERROR: ;
3049#line 6
3050 goto ERROR;
3051}
3052}
3053#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4863/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3054extern int __VERIFIER_nondet_int(void) ;
3055#line 254 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4863/dscv_tempdir/dscv/ri/43_1a/drivers/hid/hid-topseed.c.p"
3056int ldv_spin = 0;
3057#line 258 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4863/dscv_tempdir/dscv/ri/43_1a/drivers/hid/hid-topseed.c.p"
3058void ldv_check_alloc_flags(gfp_t flags )