2932#line 353
2933 if (0) {
2934 switch_default:
2935#line 355
2936 goto switch_break;
2937 } else {
2938 switch_break: ;
2939 }
2940 }
2941 }
2942 while_break: ;
2943 }
2944 {
2945#line 367
2946 xp_exit();
2947 }
2948 ldv_final:
2949 {
2950#line 370
2951 ldv_check_final_state();
2952 }
2953#line 373
2954 return;
2955}
2956}
2957#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4757/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
2958void ldv_blast_assert(void)
2959{
2960
2961 {
2962 ERROR:
2963#line 6
2964 goto ERROR;
2965}
2966}
2967#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4757/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
2968extern int __VERIFIER_nondet_int(void) ;
2969#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4757/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2970int ldv_mutex = 1;
2971#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4757/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2972int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )