5751 goto switch_break;
5752 switch_default:
5753#line 1332
5754 goto switch_break;
5755 } else {
5756 switch_break: ;
5757 }
5758 }
5759 }
5760 }
5761 while_break: ;
5762 }
5763 {
5764#line 1357
5765 ppp_mppe_cleanup();
5766 }
5767 ldv_final:
5768 {
5769#line 1360
5770 ldv_check_final_state();
5771 }
5772#line 1363
5773 return;
5774}
5775}
5776#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9572/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
5777void ldv_blast_assert(void)
5778{
5779
5780 {
5781 ERROR:
5782#line 6
5783 goto ERROR;
5784}
5785}
5786#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9572/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
5787extern int __VERIFIER_nondet_int(void) ;
5788#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9572/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5789int ldv_mutex = 1;
5790#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9572/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5791int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )