6555 goto switch_break;
6556 switch_default:
6557#line 558
6558 goto switch_break;
6559 } else {
6560 switch_break: ;
6561 }
6562 }
6563 }
6564 }
6565 while_break: ;
6566 }
6567 {
6568#line 579
6569 i2c_matroxfb_exit();
6570 }
6571 ldv_final:
6572 {
6573#line 582
6574 ldv_check_final_state();
6575 }
6576#line 585
6577 return;
6578}
6579}
6580#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/17004/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
6581void ldv_blast_assert(void)
6582{
6583
6584 {
6585 ERROR:
6586#line 6
6587 goto ERROR;
6588}
6589}
6590#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/17004/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
6591extern int __VERIFIER_nondet_int(void) ;
6592#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/17004/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6593int ldv_mutex = 1;
6594#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/17004/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6595int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )