12702 } else {
12703
12704 }
12705#line 1507
12706 goto switch_break;
12707 switch_default:
12708#line 1508
12709 goto switch_break;
12710 } else {
12711 switch_break: ;
12712 }
12713 }
12714 }
12715 }
12716 while_break: ;
12717 }
12718 ldv_module_exit:
12719 {
12720#line 1517
12721 ldv_check_final_state();
12722 }
12723#line 1520
12724 return;
12725}
12726}
12727#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13516/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
12728void ldv_blast_assert(void)
12729{
12730
12731 {
12732 ERROR:
12733#line 6
12734 goto ERROR;
12735}
12736}
12737#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13516/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
12738extern int __VERIFIER_nondet_int(void) ;
12739#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13516/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
12740int ldv_mutex = 1;
12741#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13516/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
12742int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )