12792 {
12793#line 1520
12794 get_bandwidth(var_group1, var_get_bandwidth_28_p1);
12795 }
12796#line 1527
12797 goto switch_break;
12798 switch_default:
12799#line 1528
12800 goto switch_break;
12801 } else {
12802 switch_break: ;
12803 }
12804 }
12805 }
12806 }
12807 while_break: ;
12808 }
12809 {
12810#line 1537
12811 ldv_check_final_state();
12812 }
12813#line 1540
12814 return;
12815}
12816}
12817#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13417/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
12818void ldv_blast_assert(void)
12819{
12820
12821 {
12822 ERROR:
12823#line 6
12824 goto ERROR;
12825}
12826}
12827#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13417/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
12828extern int __VERIFIER_nondet_int(void) ;
12829#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13417/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
12830int ldv_mutex = 1;
12831#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13417/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
12832int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )