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