3523 } else {
3524
3525 }
3526#line 218
3527 goto switch_break;
3528 switch_default:
3529#line 219
3530 goto switch_break;
3531 } else {
3532 switch_break: ;
3533 }
3534 }
3535 }
3536 }
3537 while_break: ;
3538 }
3539 ldv_module_exit:
3540 {
3541#line 228
3542 ldv_check_final_state();
3543 }
3544#line 231
3545 return;
3546}
3547}
3548#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1769/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3549void ldv_blast_assert(void)
3550{
3551
3552 {
3553 ERROR:
3554#line 6
3555 goto ERROR;
3556}
3557}
3558#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1769/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3559extern int __VERIFIER_nondet_int(void) ;
3560#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1769/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3561int ldv_mutex = 1;
3562#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1769/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3563int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )