9533 } else {
9534
9535 }
9536#line 505
9537 goto switch_break;
9538 switch_default:
9539#line 506
9540 goto switch_break;
9541 } else {
9542 switch_break: ;
9543 }
9544 }
9545 }
9546 }
9547 while_break: ;
9548 }
9549 ldv_module_exit:
9550 {
9551#line 515
9552 ldv_check_final_state();
9553 }
9554#line 518
9555 return;
9556}
9557}
9558#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13527/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
9559void ldv_blast_assert(void)
9560{
9561
9562 {
9563 ERROR:
9564#line 6
9565 goto ERROR;
9566}
9567}
9568#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13527/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
9569extern int __VERIFIER_nondet_int(void) ;
9570#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13527/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
9571int ldv_mutex = 1;
9572#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13527/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
9573int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )