13117 tmp___0 = __VERIFIER_nondet_int();
13118 }
13119#line 1390
13120 if (tmp___0 != 0) {
13121#line 1392
13122 goto ldv_23203;
13123 } else
13124#line 1390
13125 if (ldv_s_tuner_ops_dvb_tuner_ops != 0) {
13126#line 1392
13127 goto ldv_23203;
13128 } else {
13129#line 1394
13130 goto ldv_23205;
13131 }
13132 ldv_23205: ;
13133
13134 {
13135#line 1551
13136 ldv_check_final_state();
13137 }
13138#line 1554
13139 return;
13140}
13141}
13142#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8474/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
13143void ldv_blast_assert(void)
13144{
13145
13146 {
13147 ERROR: ;
13148#line 6
13149 goto ERROR;
13150}
13151}
13152#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8474/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
13153extern int __VERIFIER_nondet_int(void) ;
13154#line 1575 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8474/dscv_tempdir/dscv/ri/43_1a/drivers/media/dvb/frontends/tda18271c2dd.c.p"
13155int ldv_spin = 0;
13156#line 1579 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8474/dscv_tempdir/dscv/ri/43_1a/drivers/media/dvb/frontends/tda18271c2dd.c.p"
13157void ldv_check_alloc_flags(gfp_t flags )