7501#line 1007
7502 tmp___1 = __VERIFIER_nondet_int();
7503 }
7504#line 1007
7505 if (tmp___1 != 0) {
7506#line 1008
7507 goto ldv_35457;
7508 } else {
7509#line 1010
7510 goto ldv_35459;
7511 }
7512 ldv_35459: ;
7513 {
7514#line 1072
7515 marvell_exit();
7516 }
7517 ldv_final:
7518 {
7519#line 1075
7520 ldv_check_final_state();
7521 }
7522#line 1078
7523 return;
7524}
7525}
7526#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15076/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
7527void ldv_blast_assert(void)
7528{
7529
7530 {
7531 ERROR: ;
7532#line 6
7533 goto ERROR;
7534}
7535}
7536#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15076/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
7537extern int __VERIFIER_nondet_int(void) ;
7538#line 1099 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15076/dscv_tempdir/dscv/ri/43_1a/drivers/net/phy/marvell.c.p"
7539int ldv_spin = 0;
7540#line 1103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15076/dscv_tempdir/dscv/ri/43_1a/drivers/net/phy/marvell.c.p"
7541void ldv_check_alloc_flags(gfp_t flags )