2863 tmp___0 = __VERIFIER_nondet_int();
2864 }
2865#line 174
2866 if (tmp___0 != 0) {
2867#line 176
2868 goto ldv_18755;
2869 } else
2870#line 174
2871 if (ldv_s_dac7512_driver_spi_driver != 0) {
2872#line 176
2873 goto ldv_18755;
2874 } else {
2875#line 178
2876 goto ldv_18757;
2877 }
2878 ldv_18757: ;
2879 ldv_module_exit: ;
2880 {
2881#line 211
2882 ldv_check_final_state();
2883 }
2884#line 214
2885 return;
2886}
2887}
2888#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12646/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2889void ldv_blast_assert(void)
2890{
2891
2892 {
2893 ERROR: ;
2894#line 6
2895 goto ERROR;
2896}
2897}
2898#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12646/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2899extern int __VERIFIER_nondet_int(void) ;
2900#line 235 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12646/dscv_tempdir/dscv/ri/43_1a/drivers/misc/ti_dac7512.c.p"
2901int ldv_spin = 0;
2902#line 239 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12646/dscv_tempdir/dscv/ri/43_1a/drivers/misc/ti_dac7512.c.p"
2903void ldv_check_alloc_flags(gfp_t flags )