2819 } else {
2820
2821 }
2822#line 498
2823 goto switch_break;
2824 switch_default:
2825#line 499
2826 goto switch_break;
2827 } else {
2828 switch_break: ;
2829 }
2830 }
2831 }
2832 }
2833 while_break: ;
2834 }
2835 ldv_module_exit:
2836 {
2837#line 508
2838 ldv_check_final_state();
2839 }
2840#line 511
2841 return;
2842}
2843}
2844#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16432/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
2845void ldv_blast_assert(void)
2846{
2847
2848 {
2849 ERROR:
2850#line 6
2851 goto ERROR;
2852}
2853}
2854#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16432/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
2855extern int __VERIFIER_nondet_int(void) ;
2856#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16432/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2857int ldv_mutex = 1;
2858#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16432/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2859int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )