1727#line 479
1728 tmp___1 = __VERIFIER_nondet_int();
1729 }
1730#line 479
1731 if (tmp___1 != 0) {
1732#line 480
1733 goto ldv_18884;
1734 } else {
1735#line 482
1736 goto ldv_18886;
1737 }
1738 ldv_18886: ;
1739 {
1740#line 503
1741 cfag12864b_exit();
1742 }
1743 ldv_final:
1744 {
1745#line 506
1746 ldv_check_final_state();
1747 }
1748#line 509
1749 return;
1750}
1751}
1752#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1753void ldv_blast_assert(void)
1754{
1755
1756 {
1757 ERROR: ;
1758#line 6
1759 goto ERROR;
1760}
1761}
1762#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1763extern int __VERIFIER_nondet_int(void) ;
1764#line 530 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
1765int ldv_spin = 0;
1766#line 534 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
1767void ldv_check_alloc_flags(gfp_t flags )