9373 tmp___0 = __VERIFIER_nondet_int();
9374 }
9375#line 605
9376 if (tmp___0 != 0) {
9377#line 607
9378 goto ldv_22916;
9379 } else
9380#line 605
9381 if (ldv_s_qt1010_tuner_ops_dvb_tuner_ops != 0) {
9382#line 607
9383 goto ldv_22916;
9384 } else {
9385#line 609
9386 goto ldv_22918;
9387 }
9388 ldv_22918: ;
9389
9390 {
9391#line 733
9392 ldv_check_final_state();
9393 }
9394#line 736
9395 return;
9396}
9397}
9398#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9526/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
9399void ldv_blast_assert(void)
9400{
9401
9402 {
9403 ERROR: ;
9404#line 6
9405 goto ERROR;
9406}
9407}
9408#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9526/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
9409extern int __VERIFIER_nondet_int(void) ;
9410#line 757 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9526/dscv_tempdir/dscv/ri/43_1a/drivers/media/common/tuners/qt1010.c.p"
9411int ldv_spin = 0;
9412#line 761 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9526/dscv_tempdir/dscv/ri/43_1a/drivers/media/common/tuners/qt1010.c.p"
9413void ldv_check_alloc_flags(gfp_t flags )