242 goto switch_default;
243#line 102
244 if (0) {
245 switch_default:
246#line 104
247 goto switch_break;
248 } else {
249 switch_break: ;
250 }
251 }
252 }
253 while_break: ;
254 }
255 {
256#line 116
257 wait_scan_exit();
258 }
259 {
260#line 119
261 ldv_check_final_state();
262 }
263#line 122
264 return;
265}
266}
267#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/977/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
268void ldv_blast_assert(void)
269{
270
271 {
272 ERROR:
273#line 6
274 goto ERROR;
275}
276}
277#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/977/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
278extern int __VERIFIER_nondet_int(void) ;
279#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/977/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
280int ldv_mutex = 1;
281#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/977/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
282int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )