5370#line 597
5371 if (0) {
5372 switch_default:
5373#line 599
5374 goto switch_break;
5375 } else {
5376 switch_break: ;
5377 }
5378 }
5379 }
5380 while_break: ;
5381 }
5382 {
5383#line 613
5384 mtd_subpagetest_exit();
5385 }
5386 ldv_final:
5387 {
5388#line 616
5389 ldv_check_final_state();
5390 }
5391#line 619
5392 return;
5393}
5394}
5395#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5477/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
5396void ldv_blast_assert(void)
5397{
5398
5399 {
5400 ERROR:
5401#line 6
5402 goto ERROR;
5403}
5404}
5405#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5477/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
5406extern int __VERIFIER_nondet_int(void) ;
5407#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5477/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5408int ldv_mutex = 1;
5409#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5477/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5410int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )