1475#line 212
1476 if (0) {
1477 switch_default:
1478#line 214
1479 goto switch_break;
1480 } else {
1481 switch_break: ;
1482 }
1483 }
1484 }
1485 while_break: ;
1486 }
1487 {
1488#line 231
1489 cleanup_netsc520();
1490 }
1491 ldv_final:
1492 {
1493#line 234
1494 ldv_check_final_state();
1495 }
1496#line 237
1497 return;
1498}
1499}
1500#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5446/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
1501void ldv_blast_assert(void)
1502{
1503
1504 {
1505 ERROR:
1506#line 6
1507 goto ERROR;
1508}
1509}
1510#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5446/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
1511extern int __VERIFIER_nondet_int(void) ;
1512#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5446/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1513int ldv_mutex = 1;
1514#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5446/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1515int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )