1684#line 277
1685 tmp___1 = __VERIFIER_nondet_int();
1686 }
1687#line 277
1688 if (tmp___1 != 0) {
1689#line 278
1690 goto ldv_15354;
1691 } else {
1692#line 280
1693 goto ldv_15356;
1694 }
1695 ldv_15356: ;
1696 {
1697#line 320
1698 edac_exit_mce_inject();
1699 }
1700 ldv_final:
1701 {
1702#line 323
1703 ldv_check_final_state();
1704 }
1705#line 326
1706 return;
1707}
1708}
1709#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12062/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1710void ldv_blast_assert(void)
1711{
1712
1713 {
1714 ERROR: ;
1715#line 6
1716 goto ERROR;
1717}
1718}
1719#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12062/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1720extern int __VERIFIER_nondet_int(void) ;
1721#line 347 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12062/dscv_tempdir/dscv/ri/43_1a/drivers/edac/mce_amd_inj.c.p"
1722int ldv_spin = 0;
1723#line 351 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12062/dscv_tempdir/dscv/ri/43_1a/drivers/edac/mce_amd_inj.c.p"
1724void ldv_check_alloc_flags(gfp_t flags )