10210 } else {
10211
10212 }
10213#line 1169
10214 goto switch_break;
10215 switch_default:
10216#line 1170
10217 goto switch_break;
10218 } else {
10219 switch_break: ;
10220 }
10221 }
10222 }
10223 }
10224 while_break: ;
10225 }
10226 ldv_module_exit:
10227 {
10228#line 1179
10229 ldv_check_final_state();
10230 }
10231#line 1182
10232 return;
10233}
10234}
10235#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7668/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
10236void ldv_blast_assert(void)
10237{
10238
10239 {
10240 ERROR:
10241#line 6
10242 goto ERROR;
10243}
10244}
10245#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7668/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
10246extern int __VERIFIER_nondet_int(void) ;
10247#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7668/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
10248int ldv_mutex = 1;
10249#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7668/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
10250int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )