6169 switch_default:
6170#line 599
6171 goto switch_break;
6172 } else {
6173 switch_break: ;
6174 }
6175 }
6176 }
6177 }
6178 while_break: ;
6179 }
6180 ldv_module_exit:
6181 {
6182#line 621
6183 lxt_exit();
6184 }
6185 ldv_final:
6186 {
6187#line 624
6188 ldv_check_final_state();
6189 }
6190#line 627
6191 return;
6192}
6193}
6194#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9663/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
6195void ldv_blast_assert(void)
6196{
6197
6198 {
6199 ERROR:
6200#line 6
6201 goto ERROR;
6202}
6203}
6204#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9663/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
6205extern int __VERIFIER_nondet_int(void) ;
6206#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9663/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6207int ldv_mutex = 1;
6208#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9663/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6209int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )