1823#line 718
1824 tmp___1 = __VERIFIER_nondet_int();
1825 }
1826#line 718
1827 if (tmp___1 != 0) {
1828#line 719
1829 goto ldv_14760;
1830 } else {
1831#line 721
1832 goto ldv_14762;
1833 }
1834 ldv_14762: ;
1835 {
1836#line 1032
1837 test_power_exit();
1838 }
1839 ldv_final:
1840 {
1841#line 1045
1842 ldv_check_final_state();
1843 }
1844#line 1048
1845 return;
1846}
1847}
1848#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1849void ldv_blast_assert(void)
1850{
1851
1852 {
1853 ERROR: ;
1854#line 6
1855 goto ERROR;
1856}
1857}
1858#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1859extern int __VERIFIER_nondet_int(void) ;
1860#line 1069 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1861int ldv_spin = 0;
1862#line 1073 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1863void ldv_check_alloc_flags(gfp_t flags )