4485 goto switch_break;
4486 switch_default:
4487#line 2933
4488 goto switch_break;
4489 } else {
4490 switch_break: ;
4491 }
4492 }
4493 }
4494 }
4495 while_break: ;
4496 }
4497 {
4498#line 3015
4499 bsdcomp_cleanup();
4500 }
4501 ldv_final:
4502 {
4503#line 3018
4504 ldv_check_final_state();
4505 }
4506#line 3021
4507 return;
4508}
4509}
4510#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4511void ldv_blast_assert(void)
4512{
4513
4514 {
4515 ERROR:
4516#line 6
4517 goto ERROR;
4518}
4519}
4520#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4521extern int __VERIFIER_nondet_int(void) ;
4522#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4523int ldv_mutex = 1;
4524#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9568/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4525int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )