4331 switch_default:
4332#line 270
4333 goto switch_break;
4334 } else {
4335 switch_break: ;
4336 }
4337 }
4338 }
4339 }
4340 while_break: ;
4341 }
4342 ldv_module_exit:
4343 {
4344#line 287
4345 divadidd_exit();
4346 }
4347 ldv_final:
4348 {
4349#line 290
4350 ldv_check_final_state();
4351 }
4352#line 293
4353 return;
4354}
4355}
4356#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3441/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4357void ldv_blast_assert(void)
4358{
4359
4360 {
4361 ERROR:
4362#line 6
4363 goto ERROR;
4364}
4365}
4366#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3441/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4367extern int __VERIFIER_nondet_int(void) ;
4368#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3441/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4369int ldv_mutex = 1;
4370#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3441/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4371int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )