8914 goto switch_break;
8915 switch_default:
8916#line 1992
8917 goto switch_break;
8918 } else {
8919 switch_break: ;
8920 }
8921 }
8922 }
8923 }
8924 while_break: ;
8925 }
8926 {
8927#line 2042
8928 gsmi_exit();
8929 }
8930 ldv_final:
8931 {
8932#line 2045
8933 ldv_check_final_state();
8934 }
8935#line 2048
8936 return;
8937}
8938}
8939#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6152/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
8940void ldv_blast_assert(void)
8941{
8942
8943 {
8944 ERROR:
8945#line 6
8946 goto ERROR;
8947}
8948}
8949#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6152/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
8950extern int __VERIFIER_nondet_int(void) ;
8951#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6152/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
8952int ldv_mutex = 1;
8953#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6152/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
8954int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )