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