6832 } else {
6833
6834 }
6835#line 1512
6836 goto switch_break;
6837 switch_default:
6838#line 1513
6839 goto switch_break;
6840 } else {
6841 switch_break: ;
6842 }
6843 }
6844 }
6845 }
6846 while_break: ;
6847 }
6848 ldv_module_exit:
6849 {
6850#line 1522
6851 ldv_check_final_state();
6852 }
6853#line 1525
6854 return;
6855}
6856}
6857#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12370/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
6858void ldv_blast_assert(void)
6859{
6860
6861 {
6862 ERROR:
6863#line 6
6864 goto ERROR;
6865}
6866}
6867#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12370/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
6868extern int __VERIFIER_nondet_int(void) ;
6869#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12370/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6870int ldv_mutex = 1;
6871#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12370/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6872int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )