2586 } else {
2587
2588 }
2589#line 334
2590 goto switch_break;
2591 switch_default:
2592#line 335
2593 goto switch_break;
2594 } else {
2595 switch_break: ;
2596 }
2597 }
2598 }
2599 }
2600 while_break: ;
2601 }
2602 ldv_module_exit:
2603 {
2604#line 344
2605 ldv_check_final_state();
2606 }
2607#line 347
2608 return;
2609}
2610}
2611#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
2612void ldv_blast_assert(void)
2613{
2614
2615 {
2616 ERROR:
2617#line 6
2618 goto ERROR;
2619}
2620}
2621#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
2622extern int __VERIFIER_nondet_int(void) ;
2623#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2624int ldv_mutex = 1;
2625#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2626int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )