1268#line 259
1269 tmp___1 = __VERIFIER_nondet_int();
1270 }
1271#line 259
1272 if (tmp___1 != 0) {
1273#line 260
1274 goto ldv_18624;
1275 } else {
1276#line 262
1277 goto ldv_18626;
1278 }
1279 ldv_18626: ;
1280 {
1281#line 279
1282 ks0108_exit();
1283 }
1284 ldv_final:
1285 {
1286#line 282
1287 ldv_check_final_state();
1288 }
1289#line 285
1290 return;
1291}
1292}
1293#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17289/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1294void ldv_blast_assert(void)
1295{
1296
1297 {
1298 ERROR: ;
1299#line 6
1300 goto ERROR;
1301}
1302}
1303#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17289/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1304extern int __VERIFIER_nondet_int(void) ;
1305#line 306 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17289/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/ks0108.c.p"
1306int ldv_spin = 0;
1307#line 310 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17289/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/ks0108.c.p"
1308void ldv_check_alloc_flags(gfp_t flags )