1889#line 120
1890 tmp___1 = __VERIFIER_nondet_int();
1891 }
1892#line 120
1893 if (tmp___1 != 0) {
1894#line 121
1895 goto ldv_21994;
1896 } else {
1897#line 123
1898 goto ldv_21996;
1899 }
1900 ldv_21996: ;
1901 {
1902#line 137
1903 exit_rc_map_lirc();
1904 }
1905 ldv_final:
1906 {
1907#line 140
1908 ldv_check_final_state();
1909 }
1910#line 143
1911 return;
1912}
1913}
1914#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9168/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1915void ldv_blast_assert(void)
1916{
1917
1918 {
1919 ERROR: ;
1920#line 6
1921 goto ERROR;
1922}
1923}
1924#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9168/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1925extern int __VERIFIER_nondet_int(void) ;
1926#line 164 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9168/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-lirc.c.p"
1927int ldv_spin = 0;
1928#line 168 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9168/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-lirc.c.p"
1929void ldv_check_alloc_flags(gfp_t flags )