1934#line 310
1935 tmp___1 = __VERIFIER_nondet_int();
1936 }
1937#line 310
1938 if (tmp___1 != 0) {
1939#line 311
1940 goto ldv_15703;
1941 } else {
1942#line 313
1943 goto ldv_15705;
1944 }
1945 ldv_15705: ;
1946 {
1947#line 375
1948 w1_ds2760_exit();
1949 }
1950 ldv_final:
1951 {
1952#line 378
1953 ldv_check_final_state();
1954 }
1955#line 381
1956 return;
1957}
1958}
1959#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1960void ldv_blast_assert(void)
1961{
1962
1963 {
1964 ERROR: ;
1965#line 6
1966 goto ERROR;
1967}
1968}
1969#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1970extern int __VERIFIER_nondet_int(void) ;
1971#line 402 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
1972int ldv_spin = 0;
1973#line 406 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
1974void ldv_check_alloc_flags(gfp_t flags )