4305#line 818
4306 LDV_IN_INTERRUPT = 1;
4307 }
4308#line 824
4309 goto switch_break;
4310 switch_default:
4311#line 825
4312 goto switch_break;
4313 } else {
4314 switch_break: ;
4315 }
4316 }
4317 }
4318 }
4319 while_break: ;
4320 }
4321 ldv_module_exit:
4322 {
4323#line 834
4324 ldv_check_final_state();
4325 }
4326#line 837
4327 return;
4328}
4329}
4330#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1060/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4331void ldv_blast_assert(void)
4332{
4333
4334 {
4335 ERROR:
4336#line 6
4337 goto ERROR;
4338}
4339}
4340#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1060/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4341extern int __VERIFIER_nondet_int(void) ;
4342#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1060/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4343int ldv_mutex = 1;
4344#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1060/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4345int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )