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