2856 goto switch_break;
2857 switch_default:
2858#line 216
2859 goto switch_break;
2860 } else {
2861 switch_break: ;
2862 }
2863 }
2864 }
2865 }
2866 while_break: ;
2867 }
2868 {
2869#line 231
2870 mr_exit();
2871 }
2872 ldv_final:
2873 {
2874#line 234
2875 ldv_check_final_state();
2876 }
2877#line 237
2878 return;
2879}
2880}
2881#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/207/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
2882void ldv_blast_assert(void)
2883{
2884
2885 {
2886 ERROR:
2887#line 6
2888 goto ERROR;
2889}
2890}
2891#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/207/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
2892extern int __VERIFIER_nondet_int(void) ;
2893#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/207/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2894int ldv_mutex = 1;
2895#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/207/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2896int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )