11527 } else {
11528
11529 }
11530#line 2110
11531 goto switch_break;
11532 switch_default:
11533#line 2111
11534 goto switch_break;
11535 } else {
11536 switch_break: ;
11537 }
11538 }
11539 }
11540 }
11541 while_break: ;
11542 }
11543 ldv_module_exit:
11544 {
11545#line 2120
11546 ldv_check_final_state();
11547 }
11548#line 2123
11549 return;
11550}
11551}
11552#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7669/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
11553void ldv_blast_assert(void)
11554{
11555
11556 {
11557 ERROR:
11558#line 6
11559 goto ERROR;
11560}
11561}
11562#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7669/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
11563extern int __VERIFIER_nondet_int(void) ;
11564#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7669/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
11565int ldv_mutex = 1;
11566#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7669/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
11567int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )