4101#line 548
4102 LDV_IN_INTERRUPT = 1;
4103 }
4104#line 554
4105 goto switch_break;
4106 switch_default:
4107#line 555
4108 goto switch_break;
4109 } else {
4110 switch_break: ;
4111 }
4112 }
4113 }
4114 }
4115 while_break: ;
4116 }
4117 ldv_module_exit:
4118 {
4119#line 564
4120 ldv_check_final_state();
4121 }
4122#line 567
4123 return;
4124}
4125}
4126#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6222/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4127void ldv_blast_assert(void)
4128{
4129
4130 {
4131 ERROR:
4132#line 6
4133 goto ERROR;
4134}
4135}
4136#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6222/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4137extern int __VERIFIER_nondet_int(void) ;
4138#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6222/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4139int ldv_mutex = 1;
4140#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6222/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4141int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )