4140 goto switch_break;
4141 switch_default:
4142#line 230
4143 goto switch_break;
4144 } else {
4145 switch_break: ;
4146 }
4147 }
4148 }
4149 }
4150 while_break: ;
4151 }
4152 {
4153#line 246
4154 asus_nb_wmi_exit();
4155 }
4156 ldv_final:
4157 {
4158#line 249
4159 ldv_check_final_state();
4160 }
4161#line 252
4162 return;
4163}
4164}
4165#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5713/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4166void ldv_blast_assert(void)
4167{
4168
4169 {
4170 ERROR:
4171#line 6
4172 goto ERROR;
4173}
4174}
4175#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5713/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4176extern int __VERIFIER_nondet_int(void) ;
4177#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5713/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4178int ldv_mutex = 1;
4179#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5713/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4180int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )