6518 {
6519#line 496
6520 tda18218_get_if_frequency(var_group1, var_tda18218_get_if_frequency_5_p1);
6521 }
6522#line 503
6523 goto switch_break;
6524 switch_default:
6525#line 504
6526 goto switch_break;
6527 } else {
6528 switch_break: ;
6529 }
6530 }
6531 }
6532 }
6533 while_break: ;
6534 }
6535 {
6536#line 513
6537 ldv_check_final_state();
6538 }
6539#line 516
6540 return;
6541}
6542}
6543#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14006/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
6544void ldv_blast_assert(void)
6545{
6546
6547 {
6548 ERROR:
6549#line 6
6550 goto ERROR;
6551}
6552}
6553#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14006/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
6554extern int __VERIFIER_nondet_int(void) ;
6555#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14006/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6556int ldv_mutex = 1;
6557#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14006/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6558int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )