7195 tmp___0 = __VERIFIER_nondet_int();
7196 }
7197#line 764
7198 if (tmp___0 != 0) {
7199#line 766
7200 goto ldv_23174;
7201 } else
7202#line 764
7203 if (ldv_s_cxd2820r_ops_dvb_frontend_ops != 0) {
7204#line 766
7205 goto ldv_23174;
7206 } else {
7207#line 768
7208 goto ldv_23176;
7209 }
7210 ldv_23176: ;
7211
7212 {
7213#line 987
7214 ldv_check_final_state();
7215 }
7216#line 990
7217 return;
7218}
7219}
7220#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8396/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
7221void ldv_blast_assert(void)
7222{
7223
7224 {
7225 ERROR: ;
7226#line 6
7227 goto ERROR;
7228}
7229}
7230#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8396/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
7231extern int __VERIFIER_nondet_int(void) ;
7232#line 1011 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8396/dscv_tempdir/dscv/ri/43_1a/drivers/media/dvb/frontends/cxd2820r_core.c.p"
7233int ldv_spin = 0;
7234#line 1015 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8396/dscv_tempdir/dscv/ri/43_1a/drivers/media/dvb/frontends/cxd2820r_core.c.p"
7235void ldv_check_alloc_flags(gfp_t flags )