20764 goto switch_break;
20765 switch_default:
20766#line 1279
20767 goto switch_break;
20768 } else {
20769 switch_break: ;
20770 }
20771 }
20772 }
20773 }
20774 while_break: ;
20775 }
20776 {
20777#line 1296
20778 em28xx_dvb_unregister();
20779 }
20780 ldv_final:
20781 {
20782#line 1299
20783 ldv_check_final_state();
20784 }
20785#line 1302
20786 return;
20787}
20788}
20789#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14505/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
20790void ldv_blast_assert(void)
20791{
20792
20793 {
20794 ERROR:
20795#line 6
20796 goto ERROR;
20797}
20798}
20799#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14505/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
20800extern int __VERIFIER_nondet_int(void) ;
20801#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14505/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
20802int ldv_mutex = 1;
20803#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14505/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
20804int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )