3813 ldv_19186: ;
3814 ldv_19188:
3815 {
3816#line 431
3817 tmp___1 = __VERIFIER_nondet_int();
3818 }
3819#line 431
3820 if (tmp___1 != 0) {
3821#line 432
3822 goto ldv_19187;
3823 } else {
3824#line 434
3825 goto ldv_19189;
3826 }
3827 ldv_19189: ;
3828
3829 ldv_final:
3830 {
3831#line 445
3832 ldv_check_final_state();
3833 }
3834#line 448
3835 return;
3836}
3837}
3838#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11716/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3839void ldv_blast_assert(void)
3840{
3841
3842 {
3843 ERROR: ;
3844#line 6
3845 goto ERROR;
3846}
3847}
3848#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11716/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3849extern int __VERIFIER_nondet_int(void) ;
3850#line 469 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11716/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/docprobe.c.p"
3851int ldv_spin = 0;
3852#line 473 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11716/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/docprobe.c.p"
3853void ldv_check_alloc_flags(gfp_t flags )