1302#line 170
1303 if (0) {
1304 switch_default:
1305#line 172
1306 goto switch_break;
1307 } else {
1308 switch_break: ;
1309 }
1310 }
1311 }
1312 while_break: ;
1313 }
1314 {
1315#line 186
1316 pps_ktimer_exit();
1317 }
1318 ldv_final:
1319 {
1320#line 189
1321 ldv_check_final_state();
1322 }
1323#line 192
1324 return;
1325}
1326}
1327#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
1328void ldv_blast_assert(void)
1329{
1330
1331 {
1332 ERROR:
1333#line 6
1334 goto ERROR;
1335}
1336}
1337#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
1338extern int __VERIFIER_nondet_int(void) ;
1339#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1340int ldv_mutex = 1;
1341#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1342int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )