[ 0:01] compiling /home/xrockai/src/divine/nightly/test/svcomp/product-lines/minepump_spec4_product41_false.cil.c
[ 0:01] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/minepump_spec4_product41_false.cil.c:222:44: warning: incompatible redeclaration of library function 'malloc'
[ 0:01] extern  __attribute__((__nothrow__)) void *malloc(size_t __size )  __attribute__((__malloc__)) ;
[ 0:01]                                            ^
[ 0:01] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/minepump_spec4_product41_false.cil.c:222:44: note: 'malloc' is a builtin with type 'void *(unsigned long)'
[ 0:01] 1 warning generated.
[ 0:01] compiling /dios/lib/config/seqklee.bc
[ 0:01] setting up pass: functionmeta, options = 
[ 0:03] setting up pass: fuse-ctors, options = 
[ 0:03] KLEE: output directory is "/var/obj/divine-nightly/semidbg/test/__test_work_dir.19/_klee_out"
[ 0:06] KLEE: Using Z3 solver backend
[ 0:06] WARNING: this target does not support the llvm.stacksave intrinsic.
[ 0:06] warning: Linking two modules of different target triples: klee_div_zero_check.bc' is 'x86_64-unknown-linux-gnu' whereas 'klee.bc' is 'x86_64-unknown-none-elf'
[ 0:06] 
[ 0:06] KLEE: WARNING: undefined reference to function: __dios_tainted_init
[ 0:10] KLEE: WARNING: undefined reference to function: klee_free
[ 0:10] KLEE: WARNING: undefined reference to function: klee_malloc
[ 0:10] i:1
[ 0:10] KLEE: WARNING ONCE: Alignment of memory from call "klee_malloc" is not modelled. Using alignment of 8.
[ 0:10] about to __boot:0
[ 0:10] about to run the scheduler:0
[ 0:10] KLEE: WARNING ONCE: calling external: __dios_tainted_init() at /dios/libc/sys/start.cpp:49 5
[ 0:10] KLEE: ERROR: /dios/libc/sys/start.cpp:87: failed external call: __dios_tainted_init
[ 0:10] KLEE: NOTE: now ignoring this error at this location
[ 0:10] KLEE: ERROR: EXITING ON ERROR:
[ 0:10] Error: failed external call: __dios_tainted_init
[ 0:10] File: /dios/libc/sys/start.cpp
[ 0:10] Line: 87
[ 0:10] assembly.ll line: 35768
[ 0:10] Stack: 
[ 0:10] 	#000035768 in __dios_start (l=0, argc=1, argv=94203617546760, envp=94203617615880) at /dios/libc/sys/start.cpp:87
[ 0:10] 	#100011738 in _ZN6__dios10sched_nullINS_5ClockINS_10NondetKleeINS_4BaseEEEEEE13run_schedulerINS_7ContextEEEvv () at /dios/sys/sched_null.hpp:163
[ 0:10] 	#200044101 in klee_boot (argc=2, argv=94203591604992) at /dios/arch/klee/boot.c:41
[ 0:10] 
[ 0:10] 
[ 0:10]      1	/* TAGS: error c sym  */
[ 0:10]      2	/* VERIFY_OPTS: --symbolic -o nofail:malloc */
[ 0:10]      3	extern void __VERIFIER_error() __attribute__ ((__noreturn__));
[ 0:10]      4	
[ 0:10]      5	extern int __VERIFIER_nondet_int(void);
[ 0:10]      6	extern int printf (__const char *__restrict __format, ...);
[ 0:10]      7	/* Generated by CIL v. 1.3.7 */
[ 0:10]      8	/* print_CIL_Input is true */
[ 0:10]      9	
[ 0:10]     10	struct JoinPoint {
[ 0:10]     11	   void **(*fp)(struct JoinPoint * ) ;
[ 0:10]     12	   void **args ;
[ 0:10]     13	   int argsCount ;
[ 0:10]     14	   char const   **argsType ;
[ 0:10]     15	   void *(*arg)(int  , struct JoinPoint * ) ;
[ 0:10]     16	   char const   *(*argType)(int  , struct JoinPoint * ) ;
[ 0:10]     17	   void **retValue ;
[ 0:10]     18	   char const   *retType ;
[ 0:10]     19	   char const   *funcName ;
[ 0:10]     20	   char const   *targetName ;
[ 0:10]     21	   char const   *fileName ;
[ 0:10]     22	   char const   *kind ;
[ 0:10]     23	   void *excep_return ;
[ 0:10]     24	};
[ 0:10]     25	struct __UTAC__CFLOW_FUNC {
[ 0:10]     26	   int (*func)(int  , int  ) ;
[ 0:10]     27	   int val ;
[ 0:10]     28	   struct __UTAC__CFLOW_FUNC *next ;
[ 0:10]     29	};
[ 0:10]     30	struct __UTAC__EXCEPTION {
[ 0:10]     31	   void *jumpbuf ;
[ 0:10]     32	   unsigned long long prtValue ;
[ 0:10]     33	   int pops ;
[ 0:10]     34	   struct __UTAC__CFLOW_FUNC *cflowfuncs ;
[ 0:10]     35	};
[ 0:10]     36	typedef unsigned int size_t;
[ 0:10]     37	struct __ACC__ERR {
[ 0:10]     38	   void *v ;
[ 0:10]     39	   struct __ACC__ERR *next ;
[ 0:10]     40	};
[ 0:10]     41	#pragma merger(0,"Environment.i","")
[ 0:10]     42	void lowerWaterLevel(void) ;
[ 0:10]     43	void waterRise(void) ;
[ 0:10]     44	void changeMethaneLevel(void) ;
[ 0:10]     45	int isMethaneLevelCritical(void) ;
[ 0:10]     46	int getWaterLevel(void) ;
[ 0:10]     47	void printEnvironment(void) ;
[ 0:10]     48	int isHighWaterSensorDry(void) ;
[ 0:10]     49	int waterLevel  =    1;
[ 0:10]     50	int methaneLevelCritical  =    0;
[ 0:10]     51	void lowerWaterLevel(void) 
[ 0:10]     52	{ 
[ 0:10]     53	
[ 0:10]     54	  {
[ 0:10]     55	  if (waterLevel > 0) {
[ 0:10]     56	    waterLevel = waterLevel - 1;
[ 0:10]     57	  } else {
[ 0:10]     58	
[ 0:10]     59	  }
[ 0:10]     60	  return;
[ 0:10]     61	}
[ 0:10]     62	}
[ 0:10]     63	void waterRise(void) 
[ 0:10]     64	{ 
[ 0:10]     65	
[ 0:10]     66	  {
[ 0:10]     67	  if (waterLevel < 2) {
[ 0:10]     68	    waterLevel = waterLevel + 1;
[ 0:10]     69	  } else {
[ 0:10]     70	
[ 0:10]     71	  }
[ 0:10]     72	  return;
[ 0:10]     73	}
[ 0:10]     74	}
[ 0:10]     75	void changeMethaneLevel(void) 
[ 0:10]     76	{ 
[ 0:10]     77	
[ 0:10]     78	  {
[ 0:10]     79	  if (methaneLevelCritical) {
[ 0:10]     80	    methaneLevelCritical = 0;
[ 0:10]     81	  } else {
[ 0:10]     82	    methaneLevelCritical = 1;
[ 0:10]     83	  }
[ 0:10]     84	  return;
[ 0:10]     85	}
[ 0:10]     86	}
[ 0:10]     87	int isMethaneLevelCritical(void) 
[ 0:10]     88	{ int retValue_acc ;
[ 0:10]     89	
[ 0:10]     90	  {
[ 0:10]     91	  retValue_acc = methaneLevelCritical;
[ 0:10]     92	  return (retValue_acc);
[ 0:10]     93	  return (retValue_acc);
[ 0:10]     94	}
[ 0:10]     95	}
[ 0:10]     96	void printEnvironment(void) 
[ 0:10]     97	{ 
[ 0:10]     98	
[ 0:10]     99	  {
[ 0:10]    100	  {
[ 0:10]    101	  printf("Env(Water:%i", waterLevel);
[ 0:10]    102	  printf(",Meth:");
[ 0:10]    103	  }
[ 0:10]    104	  if (methaneLevelCritical) {
[ 0:10]    105	    {
[ 0:10]    106	    printf("CRIT");
[ 0:10]    107	    }
[ 0:10]    108	  } else {
[ 0:10]    109	    {
[ 0:10]    110	    printf("OK");
[ 0:10]    111	    }
[ 0:10]    112	  }
[ 0:10]    113	  {
[ 0:10]    114	  printf(")");
[ 0:10]    115	  }
[ 0:10]    116	  return;
[ 0:10]    117	}
[ 0:10]    118	}
[ 0:10]    119	int getWaterLevel(void) 
[ 0:10]    120	{ int retValue_acc ;
[ 0:10]    121	
[ 0:10]    122	  {
[ 0:10]    123	  retValue_acc = waterLevel;
[ 0:10]    124	  return (retValue_acc);
[ 0:10]    125	  return (retValue_acc);
[ 0:10]    126	}
[ 0:10]    127	}
[ 0:10]    128	int isHighWaterSensorDry(void) 
[ 0:10]    129	{ int retValue_acc ;
[ 0:10]    130	
[ 0:10]    131	  {
[ 0:10]    132	  if (waterLevel < 2) {
[ 0:10]    133	    retValue_acc = 1;
[ 0:10]    134	    return (retValue_acc);
[ 0:10]    135	  } else {
[ 0:10]    136	    retValue_acc = 0;
[ 0:10]    137	    return (retValue_acc);
[ 0:10]    138	  }
[ 0:10]    139	  return (retValue_acc);
[ 0:10]    140	}
[ 0:10]    141	}
[ 0:10]    142	#pragma merger(0,"Specification4_spec.i","")
[ 0:10]    143	void __automaton_fail(void) ;
[ 0:10]    144	int isPumpRunning(void) ;
[ 0:10]    145	inline static void __utac_acc__Specification4_spec__1(void) 
[ 0:10]    146	{ int tmp ;
[ 0:10]    147	  int tmp___0 ;
[ 0:10]    148	
[ 0:10]    149	  {
[ 0:10]    150	  {
[ 0:10]    151	  tmp = getWaterLevel();
[ 0:10]    152	  }
[ 0:10]    153	  if (tmp == 0) {
[ 0:10]    154	    {
[ 0:10]    155	    tmp___0 = isPumpRunning();
[ 0:10]    156	    }
[ 0:10]    157	    if (tmp___0) {
[ 0:10]    158	      {
[ 0:10]    159	      __automaton_fail();
[ 0:10]    160	      }
[ 0:10]    161	    } else {
[ 0:10]    162	
[ 0:10]    163	    }
[ 0:10]    164	  } else {
[ 0:10]    165	
[ 0:10]    166	  }
[ 0:10]    167	  return;
[ 0:10]    168	}
[ 0:10]    169	}
[ 0:10]    170	#pragma merger(0,"featureselect.i","")
[ 0:10]    171	int select_one(void) ;
[ 0:10]    172	void select_features(void) ;
[ 0:10]    173	void select_helpers(void) ;
[ 0:10]    174	int valid_product(void) ;
[ 0:10]    175	int select_one(void) 
[ 0:10]    176	{ int retValue_acc ;
[ 0:10]    177	  int choice = __VERIFIER_nondet_int();
[ 0:10]    178	
[ 0:10]    179	  {
[ 0:10]    180	  retValue_acc = choice;
[ 0:10]    181	  return (retValue_acc);
[ 0:10]    182	  return (retValue_acc);
[ 0:10]    183	}
[ 0:10]    184	}
[ 0:10]    185	void select_features(void) 
[ 0:10]    186	{ 
[ 0:10]    187	
[ 0:10]    188	  {
[ 0:10]    189	  return;
[ 0:10]    190	}
[ 0:10]    191	}
[ 0:10]    192	void select_helpers(void) 
[ 0:10]    193	{ 
[ 0:10]    194	
[ 0:10]    195	  {
[ 0:10]    196	  return;
[ 0:10]    197	}
[ 0:10]    198	}
[ 0:10]    199	int valid_product(void) 
[ 0:10]    200	{ int retValue_acc ;
[ 0:10]    201	
[ 0:10]    202	  {
[ 0:10]    203	  retValue_acc = 1;
[ 0:10]    204	  return (retValue_acc);
[ 0:10]    205	  return (retValue_acc);
[ 0:10]    206	}
[ 0:10]    207	}
[ 0:10]    208	#pragma merger(0,"wsllib_check.i","")
[ 0:10]    209	void __automaton_fail(void) 
[ 0:10]    210	{ 
[ 0:10]    211	
[ 0:10]    212	  {
[ 0:10]    213	  ERROR: __VERIFIER_error(); /* ERROR */
[ 0:10]    214	  return;
[ 0:10]    215	}
[ 0:10]    216	}
[ 0:10]    217	#pragma merger(0,"libacc.i","")
[ 0:10]    218	extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
[ 0:10]    219	                                                                      char const   *__file ,
[ 0:10]    220	                                                                      unsigned int __line ,
[ 0:10]    221	                                                                      char const   *__function ) ;
[ 0:10]    222	extern  __attribute__((__nothrow__)) void *malloc(size_t __size )  __attribute__((__malloc__)) ;
[ 0:10]    223	extern  __attribute__((__nothrow__)) void free(void *__ptr ) ;
[ 0:10]    224	void __utac__exception__cf_handler_set(void *exception , int (*cflow_func)(int  ,
[ 0:10]    225	                                                                           int  ) ,
[ 0:10]    226	                                       int val ) 
[ 0:10]    227	{ struct __UTAC__EXCEPTION *excep ;
[ 0:10]    228	  struct __UTAC__CFLOW_FUNC *cf ;
[ 0:10]    229	  void *tmp ;
[ 0:10]    230	  unsigned long __cil_tmp7 ;
[ 0:10]    231	  unsigned long __cil_tmp8 ;
[ 0:10]    232	  unsigned long __cil_tmp9 ;
[ 0:10]    233	  unsigned long __cil_tmp10 ;
[ 0:10]    234	  unsigned long __cil_tmp11 ;
[ 0:10]    235	  unsigned long __cil_tmp12 ;
[ 0:10]    236	  unsigned long __cil_tmp13 ;
[ 0:10]    237	  unsigned long __cil_tmp14 ;
[ 0:10]    238	  int (**mem_15)(int  , int  ) ;
[ 0:10]    239	  int *mem_16 ;
[ 0:10]    240	  struct __UTAC__CFLOW_FUNC **mem_17 ;
[ 0:10]    241	  struct __UTAC__CFLOW_FUNC **mem_18 ;
[ 0:10]    242	  struct __UTAC__CFLOW_FUNC **mem_19 ;
[ 0:10]    243	
[ 0:10]    244	  {
[ 0:10]    245	  {
[ 0:10]    246	  excep = (struct __UTAC__EXCEPTION *)exception;
[ 0:10]    247	  tmp = malloc(24UL);
[ 0:10]    248	  cf = (struct __UTAC__CFLOW_FUNC *)tmp;
[ 0:10]    249	  mem_15 = (int (**)(int  , int  ))cf;
[ 0:10]    250	  *mem_15 = cflow_func;
[ 0:10]    251	  __cil_tmp7 = (unsigned long )cf;
[ 0:10]    252	  __cil_tmp8 = __cil_tmp7 + 8;
[ 0:10]    253	  mem_16 = (int *)__cil_tmp8;
[ 0:10]    254	  *mem_16 = val;
[ 0:10]    255	  __cil_tmp9 = (unsigned long )cf;
[ 0:10]    256	  __cil_tmp10 = __cil_tmp9 + 16;
[ 0:10]    257	  __cil_tmp11 = (unsigned long )excep;
[ 0:10]    258	  __cil_tmp12 = __cil_tmp11 + 24;
[ 0:10]    259	  mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp10;
[ 0:10]    260	  mem_18 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp12;
[ 0:10]    261	  *mem_17 = *mem_18;
[ 0:10]    262	  __cil_tmp13 = (unsigned long )excep;
[ 0:10]    263	  __cil_tmp14 = __cil_tmp13 + 24;
[ 0:10]    264	  mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
[ 0:10]    265	  *mem_19 = cf;
[ 0:10]    266	  }
[ 0:10]    267	  return;
[ 0:10]    268	}
[ 0:10]    269	}
[ 0:10]    270	void __utac__exception__cf_handler_free(void *exception ) 
[ 0:10]    271	{ struct __UTAC__EXCEPTION *excep ;
[ 0:10]    272	  struct __UTAC__CFLOW_FUNC *cf ;
[ 0:10]    273	  struct __UTAC__CFLOW_FUNC *tmp ;
[ 0:10]    274	  unsigned long __cil_tmp5 ;
[ 0:10]    275	  unsigned long __cil_tmp6 ;
[ 0:10]    276	  struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
[ 0:10]    277	  unsigned long __cil_tmp8 ;
[ 0:10]    278	  unsigned long __cil_tmp9 ;
[ 0:10]    279	  unsigned long __cil_tmp10 ;
[ 0:10]    280	  unsigned long __cil_tmp11 ;
[ 0:10]    281	  void *__cil_tmp12 ;
[ 0:10]    282	  unsigned long __cil_tmp13 ;
[ 0:10]    283	  unsigned long __cil_tmp14 ;
[ 0:10]    284	  struct __UTAC__CFLOW_FUNC **mem_15 ;
[ 0:10]    285	  struct __UTAC__CFLOW_FUNC **mem_16 ;
[ 0:10]    286	  struct __UTAC__CFLOW_FUNC **mem_17 ;
[ 0:10]    287	
[ 0:10]    288	  {
[ 0:10]    289	  excep = (struct __UTAC__EXCEPTION *)exception;
[ 0:10]    290	  __cil_tmp5 = (unsigned long )excep;
[ 0:10]    291	  __cil_tmp6 = __cil_tmp5 + 24;
[ 0:10]    292	  mem_15 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
[ 0:10]    293	  cf = *mem_15;
[ 0:10]    294	  {
[ 0:10]    295	  while (1) {
[ 0:10]    296	    while_0_continue: /* CIL Label */ ;
[ 0:10]    297	    {
[ 0:10]    298	    __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
[ 0:10]    299	    __cil_tmp8 = (unsigned long )__cil_tmp7;
[ 0:10]    300	    __cil_tmp9 = (unsigned long )cf;
[ 0:10]    301	    if (__cil_tmp9 != __cil_tmp8) {
[ 0:10]    302	
[ 0:10]    303	    } else {
[ 0:10]    304	      goto while_0_break;
[ 0:10]    305	    }
[ 0:10]    306	    }
[ 0:10]    307	    {
[ 0:10]    308	    tmp = cf;
[ 0:10]    309	    __cil_tmp10 = (unsigned long )cf;
[ 0:10]    310	    __cil_tmp11 = __cil_tmp10 + 16;
[ 0:10]    311	    mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp11;
[ 0:10]    312	    cf = *mem_16;
[ 0:10]    313	    __cil_tmp12 = (void *)tmp;
[ 0:10]    314	    free(__cil_tmp12);
[ 0:10]    315	    }
[ 0:10]    316	  }
[ 0:10]    317	  while_0_break: /* CIL Label */ ;
[ 0:10]    318	  }
[ 0:10]    319	  __cil_tmp13 = (unsigned long )excep;
[ 0:10]    320	  __cil_tmp14 = __cil_tmp13 + 24;
[ 0:10]    321	  mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
[ 0:10]    322	  *mem_17 = (struct __UTAC__CFLOW_FUNC *)0;
[ 0:10]    323	  return;
[ 0:10]    324	}
[ 0:10]    325	}
[ 0:10]    326	void __utac__exception__cf_handler_reset(void *exception ) 
[ 0:10]    327	{ struct __UTAC__EXCEPTION *excep ;
[ 0:10]    328	  struct __UTAC__CFLOW_FUNC *cf ;
[ 0:10]    329	  unsigned long __cil_tmp5 ;
[ 0:10]    330	  unsigned long __cil_tmp6 ;
[ 0:10]    331	  struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
[ 0:10]    332	  unsigned long __cil_tmp8 ;
[ 0:10]    333	  unsigned long __cil_tmp9 ;
[ 0:10]    334	  int (*__cil_tmp10)(int  , int  ) ;
[ 0:10]    335	  unsigned long __cil_tmp11 ;
[ 0:10]    336	  unsigned long __cil_tmp12 ;
[ 0:10]    337	  int __cil_tmp13 ;
[ 0:10]    338	  unsigned long __cil_tmp14 ;
[ 0:10]    339	  unsigned long __cil_tmp15 ;
[ 0:10]    340	  struct __UTAC__CFLOW_FUNC **mem_16 ;
[ 0:10]    341	  int (**mem_17)(int  , int  ) ;
[ 0:10]    342	  int *mem_18 ;
[ 0:10]    343	  struct __UTAC__CFLOW_FUNC **mem_19 ;
[ 0:10]    344	
[ 0:10]    345	  {
[ 0:10]    346	  excep = (struct __UTAC__EXCEPTION *)exception;
[ 0:10]    347	  __cil_tmp5 = (unsigned long )excep;
[ 0:10]    348	  __cil_tmp6 = __cil_tmp5 + 24;
[ 0:10]    349	  mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
[ 0:10]    350	  cf = *mem_16;
[ 0:10]    351	  {
[ 0:10]    352	  while (1) {
[ 0:10]    353	    while_1_continue: /* CIL Label */ ;
[ 0:10]    354	    {
[ 0:10]    355	    __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
[ 0:10]    356	    __cil_tmp8 = (unsigned long )__cil_tmp7;
[ 0:10]    357	    __cil_tmp9 = (unsigned long )cf;
[ 0:10]    358	    if (__cil_tmp9 != __cil_tmp8) {
[ 0:10]    359	
[ 0:10]    360	    } else {
[ 0:10]    361	      goto while_1_break;
[ 0:10]    362	    }
[ 0:10]    363	    }
[ 0:10]    364	    {
[ 0:10]    365	    mem_17 = (int (**)(int  , int  ))cf;
[ 0:10]    366	    __cil_tmp10 = *mem_17;
[ 0:10]    367	    __cil_tmp11 = (unsigned long )cf;
[ 0:10]    368	    __cil_tmp12 = __cil_tmp11 + 8;
[ 0:10]    369	    mem_18 = (int *)__cil_tmp12;
[ 0:10]    370	    __cil_tmp13 = *mem_18;
[ 0:10]    371	    (*__cil_tmp10)(4, __cil_tmp13);
[ 0:10]    372	    __cil_tmp14 = (unsigned long )cf;
[ 0:10]    373	    __cil_tmp15 = __cil_tmp14 + 16;
[ 0:10]    374	    mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp15;
[ 0:10]    375	    cf = *mem_19;
[ 0:10]    376	    }
[ 0:10]    377	  }
[ 0:10]    378	  while_1_break: /* CIL Label */ ;
[ 0:10]    379	  }
[ 0:10]    380	  {
[ 0:10]    381	  __utac__exception__cf_handler_free(exception);
[ 0:10]    382	  }
[ 0:10]    383	  return;
[ 0:10]    384	}
[ 0:10]    385	}
[ 0:10]    386	void *__utac__error_stack_mgt(void *env , int mode , int count ) ;
[ 0:10]    387	static struct __ACC__ERR *head  =    (struct __ACC__ERR *)0;
[ 0:10]    388	void *__utac__error_stack_mgt(void *env , int mode , int count ) 
[ 0:10]    389	{ void *retValue_acc ;
[ 0:10]    390	  struct __ACC__ERR *new ;
[ 0:10]    391	  void *tmp ;
[ 0:10]    392	  struct __ACC__ERR *temp ;
[ 0:10]    393	  struct __ACC__ERR *next ;
[ 0:10]    394	  void *excep ;
[ 0:10]    395	  unsigned long __cil_tmp10 ;
[ 0:10]    396	  unsigned long __cil_tmp11 ;
[ 0:10]    397	  unsigned long __cil_tmp12 ;
[ 0:10]    398	  unsigned long __cil_tmp13 ;
[ 0:10]    399	  void *__cil_tmp14 ;
[ 0:10]    400	  unsigned long __cil_tmp15 ;
[ 0:10]    401	  unsigned long __cil_tmp16 ;
[ 0:10]    402	  void *__cil_tmp17 ;
[ 0:10]    403	  void **mem_18 ;
[ 0:10]    404	  struct __ACC__ERR **mem_19 ;
[ 0:10]    405	  struct __ACC__ERR **mem_20 ;
[ 0:10]    406	  void **mem_21 ;
[ 0:10]    407	  struct __ACC__ERR **mem_22 ;
[ 0:10]    408	  void **mem_23 ;
[ 0:10]    409	  void **mem_24 ;
[ 0:10]    410	
[ 0:10]    411	  {
[ 0:10]    412	  if (count == 0) {
[ 0:10]    413	    return (retValue_acc);
[ 0:10]    414	  } else {
[ 0:10]    415	
[ 0:10]    416	  }
[ 0:10]    417	  if (mode == 0) {
[ 0:10]    418	    {
[ 0:10]    419	    tmp = malloc(16UL);
[ 0:10]    420	    new = (struct __ACC__ERR *)tmp;
[ 0:10]    421	    mem_18 = (void **)new;
[ 0:10]    422	    *mem_18 = env;
[ 0:10]    423	    __cil_tmp10 = (unsigned long )new;
[ 0:10]    424	    __cil_tmp11 = __cil_tmp10 + 8;
[ 0:10]    425	    mem_19 = (struct __ACC__ERR **)__cil_tmp11;
[ 0:10]    426	    *mem_19 = head;
[ 0:10]    427	    head = new;
[ 0:10]    428	    retValue_acc = (void *)new;
[ 0:10]    429	    }
[ 0:10]    430	    return (retValue_acc);
[ 0:10]    431	  } else {
[ 0:10]    432	
[ 0:10]    433	  }
[ 0:10]    434	  if (mode == 1) {
[ 0:10]    435	    temp = head;
[ 0:10]    436	    {
[ 0:10]    437	    while (1) {
[ 0:10]    438	      while_2_continue: /* CIL Label */ ;
[ 0:10]    439	      if (count > 1) {
[ 0:10]    440	
[ 0:10]    441	      } else {
[ 0:10]    442	        goto while_2_break;
[ 0:10]    443	      }
[ 0:10]    444	      {
[ 0:10]    445	      __cil_tmp12 = (unsigned long )temp;
[ 0:10]    446	      __cil_tmp13 = __cil_tmp12 + 8;
[ 0:10]    447	      mem_20 = (struct __ACC__ERR **)__cil_tmp13;
[ 0:10]    448	      next = *mem_20;
[ 0:10]    449	      mem_21 = (void **)temp;
[ 0:10]    450	      excep = *mem_21;
[ 0:10]    451	      __cil_tmp14 = (void *)temp;
[ 0:10]    452	      free(__cil_tmp14);
[ 0:10]    453	      __utac__exception__cf_handler_reset(excep);
[ 0:10]    454	      temp = next;
[ 0:10]    455	      count = count - 1;
[ 0:10]    456	      }
[ 0:10]    457	    }
[ 0:10]    458	    while_2_break: /* CIL Label */ ;
[ 0:10]    459	    }
[ 0:10]    460	    {
[ 0:10]    461	    __cil_tmp15 = (unsigned long )temp;
[ 0:10]    462	    __cil_tmp16 = __cil_tmp15 + 8;
[ 0:10]    463	    mem_22 = (struct __ACC__ERR **)__cil_tmp16;
[ 0:10]    464	    head = *mem_22;
[ 0:10]    465	    mem_23 = (void **)temp;
[ 0:10]    466	    excep = *mem_23;
[ 0:10]    467	    __cil_tmp17 = (void *)temp;
[ 0:10]    468	    free(__cil_tmp17);
[ 0:10]    469	    __utac__exception__cf_handler_reset(excep);
[ 0:10]    470	    retValue_acc = excep;
[ 0:10]    471	    }
[ 0:10]    472	    return (retValue_acc);
[ 0:10]    473	  } else {
[ 0:10]    474	
[ 0:10]    475	  }
[ 0:10]    476	  if (mode == 2) {
[ 0:10]    477	    if (head) {
[ 0:10]    478	      mem_24 = (void **)head;
[ 0:10]    479	      retValue_acc = *mem_24;
[ 0:10]    480	      return (retValue_acc);
[ 0:10]    481	    } else {
[ 0:10]    482	      retValue_acc = (void *)0;
[ 0:10]    483	      return (retValue_acc);
[ 0:10]    484	    }
[ 0:10]    485	  } else {
[ 0:10]    486	
[ 0:10]    487	  }
[ 0:10]    488	  return (retValue_acc);
[ 0:10]    489	}
[ 0:10]    490	}
[ 0:10]    491	void *__utac__get_this_arg(int i , struct JoinPoint *this ) 
[ 0:10]    492	{ void *retValue_acc ;
[ 0:10]    493	  unsigned long __cil_tmp4 ;
[ 0:10]    494	  unsigned long __cil_tmp5 ;
[ 0:10]    495	  int __cil_tmp6 ;
[ 0:10]    496	  int __cil_tmp7 ;
[ 0:10]    497	  unsigned long __cil_tmp8 ;
[ 0:10]    498	  unsigned long __cil_tmp9 ;
[ 0:10]    499	  void **__cil_tmp10 ;
[ 0:10]    500	  void **__cil_tmp11 ;
[ 0:10]    501	  int *mem_12 ;
[ 0:10]    502	  void ***mem_13 ;
[ 0:10]    503	
[ 0:10]    504	  {
[ 0:10]    505	  if (i > 0) {
[ 0:10]    506	    {
[ 0:10]    507	    __cil_tmp4 = (unsigned long )this;
[ 0:10]    508	    __cil_tmp5 = __cil_tmp4 + 16;
[ 0:10]    509	    mem_12 = (int *)__cil_tmp5;
[ 0:10]    510	    __cil_tmp6 = *mem_12;
[ 0:10]    511	    if (i <= __cil_tmp6) {
[ 0:10]    512	
[ 0:10]    513	    } else {
[ 0:10]    514	      {
[ 0:10]    515	      __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
[ 0:10]    516	                    123U, "__utac__get_this_arg");
[ 0:10]    517	      }
[ 0:10]    518	    }
[ 0:10]    519	    }
[ 0:10]    520	  } else {
[ 0:10]    521	    {
[ 0:10]    522	    __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
[ 0:10]    523	                  123U, "__utac__get_this_arg");
[ 0:10]    524	    }
[ 0:10]    525	  }
[ 0:10]    526	  __cil_tmp7 = i - 1;
[ 0:10]    527	  __cil_tmp8 = (unsigned long )this;
[ 0:10]    528	  __cil_tmp9 = __cil_tmp8 + 8;
[ 0:10]    529	  mem_13 = (void ***)__cil_tmp9;
[ 0:10]    530	  __cil_tmp10 = *mem_13;
[ 0:10]    531	  __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
[ 0:10]    532	  retValue_acc = *__cil_tmp11;
[ 0:10]    533	  return (retValue_acc);
[ 0:10]    534	  return (retValue_acc);
[ 0:10]    535	}
[ 0:10]    536	}
[ 0:10]    537	char const   *__utac__get_this_argtype(int i , struct JoinPoint *this ) 
[ 0:10]    538	{ char const   *retValue_acc ;
[ 0:10]    539	  unsigned long __cil_tmp4 ;
[ 0:10]    540	  unsigned long __cil_tmp5 ;
[ 0:10]    541	  int __cil_tmp6 ;
[ 0:10]    542	  int __cil_tmp7 ;
[ 0:10]    543	  unsigned long __cil_tmp8 ;
[ 0:10]    544	  unsigned long __cil_tmp9 ;
[ 0:10]    545	  char const   **__cil_tmp10 ;
[ 0:10]    546	  char const   **__cil_tmp11 ;
[ 0:10]    547	  int *mem_12 ;
[ 0:10]    548	  char const   ***mem_13 ;
[ 0:10]    549	
[ 0:10]    550	  {
[ 0:10]    551	  if (i > 0) {
[ 0:10]    552	    {
[ 0:10]    553	    __cil_tmp4 = (unsigned long )this;
[ 0:10]    554	    __cil_tmp5 = __cil_tmp4 + 16;
[ 0:10]    555	    mem_12 = (int *)__cil_tmp5;
[ 0:10]    556	    __cil_tmp6 = *mem_12;
[ 0:10]    557	    if (i <= __cil_tmp6) {
[ 0:10]    558	
[ 0:10]    559	    } else {
[ 0:10]    560	      {
[ 0:10]    561	      __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
[ 0:10]    562	                    131U, "__utac__get_this_argtype");
[ 0:10]    563	      }
[ 0:10]    564	    }
[ 0:10]    565	    }
[ 0:10]    566	  } else {
[ 0:10]    567	    {
[ 0:10]    568	    __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
[ 0:10]    569	                  131U, "__utac__get_this_argtype");
[ 0:10]    570	    }
[ 0:10]    571	  }
[ 0:10]    572	  __cil_tmp7 = i - 1;
[ 0:10]    573	  __cil_tmp8 = (unsigned long )this;
[ 0:10]    574	  __cil_tmp9 = __cil_tmp8 + 24;
[ 0:10]    575	  mem_13 = (char const   ***)__cil_tmp9;
[ 0:10]    576	  __cil_tmp10 = *mem_13;
[ 0:10]    577	  __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
[ 0:10]    578	  retValue_acc = *__cil_tmp11;
[ 0:10]    579	  return (retValue_acc);
[ 0:10]    580	  return (retValue_acc);
[ 0:10]    581	}
[ 0:10]    582	}
[ 0:10]    583	#pragma merger(0,"scenario.i","")
[ 0:10]    584	void timeShift(void) ;
[ 0:10]    585	void cleanup(void) ;
[ 0:10]    586	void test(void) 
[ 0:10]    587	{ int splverifierCounter ;
[ 0:10]    588	  int tmp ;
[ 0:10]    589	  int tmp___0 ;
[ 0:10]    590	  int tmp___1 ;
[ 0:10]    591	  int tmp___2 ;
[ 0:10]    592	
[ 0:10]    593	  {
[ 0:10]    594	  splverifierCounter = 0;
[ 0:10]    595	  {
[ 0:10]    596	  while (1) {
[ 0:10]    597	    while_3_continue: /* CIL Label */ ;
[ 0:10]    598	    if (splverifierCounter < 4) {
[ 0:10]    599	
[ 0:10]    600	    } else {
[ 0:10]    601	      goto while_3_break;
[ 0:10]    602	    }
[ 0:10]    603	    {
[ 0:10]    604	    tmp = __VERIFIER_nondet_int();
[ 0:10]    605	    }
[ 0:10]    606	    if (tmp) {
[ 0:10]    607	      {
[ 0:10]    608	      waterRise();
[ 0:10]    609	      }
[ 0:10]    610	    } else {
[ 0:10]    611	
[ 0:10]    612	    }
[ 0:10]    613	    {
[ 0:10]    614	    tmp___0 = __VERIFIER_nondet_int();
[ 0:10]    615	    }
[ 0:10]    616	    if (tmp___0) {
[ 0:10]    617	      {
[ 0:10]    618	      changeMethaneLevel();
[ 0:10]    619	      }
[ 0:10]    620	    } else {
[ 0:10]    621	
[ 0:10]    622	    }
[ 0:10]    623	    {
[ 0:10]    624	    tmp___2 = __VERIFIER_nondet_int();
[ 0:10]    625	    }
[ 0:10]    626	    if (tmp___2) {
[ 0:10]    627	
[ 0:10]    628	    } else {
[ 0:10]    629	      {
[ 0:10]    630	      tmp___1 = __VERIFIER_nondet_int();
[ 0:10]    631	      }
[ 0:10]    632	      if (tmp___1) {
[ 0:10]    633	
[ 0:10]    634	      } else {
[ 0:10]    635	
[ 0:10]    636	      }
[ 0:10]    637	    }
[ 0:10]    638	    {
[ 0:10]    639	    timeShift();
[ 0:10]    640	    }
[ 0:10]    641	  }
[ 0:10]    642	  while_3_break: /* CIL Label */ ;
[ 0:10]    643	  }
[ 0:10]    644	  {
[ 0:10]    645	  cleanup();
[ 0:10]    646	  }
[ 0:10]    647	  return;
[ 0:10]    648	}
[ 0:10]    649	}
[ 0:10]    650	#pragma merger(0,"MinePump.i","")
[ 0:10]    651	void activatePump(void) ;
[ 0:10]    652	void deactivatePump(void) ;
[ 0:10]    653	void printPump(void) ;
[ 0:10]    654	int pumpRunning  =    0;
[ 0:10]    655	int systemActive  =    1;
[ 0:10]    656	void processEnvironment(void) ;
[ 0:10]    657	void timeShift(void) 
[ 0:10]    658	{ 
[ 0:10]    659	
[ 0:10]    660	  {
[ 0:10]    661	  if (pumpRunning) {
[ 0:10]    662	    {
[ 0:10]    663	    lowerWaterLevel();
[ 0:10]    664	    }
[ 0:10]    665	  } else {
[ 0:10]    666	
[ 0:10]    667	  }
[ 0:10]    668	  if (systemActive) {
[ 0:10]    669	    {
[ 0:10]    670	    processEnvironment();
[ 0:10]    671	    }
[ 0:10]    672	  } else {
[ 0:10]    673	
[ 0:10]    674	  }
[ 0:10]    675	  {
[ 0:10]    676	  __utac_acc__Specification4_spec__1();
[ 0:10]    677	  }
[ 0:10]    678	  return;
[ 0:10]    679	}
[ 0:10]    680	}
[ 0:10]    681	void processEnvironment__wrappee__base(void) 
[ 0:10]    682	{ 
[ 0:10]    683	
[ 0:10]    684	  {
[ 0:10]    685	  return;
[ 0:10]    686	}
[ 0:10]    687	}
[ 0:10]    688	int isHighWaterLevel(void) ;
[ 0:10]    689	void processEnvironment(void) 
[ 0:10]    690	{ int tmp ;
[ 0:10]    691	
[ 0:10]    692	  {
[ 0:10]    693	  if (! pumpRunning) {
[ 0:10]    694	    {
[ 0:10]    695	    tmp = isHighWaterLevel();
[ 0:10]    696	    }
[ 0:10]    697	    if (tmp) {
[ 0:10]    698	      {
[ 0:10]    699	      activatePump();
[ 0:10]    700	      }
[ 0:10]    701	    } else {
[ 0:10]    702	      {
[ 0:10]    703	      processEnvironment__wrappee__base();
[ 0:10]    704	      }
[ 0:10]    705	    }
[ 0:10]    706	  } else {
[ 0:10]    707	    {
[ 0:10]    708	    processEnvironment__wrappee__base();
[ 0:10]    709	    }
[ 0:10]    710	  }
[ 0:10]    711	  return;
[ 0:10]    712	}
[ 0:10]    713	}
[ 0:10]    714	void activatePump__wrappee__highWaterSensor(void) 
[ 0:10]    715	{ 
[ 0:10]    716	
[ 0:10]    717	  {
[ 0:10]    718	  pumpRunning = 1;
[ 0:10]    719	  return;
[ 0:10]    720	}
[ 0:10]    721	}
[ 0:10]    722	int isMethaneAlarm(void) ;
[ 0:10]    723	void activatePump(void) 
[ 0:10]    724	{ int tmp ;
[ 0:10]    725	
[ 0:10]    726	  {
[ 0:10]    727	  {
[ 0:10]    728	  tmp = isMethaneAlarm();
[ 0:10]    729	  }
[ 0:10]    730	  if (tmp) {
[ 0:10]    731	
[ 0:10]    732	  } else {
[ 0:10]    733	    {
[ 0:10]    734	    activatePump__wrappee__highWaterSensor();
[ 0:10]    735	    }
[ 0:10]    736	  }
[ 0:10]    737	  return;
[ 0:10]    738	}
[ 0:10]    739	}
[ 0:10]    740	void deactivatePump(void) 
[ 0:10]    741	{ 
[ 0:10]    742	
[ 0:10]    743	  {
[ 0:10]    744	  pumpRunning = 0;
[ 0:10]    745	  return;
[ 0:10]    746	}
[ 0:10]    747	}
[ 0:10]    748	int isMethaneAlarm(void) 
[ 0:10]    749	{ int retValue_acc ;
[ 0:10]    750	
[ 0:10]    751	  {
[ 0:10]    752	  {
[ 0:10]    753	  retValue_acc = isMethaneLevelCritical();
[ 0:10]    754	  }
[ 0:10]    755	  return (retValue_acc);
[ 0:10]    756	  return (retValue_acc);
[ 0:10]    757	}
[ 0:10]    758	}
[ 0:10]    759	int isPumpRunning(void) 
[ 0:10]    760	{ int retValue_acc ;
[ 0:10]    761	
[ 0:10]    762	  {
[ 0:10]    763	  retValue_acc = pumpRunning;
[ 0:10]    764	  return (retValue_acc);
[ 0:10]    765	  return (retValue_acc);
[ 0:10]    766	}
[ 0:10]    767	}
[ 0:10]    768	void printPump(void) 
[ 0:10]    769	{ 
[ 0:10]    770	
[ 0:10]    771	  {
[ 0:10]    772	  {
[ 0:10]    773	  printf("Pump(System:");
[ 0:10]    774	  }
[ 0:10]    775	  if (systemActive) {
[ 0:10]    776	    {
[ 0:10]    777	    printf("On");
[ 0:10]    778	    }
[ 0:10]    779	  } else {
[ 0:10]    780	    {
[ 0:10]    781	    printf("Off");
[ 0:10]    782	    }
[ 0:10]    783	  }
[ 0:10]    784	  {
[ 0:10]    785	  printf(",Pump:");
[ 0:10]    786	  }
[ 0:10]    787	  if (pumpRunning) {
[ 0:10]    788	    {
[ 0:10]    789	    printf("On");
[ 0:10]    790	    }
[ 0:10]    791	  } else {
[ 0:10]    792	    {
[ 0:10]    793	    printf("Off");
[ 0:10]    794	    }
[ 0:10]    795	  }
[ 0:10]    796	  {
[ 0:10]    797	  printf(") ");
[ 0:10]    798	  printEnvironment();
[ 0:10]    799	  printf("\n");
[ 0:10]    800	  }
[ 0:10]    801	  return;
[ 0:10]    802	}
[ 0:10]    803	}
[ 0:10]    804	int isHighWaterLevel(void) 
[ 0:10]    805	{ int retValue_acc ;
[ 0:10]    806	  int tmp ;
[ 0:10]    807	  int tmp___0 ;
[ 0:10]    808	
[ 0:10]    809	  {
[ 0:10]    810	  {
[ 0:10]    811	  tmp = isHighWaterSensorDry();
[ 0:10]    812	  }
[ 0:10]    813	  if (tmp) {
[ 0:10]    814	    tmp___0 = 0;
[ 0:10]    815	  } else {
[ 0:10]    816	    tmp___0 = 1;
[ 0:10]    817	  }
[ 0:10]    818	  retValue_acc = tmp___0;
[ 0:10]    819	  return (retValue_acc);
[ 0:10]    820	  return (retValue_acc);
[ 0:10]    821	}
[ 0:10]    822	}
[ 0:10]    823	#pragma merger(0,"Test.i","")
[ 0:10]    824	int cleanupTimeShifts  =    4;
[ 0:10]    825	void cleanup(void) 
[ 0:10]    826	{ int i ;
[ 0:10]    827	  int __cil_tmp2 ;
[ 0:10]    828	
[ 0:10]    829	  {
[ 0:10]    830	  {
[ 0:10]    831	  timeShift();
[ 0:10]    832	  i = 0;
[ 0:10]    833	  }
[ 0:10]    834	  {
[ 0:10]    835	  while (1) {
[ 0:10]    836	    while_4_continue: /* CIL Label */ ;
[ 0:10]    837	    {
[ 0:10]    838	    __cil_tmp2 = cleanupTimeShifts - 1;
[ 0:10]    839	    if (i < __cil_tmp2) {
[ 0:10]    840	
[ 0:10]    841	    } else {
[ 0:10]    842	      goto while_4_break;
[ 0:10]    843	    }
[ 0:10]    844	    }
[ 0:10]    845	    {
[ 0:10]    846	    timeShift();
[ 0:10]    847	    i = i + 1;
[ 0:10]    848	    }
[ 0:10]    849	  }
[ 0:10]    850	  while_4_break: /* CIL Label */ ;
[ 0:10]    851	  }
[ 0:10]    852	  return;
[ 0:10]    853	}
[ 0:10]    854	}
[ 0:10]    855	void Specification2(void) 
[ 0:10]    856	{ 
[ 0:10]    857	
[ 0:10]    858	  {
[ 0:10]    859	  {
[ 0:10]    860	  timeShift();
[ 0:10]    861	  printPump();
[ 0:10]    862	  timeShift();
[ 0:10]    863	  printPump();
[ 0:10]    864	  timeShift();
[ 0:10]    865	  printPump();
[ 0:10]    866	  waterRise();
[ 0:10]    867	  printPump();
[ 0:10]    868	  timeShift();
[ 0:10]    869	  printPump();
[ 0:10]    870	  changeMethaneLevel();
[ 0:10]    871	  printPump();
[ 0:10]    872	  timeShift();
[ 0:10]    873	  printPump();
[ 0:10]    874	  cleanup();
[ 0:10]    875	  }
[ 0:10]    876	  return;
[ 0:10]    877	}
[ 0:10]    878	}
[ 0:10]    879	void setup(void) 
[ 0:10]    880	{ 
[ 0:10]    881	
[ 0:10]    882	  {
[ 0:10]    883	  return;
[ 0:10]    884	}
[ 0:10]    885	}
[ 0:10]    886	void runTest(void) 
[ 0:10]    887	{ 
[ 0:10]    888	
[ 0:10]    889	  {
[ 0:10]    890	  {
[ 0:10]    891	  test();
[ 0:10]    892	  }
[ 0:10]    893	  return;
[ 0:10]    894	}
[ 0:10]    895	}
[ 0:10]    896	int main(void) 
[ 0:10]    897	{ int retValue_acc ;
[ 0:10]    898	  int tmp ;
[ 0:10]    899	
[ 0:10]    900	  {
[ 0:10]    901	  {
[ 0:10]    902	  select_helpers();
[ 0:10]    903	  select_features();
[ 0:10]    904	  tmp = valid_product();
[ 0:10]    905	  }
[ 0:10]    906	  if (tmp) {
[ 0:10]    907	    {
[ 0:10]    908	    setup();
[ 0:10]    909	    runTest();
[ 0:10]    910	    }
[ 0:10]    911	  } else {
[ 0:10]    912	
[ 0:10]    913	  }
[ 0:10]    914	  retValue_acc = 0;
[ 0:10]    915	  return (retValue_acc);
[ 0:10]    916	  return (retValue_acc);
[ 0:10]    917	}
[ 0:10]    918	}
[ 0:10] # expected error to be found at /home/xrockai/src/divine/nightly/test/svcomp/product-lines/minepump_spec4_product41_false.cil.c:213, but it was not