8437 goto switch_break;
8438 switch_default:
8439#line 1217
8440 goto switch_break;
8441 } else {
8442 switch_break: ;
8443 }
8444 }
8445 }
8446 }
8447 while_break: ;
8448 }
8449 {
8450#line 1235
8451 cleanup_inftl();
8452 }
8453 ldv_final:
8454 {
8455#line 1238
8456 ldv_check_final_state();
8457 }
8458#line 1241
8459 return;
8460}
8461}
8462#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5496/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
8463void ldv_blast_assert(void)
8464{
8465
8466 {
8467 ERROR:
8468#line 6
8469 goto ERROR;
8470}
8471}
8472#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5496/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
8473extern int __VERIFIER_nondet_int(void) ;
8474#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5496/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
8475int ldv_mutex = 1;
8476#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5496/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
8477int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )