4375#line 223
4376 if (0) {
4377 switch_default:
4378#line 225
4379 goto switch_break;
4380 } else {
4381 switch_break: ;
4382 }
4383 }
4384 }
4385 while_break: ;
4386 }
4387 {
4388#line 240
4389 pps_tty_cleanup();
4390 }
4391 ldv_final:
4392 {
4393#line 243
4394 ldv_check_final_state();
4395 }
4396#line 246
4397 return;
4398}
4399}
4400#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4610/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4401void ldv_blast_assert(void)
4402{
4403
4404 {
4405 ERROR:
4406#line 6
4407 goto ERROR;
4408}
4409}
4410#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4610/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4411extern int __VERIFIER_nondet_int(void) ;
4412#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4610/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4413int ldv_mutex = 1;
4414#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4610/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4415int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )