12628 } else {
12629
12630 }
12631#line 1411
12632 goto switch_break;
12633 switch_default:
12634#line 1412
12635 goto switch_break;
12636 } else {
12637 switch_break: ;
12638 }
12639 }
12640 }
12641 }
12642 while_break: ;
12643 }
12644 ldv_module_exit:
12645 {
12646#line 1421
12647 ldv_check_final_state();
12648 }
12649#line 1424
12650 return;
12651}
12652}
12653#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13531/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
12654void ldv_blast_assert(void)
12655{
12656
12657 {
12658 ERROR:
12659#line 6
12660 goto ERROR;
12661}
12662}
12663#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13531/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
12664extern int __VERIFIER_nondet_int(void) ;
12665#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13531/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
12666int ldv_mutex = 1;
12667#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13531/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
12668int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )