1918#line 307
1919 tmp___1 = __VERIFIER_nondet_int();
1920 }
1921#line 307
1922 if (tmp___1 != 0) {
1923#line 308
1924 goto ldv_15699;
1925 } else {
1926#line 310
1927 goto ldv_15701;
1928 }
1929 ldv_15701: ;
1930 {
1931#line 372
1932 w1_ds2781_exit();
1933 }
1934 ldv_final:
1935 {
1936#line 375
1937 ldv_check_final_state();
1938 }
1939#line 378
1940 return;
1941}
1942}
1943#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4914/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1944void ldv_blast_assert(void)
1945{
1946
1947 {
1948 ERROR: ;
1949#line 6
1950 goto ERROR;
1951}
1952}
1953#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4914/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1954extern int __VERIFIER_nondet_int(void) ;
1955#line 399 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4914/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2781.c.p"
1956int ldv_spin = 0;
1957#line 403 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4914/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2781.c.p"
1958void ldv_check_alloc_flags(gfp_t flags )