1884#line 230
1885 if (0) {
1886 switch_default:
1887#line 232
1888 goto switch_break;
1889 } else {
1890 switch_break: ;
1891 }
1892 }
1893 }
1894 while_break: ;
1895 }
1896 {
1897#line 249
1898 cleanup_mtdram();
1899 }
1900 ldv_final:
1901 {
1902#line 252
1903 ldv_check_final_state();
1904 }
1905#line 255
1906 return;
1907}
1908}
1909#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
1910void ldv_blast_assert(void)
1911{
1912
1913 {
1914 ERROR:
1915#line 6
1916 goto ERROR;
1917}
1918}
1919#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
1920extern int __VERIFIER_nondet_int(void) ;
1921#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1922int ldv_mutex = 1;
1923#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1924int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )