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