6492 switch_default:
6493#line 392
6494 goto switch_break;
6495 } else {
6496 switch_break: ;
6497 }
6498 }
6499 }
6500 }
6501 while_break: ;
6502 }
6503 ldv_module_exit:
6504 {
6505#line 407
6506 litelink_sir_cleanup();
6507 }
6508 ldv_final:
6509 {
6510#line 410
6511 ldv_check_final_state();
6512 }
6513#line 413
6514 return;
6515}
6516}
6517#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9304/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
6518void ldv_blast_assert(void)
6519{
6520
6521 {
6522 ERROR:
6523#line 6
6524 goto ERROR;
6525}
6526}
6527#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9304/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
6528extern int __VERIFIER_nondet_int(void) ;
6529#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9304/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6530int ldv_mutex = 1;
6531#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9304/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6532int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )