1276 goto switch_break;
1277 switch_default:
1278#line 397
1279 goto switch_break;
1280 } else {
1281 switch_break: ;
1282 }
1283 }
1284 }
1285 }
1286 while_break: ;
1287 }
1288 {
1289#line 412
1290 watchdog_exit();
1291 }
1292 ldv_final:
1293 {
1294#line 415
1295 ldv_check_final_state();
1296 }
1297#line 418
1298 return;
1299}
1300}
1301#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
1302void ldv_blast_assert(void)
1303{
1304
1305 {
1306 ERROR:
1307#line 6
1308 goto ERROR;
1309}
1310}
1311#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
1312extern int __VERIFIER_nondet_int(void) ;
1313#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1314int ldv_mutex = 1;
1315#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1316int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )