10041 goto switch_break;
10042 switch_default:
10043#line 732
10044 goto switch_break;
10045 } else {
10046 switch_break: ;
10047 }
10048 }
10049 }
10050 }
10051 while_break: ;
10052 }
10053 {
10054#line 746
10055 arcnet_rfc1201_exit();
10056 }
10057 ldv_final:
10058 {
10059#line 749
10060 ldv_check_final_state();
10061 }
10062#line 752
10063 return;
10064}
10065}
10066#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9439/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
10067void ldv_blast_assert(void)
10068{
10069
10070 {
10071 ERROR:
10072#line 6
10073 goto ERROR;
10074}
10075}
10076#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9439/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
10077extern int __VERIFIER_nondet_int(void) ;
10078#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9439/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
10079int ldv_mutex = 1;
10080#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9439/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
10081int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )