7907 } else {
7908
7909 }
7910#line 242
7911 goto switch_break;
7912 switch_default:
7913#line 243
7914 goto switch_break;
7915 } else {
7916 switch_break: ;
7917 }
7918 }
7919 }
7920 }
7921 while_break: ;
7922 }
7923 ldv_module_exit:
7924 {
7925#line 252
7926 ldv_check_final_state();
7927 }
7928#line 255
7929 return;
7930}
7931}
7932#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13508/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
7933void ldv_blast_assert(void)
7934{
7935
7936 {
7937 ERROR:
7938#line 6
7939 goto ERROR;
7940}
7941}
7942#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13508/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
7943extern int __VERIFIER_nondet_int(void) ;
7944#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13508/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
7945int ldv_mutex = 1;
7946#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13508/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
7947int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )