13072 {
13073#line 1345
13074 dib3000mb_read_unc_blocks(var_group1, var_dib3000mb_read_unc_blocks_10_p1);
13075 }
13076#line 1352
13077 goto switch_break;
13078 switch_default:
13079#line 1353
13080 goto switch_break;
13081 } else {
13082 switch_break: ;
13083 }
13084 }
13085 }
13086 }
13087 while_break: ;
13088 }
13089 {
13090#line 1362
13091 ldv_check_final_state();
13092 }
13093#line 1365
13094 return;
13095}
13096}
13097#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13359/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
13098void ldv_blast_assert(void)
13099{
13100
13101 {
13102 ERROR:
13103#line 6
13104 goto ERROR;
13105}
13106}
13107#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13359/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
13108extern int __VERIFIER_nondet_int(void) ;
13109#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13359/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
13110int ldv_mutex = 1;
13111#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13359/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
13112int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )