5869 {
5870#line 671
5871 mt2266_get_bandwidth(var_group1, var_mt2266_get_bandwidth_6_p1);
5872 }
5873#line 678
5874 goto switch_break;
5875 switch_default:
5876#line 679
5877 goto switch_break;
5878 } else {
5879 switch_break: ;
5880 }
5881 }
5882 }
5883 }
5884 while_break: ;
5885 }
5886 {
5887#line 688
5888 ldv_check_final_state();
5889 }
5890#line 691
5891 return;
5892}
5893}
5894#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14001/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
5895void ldv_blast_assert(void)
5896{
5897
5898 {
5899 ERROR:
5900#line 6
5901 goto ERROR;
5902}
5903}
5904#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14001/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
5905extern int __VERIFIER_nondet_int(void) ;
5906#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14001/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5907int ldv_mutex = 1;
5908#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14001/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5909int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )