9858 goto ldv_23854;
9859 } else
9860#line 799
9861 if (ldv_s_mt2032_tuner_ops_dvb_tuner_ops != 0) {
9862#line 802
9863 goto ldv_23854;
9864 } else
9865#line 799
9866 if (ldv_s_mt2050_tuner_ops_dvb_tuner_ops != 0) {
9867#line 802
9868 goto ldv_23854;
9869 } else {
9870#line 804
9871 goto ldv_23856;
9872 }
9873 ldv_23856: ;
9874
9875 {
9876#line 941
9877 ldv_check_final_state();
9878 }
9879#line 944
9880 return;
9881}
9882}
9883#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9521/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
9884void ldv_blast_assert(void)
9885{
9886
9887 {
9888 ERROR: ;
9889#line 6
9890 goto ERROR;
9891}
9892}
9893#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9521/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
9894extern int __VERIFIER_nondet_int(void) ;
9895#line 965 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9521/dscv_tempdir/dscv/ri/43_1a/drivers/media/common/tuners/mt20xx.c.p"
9896int ldv_spin = 0;
9897#line 969 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9521/dscv_tempdir/dscv/ri/43_1a/drivers/media/common/tuners/mt20xx.c.p"
9898void ldv_check_alloc_flags(gfp_t flags )