4628 } else {
4629
4630 }
4631#line 231
4632 goto switch_break;
4633 switch_default:
4634#line 232
4635 goto switch_break;
4636 } else {
4637 switch_break: ;
4638 }
4639 }
4640 }
4641 }
4642 while_break: ;
4643 }
4644 ldv_module_exit:
4645 {
4646#line 241
4647 ldv_check_final_state();
4648 }
4649#line 244
4650 return;
4651}
4652}
4653#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3996/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4654void ldv_blast_assert(void)
4655{
4656
4657 {
4658 ERROR:
4659#line 6
4660 goto ERROR;
4661}
4662}
4663#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3996/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4664extern int __VERIFIER_nondet_int(void) ;
4665#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3996/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4666int ldv_mutex = 1;
4667#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3996/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4668int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )