5081#line 673
5082 if (0) {
5083 switch_default:
5084#line 675
5085 goto switch_break;
5086 } else {
5087 switch_break: ;
5088 }
5089 }
5090 }
5091 while_break: ;
5092 }
5093 {
5094#line 729
5095 onenand_sim_exit();
5096 }
5097 ldv_final:
5098 {
5099#line 732
5100 ldv_check_final_state();
5101 }
5102#line 735
5103 return;
5104}
5105}
5106#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
5107void ldv_blast_assert(void)
5108{
5109
5110 {
5111 ERROR:
5112#line 6
5113 goto ERROR;
5114}
5115}
5116#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
5117extern int __VERIFIER_nondet_int(void) ;
5118#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5119int ldv_mutex = 1;
5120#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5462/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5121int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )