8513 } else {
8514
8515 }
8516#line 366
8517 goto switch_break;
8518 switch_default:
8519#line 367
8520 goto switch_break;
8521 } else {
8522 switch_break: ;
8523 }
8524 }
8525 }
8526 }
8527 while_break: ;
8528 }
8529 ldv_module_exit:
8530 {
8531#line 376
8532 ldv_check_final_state();
8533 }
8534#line 379
8535 return;
8536}
8537}
8538#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13509/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
8539void ldv_blast_assert(void)
8540{
8541
8542 {
8543 ERROR:
8544#line 6
8545 goto ERROR;
8546}
8547}
8548#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13509/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
8549extern int __VERIFIER_nondet_int(void) ;
8550#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13509/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
8551int ldv_mutex = 1;
8552#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13509/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
8553int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )