2494 switch_default:
2495#line 446
2496 goto switch_break;
2497 } else {
2498 switch_break: ;
2499 }
2500 }
2501 }
2502 }
2503 while_break: ;
2504 }
2505 ldv_module_exit:
2506 {
2507#line 470
2508 ct82c710_exit();
2509 }
2510 ldv_final:
2511 {
2512#line 473
2513 ldv_check_final_state();
2514 }
2515#line 476
2516 return;
2517}
2518}
2519#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
2520void ldv_blast_assert(void)
2521{
2522
2523 {
2524 ERROR:
2525#line 6
2526 goto ERROR;
2527}
2528}
2529#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
2530extern int __VERIFIER_nondet_int(void) ;
2531#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2532int ldv_mutex = 1;
2533#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4212/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2534int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )