1497 goto switch_break;
1498 switch_default:
1499#line 273
1500 goto switch_break;
1501 } else {
1502 switch_break: ;
1503 }
1504 }
1505 }
1506 }
1507 while_break: ;
1508 }
1509 {
1510#line 288
1511 w1_bq27000_exit();
1512 }
1513 ldv_final:
1514 {
1515#line 291
1516 ldv_check_final_state();
1517 }
1518#line 294
1519 return;
1520}
1521}
1522#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
1523void ldv_blast_assert(void)
1524{
1525
1526 {
1527 ERROR:
1528#line 6
1529 goto ERROR;
1530}
1531}
1532#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
1533extern int __VERIFIER_nondet_int(void) ;
1534#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1535int ldv_mutex = 1;
1536#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1537int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )