5701 goto switch_break;
5702 switch_default:
5703#line 463
5704 goto switch_break;
5705 } else {
5706 switch_break: ;
5707 }
5708 }
5709 }
5710 }
5711 while_break: ;
5712 }
5713 {
5714#line 481
5715 apanel_cleanup();
5716 }
5717 ldv_final:
5718 {
5719#line 484
5720 ldv_check_final_state();
5721 }
5722#line 487
5723 return;
5724}
5725}
5726#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4001/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
5727void ldv_blast_assert(void)
5728{
5729
5730 {
5731 ERROR:
5732#line 6
5733 goto ERROR;
5734}
5735}
5736#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4001/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
5737extern int __VERIFIER_nondet_int(void) ;
5738#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4001/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5739int ldv_mutex = 1;
5740#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4001/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5741int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )