4270#line 243
4271 if (0) {
4272 switch_default:
4273#line 245
4274 goto switch_break;
4275 } else {
4276 switch_break: ;
4277 }
4278 }
4279 }
4280 while_break: ;
4281 }
4282 {
4283#line 261
4284 dell_wmi_aio_exit();
4285 }
4286 ldv_final:
4287 {
4288#line 264
4289 ldv_check_final_state();
4290 }
4291#line 267
4292 return;
4293}
4294}
4295#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5718/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4296void ldv_blast_assert(void)
4297{
4298
4299 {
4300 ERROR:
4301#line 6
4302 goto ERROR;
4303}
4304}
4305#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5718/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4306extern int __VERIFIER_nondet_int(void) ;
4307#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5718/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4308int ldv_mutex = 1;
4309#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5718/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4310int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )