8629 } else {
8630
8631 }
8632#line 495
8633 goto switch_break;
8634 switch_default:
8635#line 496
8636 goto switch_break;
8637 } else {
8638 switch_break: ;
8639 }
8640 }
8641 }
8642 }
8643 while_break: ;
8644 }
8645 ldv_module_exit:
8646 {
8647#line 505
8648 ldv_check_final_state();
8649 }
8650#line 508
8651 return;
8652}
8653}
8654#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13501/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
8655void ldv_blast_assert(void)
8656{
8657
8658 {
8659 ERROR:
8660#line 6
8661 goto ERROR;
8662}
8663}
8664#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13501/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
8665extern int __VERIFIER_nondet_int(void) ;
8666#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13501/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
8667int ldv_mutex = 1;
8668#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13501/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
8669int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )