4260 switch_default:
4261#line 348
4262 goto switch_break;
4263 } else {
4264 switch_break: ;
4265 }
4266 }
4267 }
4268 }
4269 while_break: ;
4270 }
4271 ldv_module_exit:
4272 {
4273#line 360
4274 exit_teles_cs();
4275 }
4276 ldv_final:
4277 {
4278#line 363
4279 ldv_check_final_state();
4280 }
4281#line 366
4282 return;
4283}
4284}
4285#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3640/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4286void ldv_blast_assert(void)
4287{
4288
4289 {
4290 ERROR:
4291#line 6
4292 goto ERROR;
4293}
4294}
4295#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3640/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4296extern int __VERIFIER_nondet_int(void) ;
4297#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3640/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4298int ldv_mutex = 1;
4299#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3640/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4300int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )