[ 0:00] compiling /home/xrockai/src/divine/nightly/test/svcomp/systemc/kundu2_false.cil.c
[ 0:00] /home/xrockai/src/divine/nightly/test/svcomp/systemc/kundu2_false.cil.c:603:3: warning: expression result unused
[ 0:00]   e  ;
[ 0:00]   ^
[ 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.15/_klee_out"
[ 0:04] KLEE: Using Z3 solver backend
[ 0:04] WARNING: this target does not support the llvm.stacksave intrinsic.
[ 0:04] warning: Linking two modules of different target triples: klee_div_zero_check.bc' is 'x86_64-unknown-linux-gnu' whereas 'klee.bc' is 'x86_64-unknown-none-elf'
[ 0:04] 
[ 0:04] KLEE: WARNING: undefined reference to function: __dios_tainted_init
[ 0:07] KLEE: WARNING: undefined reference to function: klee_free
[ 0:07] KLEE: WARNING: undefined reference to function: klee_malloc
[ 0:07] i:1
[ 0:07] KLEE: WARNING ONCE: Alignment of memory from call "klee_malloc" is not modelled. Using alignment of 8.
[ 0:07] about to __boot:0
[ 0:07] about to run the scheduler:0
[ 0:07] KLEE: WARNING ONCE: calling external: __dios_tainted_init() at /dios/libc/sys/start.cpp:49 5
[ 0:07] KLEE: ERROR: /dios/libc/sys/start.cpp:87: failed external call: __dios_tainted_init
[ 0:07] KLEE: NOTE: now ignoring this error at this location
[ 0:07] KLEE: ERROR: EXITING ON ERROR:
[ 0:07] Error: failed external call: __dios_tainted_init
[ 0:07] File: /dios/libc/sys/start.cpp
[ 0:07] Line: 87
[ 0:07] assembly.ll line: 35034
[ 0:07] Stack: 
[ 0:07] 	#000035034 in __dios_start (l=0, argc=1, argv=93930840592904, envp=93930840653832) at /dios/libc/sys/start.cpp:87
[ 0:07] 	#100011053 in _ZN6__dios10sched_nullINS_5ClockINS_10NondetKleeINS_4BaseEEEEEE13run_schedulerINS_7ContextEEEvv () at /dios/sys/sched_null.hpp:163
[ 0:07] 	#200043384 in klee_boot (argc=2, argv=93930813732864) at /dios/arch/klee/boot.c:41
[ 0:07] 
[ 0:07] 
[ 0:07]      1	/* TAGS: error c sym */
[ 0:07]      2	/* VERIFY_OPTS: --symbolic --sequential -o nofail:malloc */
[ 0:07]      3	extern void __VERIFIER_error() __attribute__ ((__noreturn__));
[ 0:07]      4	
[ 0:07]      5	extern int __VERIFIER_nondet_int();
[ 0:07]      6	
[ 0:07]      7	void error(void)
[ 0:07]      8	{
[ 0:07]      9	
[ 0:07]     10	  {
[ 0:07]     11	  ERROR: __VERIFIER_error(); /* ERROR */
[ 0:07]     12	  return;
[ 0:07]     13	}
[ 0:07]     14	}
[ 0:07]     15	
[ 0:07]     16	void immediate_notify(void) ;
[ 0:07]     17	int max_loop ;
[ 0:07]     18	int num ;
[ 0:07]     19	int i  ;
[ 0:07]     20	int e  ;
[ 0:07]     21	int timer ;
[ 0:07]     22	char data_0  ;
[ 0:07]     23	char data_1  ;
[ 0:07]     24	char read_data(int i___0 )
[ 0:07]     25	{ char c ;
[ 0:07]     26	  char __retres3 ;
[ 0:07]     27	
[ 0:07]     28	  {
[ 0:07]     29	  if (i___0 == 0) {
[ 0:07]     30	    __retres3 = data_0;
[ 0:07]     31	    goto return_label;
[ 0:07]     32	  } else {
[ 0:07]     33	    if (i___0 == 1) {
[ 0:07]     34	      __retres3 = data_1;
[ 0:07]     35	      goto return_label;
[ 0:07]     36	    } else {
[ 0:07]     37	      {
[ 0:07]     38		error();
[ 0:07]     39	      }
[ 0:07]     40	    }
[ 0:07]     41	  }
[ 0:07]     42	  __retres3 = c;
[ 0:07]     43	  return_label: /* CIL Label */
[ 0:07]     44	  return (__retres3);
[ 0:07]     45	}
[ 0:07]     46	}
[ 0:07]     47	void write_data(int i___0 , char c )
[ 0:07]     48	{
[ 0:07]     49	
[ 0:07]     50	  {
[ 0:07]     51	  if (i___0 == 0) {
[ 0:07]     52	    data_0 = c;
[ 0:07]     53	  } else {
[ 0:07]     54	    if (i___0 == 1) {
[ 0:07]     55	      data_1 = c;
[ 0:07]     56	    } else {
[ 0:07]     57	      {
[ 0:07]     58		error();
[ 0:07]     59	      }
[ 0:07]     60	    }
[ 0:07]     61	  }
[ 0:07]     62	
[ 0:07]     63	  return;
[ 0:07]     64	}
[ 0:07]     65	}
[ 0:07]     66	int P_1_pc;
[ 0:07]     67	int P_1_st  ;
[ 0:07]     68	int P_1_i  ;
[ 0:07]     69	int P_1_ev  ;
[ 0:07]     70	void P_1(void)
[ 0:07]     71	{
[ 0:07]     72	
[ 0:07]     73	  {
[ 0:07]     74	  if ((int )P_1_pc == 0) {
[ 0:07]     75	    goto P_1_ENTRY_LOC;
[ 0:07]     76	  } else {
[ 0:07]     77	    if ((int )P_1_pc == 1) {
[ 0:07]     78	      goto P_1_WAIT_LOC;
[ 0:07]     79	    } else {
[ 0:07]     80	
[ 0:07]     81	    }
[ 0:07]     82	  }
[ 0:07]     83	  P_1_ENTRY_LOC:
[ 0:07]     84	  {
[ 0:07]     85	  while (i < max_loop) {
[ 0:07]     86	    while_0_continue: /* CIL Label */ ;
[ 0:07]     87	    {
[ 0:07]     88	    write_data(num, 'A');
[ 0:07]     89	    num += 1;
[ 0:07]     90	    P_1_pc = 1;
[ 0:07]     91	    P_1_st = 2;
[ 0:07]     92	    }
[ 0:07]     93	
[ 0:07]     94	    goto return_label;
[ 0:07]     95	    P_1_WAIT_LOC: ;
[ 0:07]     96	  }
[ 0:07]     97	  while_0_break: /* CIL Label */ ;
[ 0:07]     98	  }
[ 0:07]     99	  P_1_st = 2;
[ 0:07]    100	
[ 0:07]    101	  return_label: /* CIL Label */
[ 0:07]    102	  return;
[ 0:07]    103	}
[ 0:07]    104	}
[ 0:07]    105	int is_P_1_triggered(void)
[ 0:07]    106	{ int __retres1 ;
[ 0:07]    107	
[ 0:07]    108	  {
[ 0:07]    109	  if ((int )P_1_pc == 1) {
[ 0:07]    110	    if ((int )P_1_ev == 1) {
[ 0:07]    111	      __retres1 = 1;
[ 0:07]    112	      goto return_label;
[ 0:07]    113	    } else {
[ 0:07]    114	
[ 0:07]    115	    }
[ 0:07]    116	  } else {
[ 0:07]    117	
[ 0:07]    118	  }
[ 0:07]    119	  __retres1 = 0;
[ 0:07]    120	  return_label: /* CIL Label */
[ 0:07]    121	  return (__retres1);
[ 0:07]    122	}
[ 0:07]    123	}
[ 0:07]    124	int P_2_pc  ;
[ 0:07]    125	int P_2_st  ;
[ 0:07]    126	int P_2_i  ;
[ 0:07]    127	int P_2_ev  ;
[ 0:07]    128	void P_2(void)
[ 0:07]    129	{
[ 0:07]    130	
[ 0:07]    131	  {
[ 0:07]    132	  if ((int )P_2_pc == 0) {
[ 0:07]    133	    goto P_2_ENTRY_LOC;
[ 0:07]    134	  } else {
[ 0:07]    135	    if ((int )P_2_pc == 1) {
[ 0:07]    136	      goto P_2_WAIT_LOC;
[ 0:07]    137	    } else {
[ 0:07]    138	
[ 0:07]    139	    }
[ 0:07]    140	  }
[ 0:07]    141	  P_2_ENTRY_LOC:
[ 0:07]    142	  {
[ 0:07]    143	  while (i < max_loop) {
[ 0:07]    144	    while_1_continue: /* CIL Label */ ;
[ 0:07]    145	    {
[ 0:07]    146	    write_data(num, 'B');
[ 0:07]    147	    num += 1;
[ 0:07]    148	    }
[ 0:07]    149	    if (timer) {
[ 0:07]    150	      {
[ 0:07]    151	      timer = 0;
[ 0:07]    152	      e = 1;
[ 0:07]    153	      immediate_notify();
[ 0:07]    154	      e = 2;
[ 0:07]    155	      }
[ 0:07]    156	    } else {
[ 0:07]    157	
[ 0:07]    158	    }
[ 0:07]    159	    P_2_pc = 1;
[ 0:07]    160	    P_2_st = 2;
[ 0:07]    161	
[ 0:07]    162	    goto return_label;
[ 0:07]    163	    P_2_WAIT_LOC: ;
[ 0:07]    164	  }
[ 0:07]    165	  while_1_break: /* CIL Label */ ;
[ 0:07]    166	  }
[ 0:07]    167	  P_2_st = 2;
[ 0:07]    168	
[ 0:07]    169	  return_label: /* CIL Label */
[ 0:07]    170	  return;
[ 0:07]    171	}
[ 0:07]    172	}
[ 0:07]    173	int is_P_2_triggered(void)
[ 0:07]    174	{ int __retres1 ;
[ 0:07]    175	
[ 0:07]    176	  {
[ 0:07]    177	  if ((int )P_2_pc == 1) {
[ 0:07]    178	    if ((int )P_2_ev == 1) {
[ 0:07]    179	      __retres1 = 1;
[ 0:07]    180	      goto return_label;
[ 0:07]    181	    } else {
[ 0:07]    182	
[ 0:07]    183	    }
[ 0:07]    184	  } else {
[ 0:07]    185	
[ 0:07]    186	  }
[ 0:07]    187	  __retres1 = 0;
[ 0:07]    188	  return_label: /* CIL Label */
[ 0:07]    189	  return (__retres1);
[ 0:07]    190	}
[ 0:07]    191	}
[ 0:07]    192	int C_1_pc  ;
[ 0:07]    193	int C_1_st  ;
[ 0:07]    194	int C_1_i  ;
[ 0:07]    195	int C_1_ev  ;
[ 0:07]    196	int C_1_pr  ;
[ 0:07]    197	void C_1(void)
[ 0:07]    198	{ char c ;
[ 0:07]    199	
[ 0:07]    200	  {
[ 0:07]    201	  if ((int )C_1_pc == 0) {
[ 0:07]    202	    goto C_1_ENTRY_LOC;
[ 0:07]    203	  } else {
[ 0:07]    204	    if ((int )C_1_pc == 1) {
[ 0:07]    205	      goto C_1_WAIT_1_LOC;
[ 0:07]    206	    } else {
[ 0:07]    207	      if ((int )C_1_pc == 2) {
[ 0:07]    208	        goto C_1_WAIT_2_LOC;
[ 0:07]    209	      } else {
[ 0:07]    210	
[ 0:07]    211	      }
[ 0:07]    212	    }
[ 0:07]    213	  }
[ 0:07]    214	  C_1_ENTRY_LOC:
[ 0:07]    215	  {
[ 0:07]    216	  while (i < max_loop) {
[ 0:07]    217	    while_2_continue: /* CIL Label */ ;
[ 0:07]    218	    if (num == 0) {
[ 0:07]    219	      timer = 1;
[ 0:07]    220	      i += 1;
[ 0:07]    221	      C_1_pc = 1;
[ 0:07]    222	      C_1_st = 2;
[ 0:07]    223	
[ 0:07]    224	      goto return_label;
[ 0:07]    225	      C_1_WAIT_1_LOC: ;
[ 0:07]    226	    } else {
[ 0:07]    227	
[ 0:07]    228	    }
[ 0:07]    229	    num -= 1;
[ 0:07]    230	    if (! (num >= 0)) {
[ 0:07]    231	      {
[ 0:07]    232		error();
[ 0:07]    233	      }
[ 0:07]    234	    } else {
[ 0:07]    235	
[ 0:07]    236	    }
[ 0:07]    237	    {
[ 0:07]    238	    c = read_data(num);
[ 0:07]    239	    i += 1;
[ 0:07]    240	    C_1_pc = 2;
[ 0:07]    241	    C_1_st = 2;
[ 0:07]    242	    }
[ 0:07]    243	
[ 0:07]    244	    goto return_label;
[ 0:07]    245	    C_1_WAIT_2_LOC: ;
[ 0:07]    246	  }
[ 0:07]    247	  while_2_break: /* CIL Label */ ;
[ 0:07]    248	  }
[ 0:07]    249	  C_1_st = 2;
[ 0:07]    250	
[ 0:07]    251	  return_label: /* CIL Label */
[ 0:07]    252	  return;
[ 0:07]    253	}
[ 0:07]    254	}
[ 0:07]    255	int is_C_1_triggered(void)
[ 0:07]    256	{ int __retres1 ;
[ 0:07]    257	
[ 0:07]    258	  {
[ 0:07]    259	  if ((int )C_1_pc == 1) {
[ 0:07]    260	    if ((int )e == 1) {
[ 0:07]    261	      __retres1 = 1;
[ 0:07]    262	      goto return_label;
[ 0:07]    263	    } else {
[ 0:07]    264	
[ 0:07]    265	    }
[ 0:07]    266	  } else {
[ 0:07]    267	
[ 0:07]    268	  }
[ 0:07]    269	  if ((int )C_1_pc == 2) {
[ 0:07]    270	    if ((int )C_1_ev == 1) {
[ 0:07]    271	      __retres1 = 1;
[ 0:07]    272	      goto return_label;
[ 0:07]    273	    } else {
[ 0:07]    274	
[ 0:07]    275	    }
[ 0:07]    276	  } else {
[ 0:07]    277	
[ 0:07]    278	  }
[ 0:07]    279	  __retres1 = 0;
[ 0:07]    280	  return_label: /* CIL Label */
[ 0:07]    281	  return (__retres1);
[ 0:07]    282	}
[ 0:07]    283	}
[ 0:07]    284	void update_channels(void)
[ 0:07]    285	{
[ 0:07]    286	
[ 0:07]    287	  {
[ 0:07]    288	
[ 0:07]    289	  return;
[ 0:07]    290	}
[ 0:07]    291	}
[ 0:07]    292	void init_threads(void)
[ 0:07]    293	{
[ 0:07]    294	
[ 0:07]    295	  {
[ 0:07]    296	  if ((int )P_1_i == 1) {
[ 0:07]    297	    P_1_st = 0;
[ 0:07]    298	  } else {
[ 0:07]    299	    P_1_st = 2;
[ 0:07]    300	  }
[ 0:07]    301	  if ((int )P_2_i == 1) {
[ 0:07]    302	    P_2_st = 0;
[ 0:07]    303	  } else {
[ 0:07]    304	    P_2_st = 2;
[ 0:07]    305	  }
[ 0:07]    306	  if ((int )C_1_i == 1) {
[ 0:07]    307	    C_1_st = 0;
[ 0:07]    308	  } else {
[ 0:07]    309	    C_1_st = 2;
[ 0:07]    310	  }
[ 0:07]    311	
[ 0:07]    312	  return;
[ 0:07]    313	}
[ 0:07]    314	}
[ 0:07]    315	int exists_runnable_thread(void)
[ 0:07]    316	{ int __retres1 ;
[ 0:07]    317	
[ 0:07]    318	  {
[ 0:07]    319	  if ((int )P_1_st == 0) {
[ 0:07]    320	    __retres1 = 1;
[ 0:07]    321	    goto return_label;
[ 0:07]    322	  } else {
[ 0:07]    323	    if ((int )P_2_st == 0) {
[ 0:07]    324	      __retres1 = 1;
[ 0:07]    325	      goto return_label;
[ 0:07]    326	    } else {
[ 0:07]    327	      if ((int )C_1_st == 0) {
[ 0:07]    328	        __retres1 = 1;
[ 0:07]    329	        goto return_label;
[ 0:07]    330	      } else {
[ 0:07]    331	
[ 0:07]    332	      }
[ 0:07]    333	    }
[ 0:07]    334	  }
[ 0:07]    335	  __retres1 = 0;
[ 0:07]    336	  return_label: /* CIL Label */
[ 0:07]    337	  return (__retres1);
[ 0:07]    338	}
[ 0:07]    339	}
[ 0:07]    340	void eval(void)
[ 0:07]    341	{ int tmp ;
[ 0:07]    342	  int tmp___0 ;
[ 0:07]    343	  int tmp___1 ;
[ 0:07]    344	  int tmp___2 ;
[ 0:07]    345	
[ 0:07]    346	  {
[ 0:07]    347	  {
[ 0:07]    348	  while (1) {
[ 0:07]    349	    while_3_continue: /* CIL Label */ ;
[ 0:07]    350	    {
[ 0:07]    351	    tmp___2 = exists_runnable_thread();
[ 0:07]    352	    }
[ 0:07]    353	    if (tmp___2) {
[ 0:07]    354	
[ 0:07]    355	    } else {
[ 0:07]    356	      goto while_3_break;
[ 0:07]    357	    }
[ 0:07]    358	    if ((int )P_1_st == 0) {
[ 0:07]    359	      {
[ 0:07]    360	      tmp = __VERIFIER_nondet_int();
[ 0:07]    361	      }
[ 0:07]    362	      if (tmp) {
[ 0:07]    363	        {
[ 0:07]    364	        P_1_st = 1;
[ 0:07]    365	        P_1();
[ 0:07]    366	        }
[ 0:07]    367	      } else {
[ 0:07]    368	
[ 0:07]    369	      }
[ 0:07]    370	    } else {
[ 0:07]    371	
[ 0:07]    372	    }
[ 0:07]    373	    if ((int )P_2_st == 0) {
[ 0:07]    374	      {
[ 0:07]    375	      tmp___0 = __VERIFIER_nondet_int();
[ 0:07]    376	      }
[ 0:07]    377	      if (tmp___0) {
[ 0:07]    378	        {
[ 0:07]    379	        P_2_st = 1;
[ 0:07]    380	        P_2();
[ 0:07]    381	        }
[ 0:07]    382	      } else {
[ 0:07]    383	
[ 0:07]    384	      }
[ 0:07]    385	    } else {
[ 0:07]    386	
[ 0:07]    387	    }
[ 0:07]    388	    if ((int )C_1_st == 0) {
[ 0:07]    389	      {
[ 0:07]    390		tmp___1 = __VERIFIER_nondet_int();
[ 0:07]    391	      }
[ 0:07]    392	      if (tmp___1) {
[ 0:07]    393	        {
[ 0:07]    394	        C_1_st = 1;
[ 0:07]    395	        C_1();
[ 0:07]    396	        }
[ 0:07]    397	      } else {
[ 0:07]    398	
[ 0:07]    399	      }
[ 0:07]    400	    } else {
[ 0:07]    401	
[ 0:07]    402	    }
[ 0:07]    403	  }
[ 0:07]    404	  while_3_break: /* CIL Label */ ;
[ 0:07]    405	  }
[ 0:07]    406	
[ 0:07]    407	  return;
[ 0:07]    408	}
[ 0:07]    409	}
[ 0:07]    410	void fire_delta_events(void)
[ 0:07]    411	{
[ 0:07]    412	
[ 0:07]    413	  {
[ 0:07]    414	
[ 0:07]    415	  return;
[ 0:07]    416	}
[ 0:07]    417	}
[ 0:07]    418	void reset_delta_events(void)
[ 0:07]    419	{
[ 0:07]    420	
[ 0:07]    421	  {
[ 0:07]    422	
[ 0:07]    423	  return;
[ 0:07]    424	}
[ 0:07]    425	}
[ 0:07]    426	void fire_time_events(void)
[ 0:07]    427	{
[ 0:07]    428	
[ 0:07]    429	  {
[ 0:07]    430	  C_1_ev = 1;
[ 0:07]    431	  P_1_ev = 1;
[ 0:07]    432	  P_2_ev = 1;
[ 0:07]    433	
[ 0:07]    434	  return;
[ 0:07]    435	}
[ 0:07]    436	}
[ 0:07]    437	void reset_time_events(void)
[ 0:07]    438	{
[ 0:07]    439	
[ 0:07]    440	  {
[ 0:07]    441	  if ((int )P_1_ev == 1) {
[ 0:07]    442	    P_1_ev = 2;
[ 0:07]    443	  } else {
[ 0:07]    444	
[ 0:07]    445	  }
[ 0:07]    446	  if ((int )P_2_ev == 1) {
[ 0:07]    447	    P_2_ev = 2;
[ 0:07]    448	  } else {
[ 0:07]    449	
[ 0:07]    450	  }
[ 0:07]    451	  if ((int )C_1_ev == 1) {
[ 0:07]    452	    C_1_ev = 2;
[ 0:07]    453	  } else {
[ 0:07]    454	
[ 0:07]    455	  }
[ 0:07]    456	
[ 0:07]    457	  return;
[ 0:07]    458	}
[ 0:07]    459	}
[ 0:07]    460	void activate_threads(void)
[ 0:07]    461	{ int tmp ;
[ 0:07]    462	  int tmp___0 ;
[ 0:07]    463	  int tmp___1 ;
[ 0:07]    464	
[ 0:07]    465	  {
[ 0:07]    466	  {
[ 0:07]    467	  tmp = is_P_1_triggered();
[ 0:07]    468	  }
[ 0:07]    469	  if (tmp) {
[ 0:07]    470	    P_1_st = 0;
[ 0:07]    471	  } else {
[ 0:07]    472	
[ 0:07]    473	  }
[ 0:07]    474	  {
[ 0:07]    475	  tmp___0 = is_P_2_triggered();
[ 0:07]    476	  }
[ 0:07]    477	  if (tmp___0) {
[ 0:07]    478	    P_2_st = 0;
[ 0:07]    479	  } else {
[ 0:07]    480	
[ 0:07]    481	  }
[ 0:07]    482	  {
[ 0:07]    483	  tmp___1 = is_C_1_triggered();
[ 0:07]    484	  }
[ 0:07]    485	  if (tmp___1) {
[ 0:07]    486	    C_1_st = 0;
[ 0:07]    487	  } else {
[ 0:07]    488	
[ 0:07]    489	  }
[ 0:07]    490	
[ 0:07]    491	  return;
[ 0:07]    492	}
[ 0:07]    493	}
[ 0:07]    494	void immediate_notify(void)
[ 0:07]    495	{
[ 0:07]    496	
[ 0:07]    497	  {
[ 0:07]    498	  {
[ 0:07]    499	  activate_threads();
[ 0:07]    500	  }
[ 0:07]    501	
[ 0:07]    502	  return;
[ 0:07]    503	}
[ 0:07]    504	}
[ 0:07]    505	int stop_simulation(void)
[ 0:07]    506	{ int tmp ;
[ 0:07]    507	  int __retres2 ;
[ 0:07]    508	
[ 0:07]    509	  {
[ 0:07]    510	  {
[ 0:07]    511	  tmp = exists_runnable_thread();
[ 0:07]    512	  }
[ 0:07]    513	  if (tmp) {
[ 0:07]    514	    __retres2 = 0;
[ 0:07]    515	    goto return_label;
[ 0:07]    516	  } else {
[ 0:07]    517	
[ 0:07]    518	  }
[ 0:07]    519	  __retres2 = 1;
[ 0:07]    520	  return_label: /* CIL Label */
[ 0:07]    521	  return (__retres2);
[ 0:07]    522	}
[ 0:07]    523	}
[ 0:07]    524	void start_simulation(void)
[ 0:07]    525	{ int kernel_st ;
[ 0:07]    526	  int tmp ;
[ 0:07]    527	  int tmp___0 ;
[ 0:07]    528	
[ 0:07]    529	  {
[ 0:07]    530	  {
[ 0:07]    531	  kernel_st = 0;
[ 0:07]    532	  update_channels();
[ 0:07]    533	  init_threads();
[ 0:07]    534	  fire_delta_events();
[ 0:07]    535	  activate_threads();
[ 0:07]    536	  reset_delta_events();
[ 0:07]    537	  }
[ 0:07]    538	  {
[ 0:07]    539	  while (1) {
[ 0:07]    540	    while_4_continue: /* CIL Label */ ;
[ 0:07]    541	    {
[ 0:07]    542	    kernel_st = 1;
[ 0:07]    543	    eval();
[ 0:07]    544	    }
[ 0:07]    545	    {
[ 0:07]    546	    kernel_st = 2;
[ 0:07]    547	    update_channels();
[ 0:07]    548	    }
[ 0:07]    549	    {
[ 0:07]    550	    kernel_st = 3;
[ 0:07]    551	    fire_delta_events();
[ 0:07]    552	    activate_threads();
[ 0:07]    553	    reset_delta_events();
[ 0:07]    554	    }
[ 0:07]    555	    {
[ 0:07]    556	    tmp = exists_runnable_thread();
[ 0:07]    557	    }
[ 0:07]    558	    if (tmp == 0) {
[ 0:07]    559	      {
[ 0:07]    560	      kernel_st = 4;
[ 0:07]    561	      fire_time_events();
[ 0:07]    562	      activate_threads();
[ 0:07]    563	      reset_time_events();
[ 0:07]    564	      }
[ 0:07]    565	    } else {
[ 0:07]    566	
[ 0:07]    567	    }
[ 0:07]    568	    {
[ 0:07]    569	    tmp___0 = stop_simulation();
[ 0:07]    570	    }
[ 0:07]    571	    if (tmp___0) {
[ 0:07]    572	      goto while_4_break;
[ 0:07]    573	    } else {
[ 0:07]    574	
[ 0:07]    575	    }
[ 0:07]    576	  }
[ 0:07]    577	  while_4_break: /* CIL Label */ ;
[ 0:07]    578	  }
[ 0:07]    579	
[ 0:07]    580	  return;
[ 0:07]    581	}
[ 0:07]    582	}
[ 0:07]    583	void init_model(void)
[ 0:07]    584	{
[ 0:07]    585	
[ 0:07]    586	  {
[ 0:07]    587	  P_1_i = 1;
[ 0:07]    588	  P_2_i = 1;
[ 0:07]    589	  C_1_i = 1;
[ 0:07]    590	
[ 0:07]    591	  return;
[ 0:07]    592	}
[ 0:07]    593	}
[ 0:07]    594	int main(void)
[ 0:07]    595	{ int count ;
[ 0:07]    596	  int __retres2 ;
[ 0:07]    597	
[ 0:07]    598	  {
[ 0:07]    599	  {
[ 0:07]    600	  num  =    0;
[ 0:07]    601	  i  =    0;
[ 0:07]    602	  max_loop = 2;
[ 0:07]    603	  e  ;
[ 0:07]    604	  timer  =    0;
[ 0:07]    605	  P_1_pc  =    0;
[ 0:07]    606	  P_2_pc  =    0;
[ 0:07]    607	  C_1_pc  =    0;
[ 0:07]    608	
[ 0:07]    609	  count = 0;
[ 0:07]    610	  init_model();
[ 0:07]    611	  start_simulation();
[ 0:07]    612	  }
[ 0:07]    613	  __retres2 = 0;
[ 0:07]    614	  return (__retres2);
[ 0:07]    615	}
[ 0:07]    616	}
[ 0:07]    617	
[ 0:07]    618	
[ 0:07]    619	
[ 0:07] # expected error to be found at /home/xrockai/src/divine/nightly/test/svcomp/systemc/kundu2_false.cil.c:11, but it was not