304#line 138
305 if (0) {
306 switch_default:
307#line 140
308 goto switch_break;
309 } else {
310 switch_break: ;
311 }
312 }
313 }
314 while_break: ;
315 }
316 {
317#line 152
318 exit_rc_map_flyvideo();
319 }
320 ldv_final:
321 {
322#line 155
323 ldv_check_final_state();
324 }
325#line 158
326 return;
327}
328}
329#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12894/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
330void ldv_blast_assert(void)
331{
332
333 {
334 ERROR:
335#line 6
336 goto ERROR;
337}
338}
339#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12894/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
340extern int __VERIFIER_nondet_int(void) ;
341#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12894/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
342int ldv_mutex = 1;
343#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12894/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
344int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )