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