3818#line 262
3819 dac124s085_remove(var_group1);
3820 }
3821#line 269
3822 goto switch_break;
3823 switch_default:
3824#line 270
3825 goto switch_break;
3826 } else {
3827 switch_break: ;
3828 }
3829 }
3830 }
3831 }
3832 while_break: ;
3833 }
3834 ldv_module_exit:
3835 {
3836#line 279
3837 ldv_check_final_state();
3838 }
3839#line 282
3840 return;
3841}
3842}
3843#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12597/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3844void ldv_blast_assert(void)
3845{
3846
3847 {
3848 ERROR:
3849#line 6
3850 goto ERROR;
3851}
3852}
3853#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12597/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3854extern int __VERIFIER_nondet_int(void) ;
3855#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12597/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3856int ldv_mutex = 1;
3857#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12597/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3858int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )