3223 } else {
3224
3225 }
3226#line 481
3227 goto switch_break;
3228 switch_default:
3229#line 482
3230 goto switch_break;
3231 } else {
3232 switch_break: ;
3233 }
3234 }
3235 }
3236 }
3237 while_break: ;
3238 }
3239 ldv_module_exit:
3240 {
3241#line 491
3242 ldv_check_final_state();
3243 }
3244#line 494
3245 return;
3246}
3247}
3248#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5877/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3249void ldv_blast_assert(void)
3250{
3251
3252 {
3253 ERROR:
3254#line 6
3255 goto ERROR;
3256}
3257}
3258#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5877/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3259extern int __VERIFIER_nondet_int(void) ;
3260#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5877/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3261int ldv_mutex = 1;
3262#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5877/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3263int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )