6077 {
6078#line 681
6079 mt2060_get_if_frequency(var_group1, var_mt2060_get_if_frequency_8_p1);
6080 }
6081#line 688
6082 goto switch_break;
6083 switch_default:
6084#line 689
6085 goto switch_break;
6086 } else {
6087 switch_break: ;
6088 }
6089 }
6090 }
6091 }
6092 while_break: ;
6093 }
6094 {
6095#line 698
6096 ldv_check_final_state();
6097 }
6098#line 701
6099 return;
6100}
6101}
6102#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13997/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
6103void ldv_blast_assert(void)
6104{
6105
6106 {
6107 ERROR:
6108#line 6
6109 goto ERROR;
6110}
6111}
6112#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13997/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
6113extern int __VERIFIER_nondet_int(void) ;
6114#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13997/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6115int ldv_mutex = 1;
6116#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13997/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6117int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )