6364 goto switch_break;
6365 switch_default:
6366#line 387
6367 goto switch_break;
6368 } else {
6369 switch_break: ;
6370 }
6371 }
6372 }
6373 }
6374 while_break: ;
6375 }
6376 {
6377#line 406
6378 icplus_exit();
6379 }
6380 ldv_final:
6381 {
6382#line 409
6383 ldv_check_final_state();
6384 }
6385#line 412
6386 return;
6387}
6388}
6389#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9662/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
6390void ldv_blast_assert(void)
6391{
6392
6393 {
6394 ERROR:
6395#line 6
6396 goto ERROR;
6397}
6398}
6399#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9662/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
6400extern int __VERIFIER_nondet_int(void) ;
6401#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9662/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6402int ldv_mutex = 1;
6403#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9662/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6404int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )