2969 switch_default:
2970#line 261
2971 goto switch_break;
2972 } else {
2973 switch_break: ;
2974 }
2975 }
2976 }
2977 }
2978 while_break: ;
2979 }
2980 ldv_module_exit:
2981 {
2982#line 273
2983 px_exit();
2984 }
2985 ldv_final:
2986 {
2987#line 276
2988 ldv_check_final_state();
2989 }
2990#line 279
2991 return;
2992}
2993}
2994#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/214/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
2995void ldv_blast_assert(void)
2996{
2997
2998 {
2999 ERROR:
3000#line 6
3001 goto ERROR;
3002}
3003}
3004#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/214/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3005extern int __VERIFIER_nondet_int(void) ;
3006#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/214/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3007int ldv_mutex = 1;
3008#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/214/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3009int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )