8831 } else {
8832
8833 }
8834#line 383
8835 goto switch_break;
8836 switch_default:
8837#line 384
8838 goto switch_break;
8839 } else {
8840 switch_break: ;
8841 }
8842 }
8843 }
8844 }
8845 while_break: ;
8846 }
8847 ldv_module_exit:
8848 {
8849#line 393
8850 ldv_check_final_state();
8851 }
8852#line 396
8853 return;
8854}
8855}
8856#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13524/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
8857void ldv_blast_assert(void)
8858{
8859
8860 {
8861 ERROR:
8862#line 6
8863 goto ERROR;
8864}
8865}
8866#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13524/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
8867extern int __VERIFIER_nondet_int(void) ;
8868#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13524/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
8869int ldv_mutex = 1;
8870#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13524/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
8871int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )