1148#line 137
1149 if (0) {
1150 switch_default:
1151#line 139
1152 goto switch_break;
1153 } else {
1154 switch_break: ;
1155 }
1156 }
1157 }
1158 while_break: ;
1159 }
1160 {
1161#line 151
1162 w1_smem_fini();
1163 }
1164 ldv_final:
1165 {
1166#line 154
1167 ldv_check_final_state();
1168 }
1169#line 157
1170 return;
1171}
1172}
1173#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12361/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
1174void ldv_blast_assert(void)
1175{
1176
1177 {
1178 ERROR:
1179#line 6
1180 goto ERROR;
1181}
1182}
1183#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12361/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
1184extern int __VERIFIER_nondet_int(void) ;
1185#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12361/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1186int ldv_mutex = 1;
1187#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12361/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1188int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )