9512 {
9513#line 6219
9514 genmii_read_link(var_group2);
9515 }
9516#line 6242
9517 goto switch_break;
9518 switch_default:
9519#line 6243
9520 goto switch_break;
9521 } else {
9522 switch_break: ;
9523 }
9524 }
9525 }
9526 }
9527 while_break: ;
9528 }
9529 {
9530#line 6252
9531 ldv_check_final_state();
9532 }
9533#line 6255
9534 return;
9535}
9536}
9537#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12129/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
9538void ldv_blast_assert(void)
9539{
9540
9541 {
9542 ERROR:
9543#line 6
9544 goto ERROR;
9545}
9546}
9547#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12129/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
9548extern int __VERIFIER_nondet_int(void) ;
9549#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12129/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
9550int ldv_mutex = 1;
9551#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12129/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
9552int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )