5635 switch_default:
5636#line 242
5637 goto switch_break;
5638 } else {
5639 switch_break: ;
5640 }
5641 }
5642 }
5643 }
5644 while_break: ;
5645 }
5646 ldv_module_exit:
5647 {
5648#line 256
5649 pnpide_exit();
5650 }
5651 ldv_final:
5652 {
5653#line 259
5654 ldv_check_final_state();
5655 }
5656#line 262
5657 return;
5658}
5659}
5660#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12321/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
5661void ldv_blast_assert(void)
5662{
5663
5664 {
5665 ERROR:
5666#line 6
5667 goto ERROR;
5668}
5669}
5670#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12321/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
5671extern int __VERIFIER_nondet_int(void) ;
5672#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12321/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5673int ldv_mutex = 1;
5674#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12321/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5675int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )