5078#line 426
5079 if (0) {
5080 switch_default:
5081#line 428
5082 goto switch_break;
5083 } else {
5084 switch_break: ;
5085 }
5086 }
5087 }
5088 while_break: ;
5089 }
5090 {
5091#line 453
5092 cleanup_slram();
5093 }
5094 ldv_final:
5095 {
5096#line 456
5097 ldv_check_final_state();
5098 }
5099#line 459
5100 return;
5101}
5102}
5103#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5416/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
5104void ldv_blast_assert(void)
5105{
5106
5107 {
5108 ERROR:
5109#line 6
5110 goto ERROR;
5111}
5112}
5113#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5416/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
5114extern int __VERIFIER_nondet_int(void) ;
5115#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5416/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5116int ldv_mutex = 1;
5117#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5416/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5118int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )