15606 switch_default:
15607#line 1443
15608 goto switch_break;
15609 } else {
15610 switch_break: ;
15611 }
15612 }
15613 }
15614 }
15615 while_break: ;
15616 }
15617 ldv_module_exit:
15618 {
15619#line 1463
15620 dvb_bt8xx_exit();
15621 }
15622 ldv_final:
15623 {
15624#line 1466
15625 ldv_check_final_state();
15626 }
15627#line 1469
15628 return;
15629}
15630}
15631#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13577/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
15632void ldv_blast_assert(void)
15633{
15634
15635 {
15636 ERROR:
15637#line 6
15638 goto ERROR;
15639}
15640}
15641#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13577/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
15642extern int __VERIFIER_nondet_int(void) ;
15643#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13577/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
15644int ldv_mutex = 1;
15645#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13577/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
15646int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )