6188 goto switch_break;
6189 switch_default:
6190#line 907
6191 goto switch_break;
6192 } else {
6193 switch_break: ;
6194 }
6195 }
6196 }
6197 }
6198 while_break: ;
6199 }
6200 {
6201#line 934
6202 intel_menlow_module_exit();
6203 }
6204 ldv_final:
6205 {
6206#line 937
6207 ldv_check_final_state();
6208 }
6209#line 940
6210 return;
6211}
6212}
6213#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5730/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
6214void ldv_blast_assert(void)
6215{
6216
6217 {
6218 ERROR:
6219#line 6
6220 goto ERROR;
6221}
6222}
6223#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5730/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
6224extern int __VERIFIER_nondet_int(void) ;
6225#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5730/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6226int ldv_mutex = 1;
6227#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5730/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6228int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )