1175 goto switch_break;
1176 switch_default:
1177#line 278
1178 goto switch_break;
1179 } else {
1180 switch_break: ;
1181 }
1182 }
1183 }
1184 }
1185 while_break: ;
1186 }
1187 {
1188#line 293
1189 memconsole_exit();
1190 }
1191 ldv_final:
1192 {
1193#line 296
1194 ldv_check_final_state();
1195 }
1196#line 299
1197 return;
1198}
1199}
1200#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
1201void ldv_blast_assert(void)
1202{
1203
1204 {
1205 ERROR:
1206#line 6
1207 goto ERROR;
1208}
1209}
1210#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
1211extern int __VERIFIER_nondet_int(void) ;
1212#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1213int ldv_mutex = 1;
1214#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1215int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )