14754 {
14755#line 1539
14756 it913x_fe_read_ucblocks(var_group1, var_it913x_fe_read_ucblocks_12_p1);
14757 }
14758#line 1546
14759 goto switch_break;
14760 switch_default:
14761#line 1547
14762 goto switch_break;
14763 } else {
14764 switch_break: ;
14765 }
14766 }
14767 }
14768 }
14769 while_break: ;
14770 }
14771 {
14772#line 1556
14773 ldv_check_final_state();
14774 }
14775#line 1559
14776 return;
14777}
14778}
14779#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13374/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
14780void ldv_blast_assert(void)
14781{
14782
14783 {
14784 ERROR:
14785#line 6
14786 goto ERROR;
14787}
14788}
14789#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13374/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
14790extern int __VERIFIER_nondet_int(void) ;
14791#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13374/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
14792int ldv_mutex = 1;
14793#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13374/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
14794int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )