6628#line 234
6629 tmp___1 = nondet_int();
6630 }
6631#line 234
6632 if (tmp___1 != 0) {
6633#line 235
6634 goto ldv_38480;
6635 } else {
6636#line 237
6637 goto ldv_38482;
6638 }
6639 ldv_38482:
6640 {
6641#line 267
6642 pppox_exit();
6643 }
6644 ldv_final:
6645 {
6646#line 270
6647 ldv_check_final_state();
6648 }
6649#line 273
6650 return;
6651}
6652}
6653#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/net/pppox.ko--X--aerrlinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/kernel-rules/files/engine-blast-assert.h"
6654void ldv_blast_assert(void)
6655{
6656
6657 {
6658 ERROR: ;
6659#line 6
6660 goto ERROR;
6661}
6662}
6663#line 6 "/anthill/stuff/tacas-comp/work/current--X--drivers/net/pppox.ko--X--aerrlinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/kernel-rules/files/engine-blast.h"
6664extern int ldv_undefined_int(void) ;
6665#line 290 "/anthill/stuff/tacas-comp/work/current--X--drivers/net/pppox.ko--X--aerrlinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/net/pppox.c.p"
6666int ldv_module_refcounter = 1;
6667#line 293 "/anthill/stuff/tacas-comp/work/current--X--drivers/net/pppox.ko--X--aerrlinux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/11/dscv_tempdir/dscv/ri/08_1/drivers/net/pppox.c.p"
6668void ldv_module_get(struct module *module )