708#line 219
709 if (0) {
710 switch_default:
711#line 221
712 goto switch_break;
713 } else {
714 switch_break: ;
715 }
716 }
717 }
718 while_break: ;
719 }
720 {
721#line 237
722 dummy_exit();
723 }
724 ldv_final:
725 {
726#line 240
727 ldv_check_final_state();
728 }
729#line 243
730 return;
731}
732}
733#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
734void ldv_blast_assert(void)
735{
736
737 {
738 ERROR:
739#line 6
740 goto ERROR;
741}
742}
743#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
744extern int __VERIFIER_nondet_int(void) ;
745#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
746int ldv_mutex = 1;
747#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
748int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )