1989 goto switch_break;
1990 switch_default:
1991#line 346
1992 goto switch_break;
1993 } else {
1994 switch_break: ;
1995 }
1996 }
1997 }
1998 }
1999 while_break: ;
2000 }
2001 {
2002#line 358
2003 w1_ds2781_exit();
2004 }
2005 ldv_final:
2006 {
2007#line 361
2008 ldv_check_final_state();
2009 }
2010#line 364
2011 return;
2012}
2013}
2014#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12360/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
2015void ldv_blast_assert(void)
2016{
2017
2018 {
2019 ERROR:
2020#line 6
2021 goto ERROR;
2022}
2023}
2024#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12360/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
2025extern int __VERIFIER_nondet_int(void) ;
2026#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12360/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2027int ldv_mutex = 1;
2028#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12360/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2029int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )