8428 } else {
8429
8430 }
8431#line 286
8432 goto switch_break;
8433 switch_default:
8434#line 287
8435 goto switch_break;
8436 } else {
8437 switch_break: ;
8438 }
8439 }
8440 }
8441 }
8442 while_break: ;
8443 }
8444 ldv_module_exit:
8445 {
8446#line 296
8447 ldv_check_final_state();
8448 }
8449#line 299
8450 return;
8451}
8452}
8453#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13510/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
8454void ldv_blast_assert(void)
8455{
8456
8457 {
8458 ERROR:
8459#line 6
8460 goto ERROR;
8461}
8462}
8463#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13510/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
8464extern int __VERIFIER_nondet_int(void) ;
8465#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13510/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
8466int ldv_mutex = 1;
8467#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13510/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
8468int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )