14803 } else {
14804
14805 }
14806#line 1567
14807 goto switch_break;
14808 switch_default:
14809#line 1568
14810 goto switch_break;
14811 } else {
14812 switch_break: ;
14813 }
14814 }
14815 }
14816 }
14817 while_break: ;
14818 }
14819 ldv_module_exit:
14820 {
14821#line 1577
14822 ldv_check_final_state();
14823 }
14824#line 1580
14825 return;
14826}
14827}
14828#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/10324/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
14829void ldv_blast_assert(void)
14830{
14831
14832 {
14833 ERROR:
14834#line 6
14835 goto ERROR;
14836}
14837}
14838#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/10324/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
14839extern int __VERIFIER_nondet_int(void) ;
14840#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/10324/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
14841int ldv_mutex = 1;
14842#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/10324/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
14843int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )