2696#line 419
2697 if (0) {
2698 switch_default:
2699#line 421
2700 goto switch_break;
2701 } else {
2702 switch_break: ;
2703 }
2704 }
2705 }
2706 while_break: ;
2707 }
2708 {
2709#line 444
2710 l4_exit();
2711 }
2712 ldv_final:
2713 {
2714#line 447
2715 ldv_check_final_state();
2716 }
2717#line 450
2718 return;
2719}
2720}
2721#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3960/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
2722void ldv_blast_assert(void)
2723{
2724
2725 {
2726 ERROR:
2727#line 6
2728 goto ERROR;
2729}
2730}
2731#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3960/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
2732extern int __VERIFIER_nondet_int(void) ;
2733#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3960/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2734int ldv_mutex = 1;
2735#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3960/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2736int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )