4677#line 302
4678 tmp___1 = __VERIFIER_nondet_int();
4679 }
4680#line 302
4681 if (tmp___1 != 0) {
4682#line 303
4683 goto ldv_25820;
4684 } else {
4685#line 305
4686 goto ldv_25822;
4687 }
4688 ldv_25822: ;
4689 {
4690#line 383
4691 n411_exit();
4692 }
4693 ldv_final:
4694 {
4695#line 386
4696 ldv_check_final_state();
4697 }
4698#line 389
4699 return;
4700}
4701}
4702#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1619/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4703void ldv_blast_assert(void)
4704{
4705
4706 {
4707 ERROR: ;
4708#line 6
4709 goto ERROR;
4710}
4711}
4712#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1619/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4713extern int __VERIFIER_nondet_int(void) ;
4714#line 410 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1619/dscv_tempdir/dscv/ri/43_1a/drivers/video/n411.c.p"
4715int ldv_spin = 0;
4716#line 414 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1619/dscv_tempdir/dscv/ri/43_1a/drivers/video/n411.c.p"
4717void ldv_check_alloc_flags(gfp_t flags )