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