10139 {
10140#line 566
10141 dibusb_i2c_func(var_group1);
10142 }
10143#line 578
10144 goto switch_break;
10145 switch_default:
10146#line 579
10147 goto switch_break;
10148 } else {
10149 switch_break: ;
10150 }
10151 }
10152 }
10153 }
10154 while_break: ;
10155 }
10156 {
10157#line 588
10158 ldv_check_final_state();
10159 }
10160#line 591
10161 return;
10162}
10163}
10164#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13505/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
10165void ldv_blast_assert(void)
10166{
10167
10168 {
10169 ERROR:
10170#line 6
10171 goto ERROR;
10172}
10173}
10174#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13505/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
10175extern int __VERIFIER_nondet_int(void) ;
10176#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13505/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
10177int ldv_mutex = 1;
10178#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13505/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
10179int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )