10437 tmp___0 = __VERIFIER_nondet_int();
10438 }
10439#line 1076
10440 if (tmp___0 != 0) {
10441#line 1078
10442 goto ldv_23325;
10443 } else
10444#line 1076
10445 if (ldv_s_dib3000mc_ops_dvb_frontend_ops != 0) {
10446#line 1078
10447 goto ldv_23325;
10448 } else {
10449#line 1080
10450 goto ldv_23327;
10451 }
10452 ldv_23327: ;
10453
10454 {
10455#line 1289
10456 ldv_check_final_state();
10457 }
10458#line 1292
10459 return;
10460}
10461}
10462#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8417/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
10463void ldv_blast_assert(void)
10464{
10465
10466 {
10467 ERROR: ;
10468#line 6
10469 goto ERROR;
10470}
10471}
10472#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8417/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
10473extern int __VERIFIER_nondet_int(void) ;
10474#line 1313 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8417/dscv_tempdir/dscv/ri/43_1a/drivers/media/dvb/frontends/dib3000mc.c.p"
10475int ldv_spin = 0;
10476#line 1317 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8417/dscv_tempdir/dscv/ri/43_1a/drivers/media/dvb/frontends/dib3000mc.c.p"
10477void ldv_check_alloc_flags(gfp_t flags )