4435#line 653
4436 tmp___1 = __VERIFIER_nondet_int();
4437 }
4438#line 653
4439 if (tmp___1 != 0) {
4440#line 654
4441 goto ldv_28948;
4442 } else {
4443#line 656
4444 goto ldv_28950;
4445 }
4446 ldv_28950: ;
4447 {
4448#line 1182
4449 ksphy_exit();
4450 }
4451 ldv_final:
4452 {
4453#line 1185
4454 ldv_check_final_state();
4455 }
4456#line 1188
4457 return;
4458}
4459}
4460#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15079/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4461void ldv_blast_assert(void)
4462{
4463
4464 {
4465 ERROR: ;
4466#line 6
4467 goto ERROR;
4468}
4469}
4470#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15079/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4471extern int __VERIFIER_nondet_int(void) ;
4472#line 1209 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15079/dscv_tempdir/dscv/ri/43_1a/drivers/net/phy/micrel.c.p"
4473int ldv_spin = 0;
4474#line 1213 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15079/dscv_tempdir/dscv/ri/43_1a/drivers/net/phy/micrel.c.p"
4475void ldv_check_alloc_flags(gfp_t flags )