4058 goto switch_break;
4059 switch_default:
4060#line 379
4061 goto switch_break;
4062 } else {
4063 switch_break: ;
4064 }
4065 }
4066 }
4067 }
4068 while_break: ;
4069 }
4070 {
4071#line 403
4072 dell_led_exit();
4073 }
4074 ldv_final:
4075 {
4076#line 406
4077 ldv_check_final_state();
4078 }
4079#line 409
4080 return;
4081}
4082}
4083#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12593/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4084void ldv_blast_assert(void)
4085{
4086
4087 {
4088 ERROR:
4089#line 6
4090 goto ERROR;
4091}
4092}
4093#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12593/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4094extern int __VERIFIER_nondet_int(void) ;
4095#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12593/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4096int ldv_mutex = 1;
4097#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12593/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4098int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )