4598 } else {
4599
4600 }
4601#line 363
4602 goto switch_break;
4603 switch_default:
4604#line 364
4605 goto switch_break;
4606 } else {
4607 switch_break: ;
4608 }
4609 }
4610 }
4611 }
4612 while_break: ;
4613 }
4614 ldv_module_exit:
4615 {
4616#line 373
4617 ldv_check_final_state();
4618 }
4619#line 376
4620 return;
4621}
4622}
4623#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6245/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4624void ldv_blast_assert(void)
4625{
4626
4627 {
4628 ERROR:
4629#line 6
4630 goto ERROR;
4631}
4632}
4633#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6245/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4634extern int __VERIFIER_nondet_int(void) ;
4635#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6245/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4636int ldv_mutex = 1;
4637#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6245/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4638int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )