5597#line 287
5598 tmp___1 = __VERIFIER_nondet_int();
5599 }
5600#line 287
5601 if (tmp___1 != 0) {
5602#line 288
5603 goto ldv_35148;
5604 } else {
5605#line 290
5606 goto ldv_35150;
5607 }
5608 ldv_35150: ;
5609 {
5610#line 442
5611 ste10Xp_exit();
5612 }
5613 ldv_final:
5614 {
5615#line 445
5616 ldv_check_final_state();
5617 }
5618#line 448
5619 return;
5620}
5621}
5622#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15085/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
5623void ldv_blast_assert(void)
5624{
5625
5626 {
5627 ERROR: ;
5628#line 6
5629 goto ERROR;
5630}
5631}
5632#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15085/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
5633extern int __VERIFIER_nondet_int(void) ;
5634#line 469 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15085/dscv_tempdir/dscv/ri/43_1a/drivers/net/phy/ste10Xp.c.p"
5635int ldv_spin = 0;
5636#line 473 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15085/dscv_tempdir/dscv/ri/43_1a/drivers/net/phy/ste10Xp.c.p"
5637void ldv_check_alloc_flags(gfp_t flags )