1879 tmp___0 = __VERIFIER_nondet_int();
1880 }
1881#line 275
1882 if (tmp___0 != 0) {
1883#line 277
1884 goto ldv_15453;
1885 } else
1886#line 275
1887 if (ldv_s_regulator_userspace_consumer_driver_platform_driver != 0) {
1888#line 277
1889 goto ldv_15453;
1890 } else {
1891#line 279
1892 goto ldv_15455;
1893 }
1894 ldv_15455: ;
1895 ldv_module_exit: ;
1896 {
1897#line 325
1898 ldv_check_final_state();
1899 }
1900#line 328
1901 return;
1902}
1903}
1904#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1905void ldv_blast_assert(void)
1906{
1907
1908 {
1909 ERROR: ;
1910#line 6
1911 goto ERROR;
1912}
1913}
1914#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1915extern int __VERIFIER_nondet_int(void) ;
1916#line 349 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/userspace-consumer.c.p"
1917int ldv_spin = 0;
1918#line 353 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/userspace-consumer.c.p"
1919void ldv_check_alloc_flags(gfp_t flags )