10480 {
10481#line 1467
10482 tda9887_set_config(var_group1, var_tda9887_set_config_11_p1);
10483 }
10484#line 1474
10485 goto switch_break;
10486 switch_default:
10487#line 1475
10488 goto switch_break;
10489 } else {
10490 switch_break: ;
10491 }
10492 }
10493 }
10494 }
10495 while_break: ;
10496 }
10497 {
10498#line 1484
10499 ldv_check_final_state();
10500 }
10501#line 1487
10502 return;
10503}
10504}
10505#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14009/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
10506void ldv_blast_assert(void)
10507{
10508
10509 {
10510 ERROR:
10511#line 6
10512 goto ERROR;
10513}
10514}
10515#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14009/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
10516extern int __VERIFIER_nondet_int(void) ;
10517#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14009/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
10518int ldv_mutex = 1;
10519#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14009/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
10520int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )