9330 goto switch_break;
9331 switch_default:
9332#line 982
9333 goto switch_break;
9334 } else {
9335 switch_break: ;
9336 }
9337 }
9338 }
9339 }
9340 while_break: ;
9341 }
9342 {
9343#line 1002
9344 zram_exit();
9345 }
9346 ldv_final:
9347 {
9348#line 1005
9349 ldv_check_final_state();
9350 }
9351#line 1008
9352 return;
9353}
9354}
9355#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1136/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
9356void ldv_blast_assert(void)
9357{
9358
9359 {
9360 ERROR:
9361#line 6
9362 goto ERROR;
9363}
9364}
9365#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1136/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
9366extern int __VERIFIER_nondet_int(void) ;
9367#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1136/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
9368int ldv_mutex = 1;
9369#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1136/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
9370int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )