4029 switch_default:
4030#line 273
4031 goto switch_break;
4032 } else {
4033 switch_break: ;
4034 }
4035 }
4036 }
4037 }
4038 while_break: ;
4039 }
4040 ldv_module_exit:
4041 {
4042#line 285
4043 exit_avma1_cs();
4044 }
4045 ldv_final:
4046 {
4047#line 288
4048 ldv_check_final_state();
4049 }
4050#line 291
4051 return;
4052}
4053}
4054#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3633/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4055void ldv_blast_assert(void)
4056{
4057
4058 {
4059 ERROR:
4060#line 6
4061 goto ERROR;
4062}
4063}
4064#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3633/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4065extern int __VERIFIER_nondet_int(void) ;
4066#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3633/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4067int ldv_mutex = 1;
4068#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3633/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4069int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )