4177#line 1625
4178 LDV_IN_INTERRUPT = 1;
4179 }
4180#line 1631
4181 goto switch_break;
4182 switch_default:
4183#line 1632
4184 goto switch_break;
4185 } else {
4186 switch_break: ;
4187 }
4188 }
4189 }
4190 }
4191 while_break: ;
4192 }
4193 ldv_module_exit:
4194 {
4195#line 1641
4196 ldv_check_final_state();
4197 }
4198#line 1644
4199 return;
4200}
4201}
4202#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6264/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4203void ldv_blast_assert(void)
4204{
4205
4206 {
4207 ERROR:
4208#line 6
4209 goto ERROR;
4210}
4211}
4212#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6264/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4213extern int __VERIFIER_nondet_int(void) ;
4214#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6264/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4215int ldv_mutex = 1;
4216#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6264/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4217int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )