9836 tmp___0 = __VERIFIER_nondet_int();
9837 }
9838#line 925
9839 if (tmp___0 != 0) {
9840#line 927
9841 goto ldv_39163;
9842 } else
9843#line 925
9844 if (ldv_s_mxl111sf_demod_ops_dvb_frontend_ops != 0) {
9845#line 927
9846 goto ldv_39163;
9847 } else {
9848#line 929
9849 goto ldv_39165;
9850 }
9851 ldv_39165: ;
9852
9853 {
9854#line 1289
9855 ldv_check_final_state();
9856 }
9857#line 1292
9858 return;
9859}
9860}
9861#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8605/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
9862void ldv_blast_assert(void)
9863{
9864
9865 {
9866 ERROR: ;
9867#line 6
9868 goto ERROR;
9869}
9870}
9871#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8605/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
9872extern int __VERIFIER_nondet_int(void) ;
9873#line 1313 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8605/dscv_tempdir/dscv/ri/43_1a/drivers/media/dvb/dvb-usb/mxl111sf-demod.c.p"
9874int ldv_spin = 0;
9875#line 1317 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8605/dscv_tempdir/dscv/ri/43_1a/drivers/media/dvb/dvb-usb/mxl111sf-demod.c.p"
9876void ldv_check_alloc_flags(gfp_t flags )