13559 } else {
13560
13561 }
13562#line 6882
13563 goto switch_break;
13564 switch_default:
13565#line 6883
13566 goto switch_break;
13567 } else {
13568 switch_break: ;
13569 }
13570 }
13571 }
13572 }
13573 while_break: ;
13574 }
13575 ldv_module_exit:
13576 {
13577#line 6892
13578 ldv_check_final_state();
13579 }
13580#line 6895
13581 return;
13582}
13583}
13584#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13535/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
13585void ldv_blast_assert(void)
13586{
13587
13588 {
13589 ERROR:
13590#line 6
13591 goto ERROR;
13592}
13593}
13594#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13535/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
13595extern int __VERIFIER_nondet_int(void) ;
13596#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13535/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
13597int ldv_mutex = 1;
13598#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13535/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
13599int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )