13807#line 2381
13808 adapter->link_duplex = (u16 )65535U;
13809#line 2382
13810 __cil_tmp7 = (enum atl1c_trans_queue )0;
13811#line 2382
13812 atl1c_clean_tx_ring(adapter, __cil_tmp7);
13813#line 2383
13814 __cil_tmp8 = (enum atl1c_trans_queue )1;
13815#line 2383
13816 atl1c_clean_tx_ring(adapter, __cil_tmp8);
13817#line 2384
13818 atl1c_clean_rx_ring(adapter);
13819 }
13820#line 2385
13821 return;
13822}
13823}
13824#line 2942
13825void ldv_check_final_state(void) ;
13826#line 2948
13827extern void ldv_initialize(void) ;
13828#line 2951
13829extern int nondet_int(void) ;
13830#line 2954 "/anthill/stuff/tacas-comp/work/current--X--drivers/net/atl1c/atl1c.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/13/dscv_tempdir/dscv/ri/08_1/drivers/net/atl1c/atl1c_main.c.p"
13831int LDV_IN_INTERRUPT ;
13832#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/net/atl1c/atl1c.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/13/dscv_tempdir/dscv/ri/08_1/kernel-rules/files/engine-blast-assert.h"
13833void ldv_blast_assert(void)
13834{
13835
13836 {
13837 ERROR: ;
13838#line 6
13839 goto ERROR;
13840}
13841}
13842#line 6 "/anthill/stuff/tacas-comp/work/current--X--drivers/net/atl1c/atl1c.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/13/dscv_tempdir/dscv/ri/08_1/kernel-rules/files/engine-blast.h"
13843extern int ldv_undefined_int(void) ;
13844#line 4152 "/anthill/stuff/tacas-comp/work/current--X--drivers/net/atl1c/atl1c.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/13/dscv_tempdir/dscv/ri/08_1/drivers/net/atl1c/atl1c_main.c.p"
13845int ldv_module_refcounter = 1;
13846#line 4155 "/anthill/stuff/tacas-comp/work/current--X--drivers/net/atl1c/atl1c.ko--X--bulklinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/13/dscv_tempdir/dscv/ri/08_1/drivers/net/atl1c/atl1c_main.c.p"
13847void ldv_module_get(struct module *module )