11681 switch_default:
11682#line 2316
11683 goto switch_break;
11684 } else {
11685 switch_break: ;
11686 }
11687 }
11688 }
11689 }
11690 while_break: ;
11691 }
11692 ldv_module_exit:
11693 {
11694#line 2387
11695 atk0110_exit();
11696 }
11697 ldv_final:
11698 {
11699#line 2390
11700 ldv_check_final_state();
11701 }
11702#line 2393
11703 return;
11704}
11705}
11706#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6030/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
11707void ldv_blast_assert(void)
11708{
11709
11710 {
11711 ERROR:
11712#line 6
11713 goto ERROR;
11714}
11715}
11716#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6030/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
11717extern int __VERIFIER_nondet_int(void) ;
11718#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6030/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
11719int ldv_mutex = 1;
11720#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6030/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
11721int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )