9569 } else {
9570
9571 }
9572#line 855
9573 goto switch_break;
9574 switch_default:
9575#line 856
9576 goto switch_break;
9577 } else {
9578 switch_break: ;
9579 }
9580 }
9581 }
9582 }
9583 while_break: ;
9584 }
9585 ldv_module_exit:
9586 {
9587#line 865
9588 ldv_check_final_state();
9589 }
9590#line 868
9591 return;
9592}
9593}
9594#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13504/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
9595void ldv_blast_assert(void)
9596{
9597
9598 {
9599 ERROR:
9600#line 6
9601 goto ERROR;
9602}
9603}
9604#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13504/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
9605extern int __VERIFIER_nondet_int(void) ;
9606#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13504/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
9607int ldv_mutex = 1;
9608#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13504/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
9609int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )