11812 {
11813#line 1362
11814 tda8295_i2c_bridge(var_group1, var_tda8295_i2c_bridge_1_p1);
11815 }
11816#line 1375
11817 goto switch_break;
11818 switch_default:
11819#line 1376
11820 goto switch_break;
11821 } else {
11822 switch_break: ;
11823 }
11824 }
11825 }
11826 }
11827 while_break: ;
11828 }
11829 {
11830#line 1385
11831 ldv_check_final_state();
11832 }
11833#line 1388
11834 return;
11835}
11836}
11837#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14008/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
11838void ldv_blast_assert(void)
11839{
11840
11841 {
11842 ERROR:
11843#line 6
11844 goto ERROR;
11845}
11846}
11847#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14008/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
11848extern int __VERIFIER_nondet_int(void) ;
11849#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14008/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
11850int ldv_mutex = 1;
11851#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14008/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
11852int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )