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