6351 goto switch_break;
6352 switch_default:
6353#line 599
6354 goto switch_break;
6355 } else {
6356 switch_break: ;
6357 }
6358 }
6359 }
6360 }
6361 while_break: ;
6362 }
6363 {
6364#line 615
6365 mtdoops_exit();
6366 }
6367 ldv_final:
6368 {
6369#line 618
6370 ldv_check_final_state();
6371 }
6372#line 621
6373 return;
6374}
6375}
6376#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5642/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
6377void ldv_blast_assert(void)
6378{
6379
6380 {
6381 ERROR:
6382#line 6
6383 goto ERROR;
6384}
6385}
6386#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5642/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
6387extern int __VERIFIER_nondet_int(void) ;
6388#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5642/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6389int ldv_mutex = 1;
6390#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5642/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6391int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )