5380 tmp___0 = __VERIFIER_nondet_int();
5381 }
5382#line 408
5383 if (tmp___0 != 0) {
5384#line 410
5385 goto ldv_22870;
5386 } else
5387#line 408
5388 if (ldv_s_mt2131_tuner_ops_dvb_tuner_ops != 0) {
5389#line 410
5390 goto ldv_22870;
5391 } else {
5392#line 412
5393 goto ldv_22872;
5394 }
5395 ldv_22872: ;
5396
5397 {
5398#line 518
5399 ldv_check_final_state();
5400 }
5401#line 521
5402 return;
5403}
5404}
5405#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9522/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
5406void ldv_blast_assert(void)
5407{
5408
5409 {
5410 ERROR: ;
5411#line 6
5412 goto ERROR;
5413}
5414}
5415#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9522/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
5416extern int __VERIFIER_nondet_int(void) ;
5417#line 542 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9522/dscv_tempdir/dscv/ri/43_1a/drivers/media/common/tuners/mt2131.c.p"
5418int ldv_spin = 0;
5419#line 546 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9522/dscv_tempdir/dscv/ri/43_1a/drivers/media/common/tuners/mt2131.c.p"
5420void ldv_check_alloc_flags(gfp_t flags )