6863#line 1003
6864 LDV_IN_INTERRUPT = 1;
6865 }
6866#line 1009
6867 goto switch_break;
6868 switch_default:
6869#line 1010
6870 goto switch_break;
6871 } else {
6872 switch_break: ;
6873 }
6874 }
6875 }
6876 }
6877 while_break: ;
6878 }
6879 ldv_module_exit:
6880 {
6881#line 1019
6882 ldv_check_final_state();
6883 }
6884#line 1022
6885 return;
6886}
6887}
6888#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6232/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
6889void ldv_blast_assert(void)
6890{
6891
6892 {
6893 ERROR:
6894#line 6
6895 goto ERROR;
6896}
6897}
6898#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6232/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
6899extern int __VERIFIER_nondet_int(void) ;
6900#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6232/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6901int ldv_mutex = 1;
6902#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6232/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6903int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )