20462 goto switch_break;
20463 switch_default:
20464#line 2563
20465 goto switch_break;
20466 } else {
20467 switch_break: ;
20468 }
20469 }
20470 }
20471 }
20472 while_break: ;
20473 }
20474 {
20475#line 2584
20476 mwifiex_pcie_cleanup_module();
20477 }
20478 ldv_final:
20479 {
20480#line 2587
20481 ldv_check_final_state();
20482 }
20483#line 2590
20484 return;
20485}
20486}
20487#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/10020/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
20488void ldv_blast_assert(void)
20489{
20490
20491 {
20492 ERROR:
20493#line 6
20494 goto ERROR;
20495}
20496}
20497#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/10020/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
20498extern int __VERIFIER_nondet_int(void) ;
20499#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/10020/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
20500int ldv_mutex = 1;
20501#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/10020/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
20502int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )