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