14581 } else {
14582
14583 }
14584#line 1467
14585 goto switch_break;
14586 switch_default:
14587#line 1468
14588 goto switch_break;
14589 } else {
14590 switch_break: ;
14591 }
14592 }
14593 }
14594 }
14595 while_break: ;
14596 }
14597 ldv_module_exit:
14598 {
14599#line 1477
14600 ldv_check_final_state();
14601 }
14602#line 1480
14603 return;
14604}
14605}
14606#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7657/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
14607void ldv_blast_assert(void)
14608{
14609
14610 {
14611 ERROR:
14612#line 6
14613 goto ERROR;
14614}
14615}
14616#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7657/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
14617extern int __VERIFIER_nondet_int(void) ;
14618#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7657/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
14619int ldv_mutex = 1;
14620#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7657/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
14621int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )