2044 goto switch_break;
2045 switch_default:
2046#line 518
2047 goto switch_break;
2048 } else {
2049 switch_break: ;
2050 }
2051 }
2052 }
2053 }
2054 while_break: ;
2055 }
2056 {
2057#line 543
2058 cleanup_sbc_gxx();
2059 }
2060 ldv_final:
2061 {
2062#line 546
2063 ldv_check_final_state();
2064 }
2065#line 549
2066 return;
2067}
2068}
2069#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5452/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
2070void ldv_blast_assert(void)
2071{
2072
2073 {
2074 ERROR:
2075#line 6
2076 goto ERROR;
2077}
2078}
2079#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5452/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
2080extern int __VERIFIER_nondet_int(void) ;
2081#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5452/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2082int ldv_mutex = 1;
2083#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5452/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2084int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )