327#line 160
328 if (0) {
329 switch_default:
330#line 162
331 goto switch_break;
332 } else {
333 switch_break: ;
334 }
335 }
336 }
337 while_break: ;
338 }
339 {
340#line 174
341 exit_rc_map_videomate_k100();
342 }
343 ldv_final:
344 {
345#line 177
346 ldv_check_final_state();
347 }
348#line 180
349 return;
350}
351}
352#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12949/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
353void ldv_blast_assert(void)
354{
355
356 {
357 ERROR:
358#line 6
359 goto ERROR;
360}
361}
362#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12949/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
363extern int __VERIFIER_nondet_int(void) ;
364#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12949/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
365int ldv_mutex = 1;
366#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12949/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
367int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )