extern void __VERIFIER_error() __attribute__ ((__noreturn__));

/**********************************************************************

Copyright (c) 2013 Carnegie Mellon University. All Rights Reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are
met:

1. Redistributions of source code must retain the above copyright
notice, this list of conditions and the following acknowledgments and
disclaimers.

2. Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.

3. The names "Carnegie Mellon University," "SEI" and/or "Software
Engineering Institute" shall not be used to endorse or promote
products derived from this software without prior written
permission. For written permission, please contact
permission@sei.cmu.edu.

4. Products derived from this software may not be called "SEI" nor may
"SEI" appear in their names without prior written permission of
permission@sei.cmu.edu.

5. Redistributions of any form whatsoever must retain the following
acknowledgment:

This material is based upon work funded and supported by the
Department of Defense under Contract No. FA8721-05-C-0003 with
Carnegie Mellon University for the operation of the Software
Engineering Institute, a federally funded research and development
center.

Any opinions, findings and conclusions or recommendations expressed in
this material are those of the author(s) and do not necessarily
reflect the views of the United States Department of Defense.

NO WARRANTY. THIS CARNEGIE MELLON UNIVERSITY AND SOFTWARE ENGINEERING
INSTITUTE MATERIAL IS FURNISHEDON AN "AS-IS" BASIS. CARNEGIE MELLON
UNIVERSITY MAKES NO WARRANTIES OF ANY KIND, EITHER EXPRESSED OR
IMPLIED, AS TO ANY MATTER INCLUDING, BUT NOT LIMITED TO, WARRANTY OF
FITNESS FOR PURPOSE OR MERCHANTABILITY, EXCLUSIVITY, OR RESULTS
OBTAINED FROM USE OF THE MATERIAL. CARNEGIE MELLON UNIVERSITY DOES NOT
MAKE ANY WARRANTY OF ANY KIND WITH RESPECT TO FREEDOM FROM PATENT,
TRADEMARK, OR COPYRIGHT INFRINGEMENT.

This material has been approved for public release and unlimited
distribution.

DM-0000575

**********************************************************************/

/* Generated by CIL v. 1.4.0 */
/* print_CIL_Input is true */

_Bool __startrek_Assert_t2_i0[24]  = 
     {1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1};
_Bool __startrek_Assert_t1_i0[2]  =    {1, 1};
_Bool __startrek_Assert_t0_i0[1]  =    {1};
unsigned char __startrek_start_t2[24]  ;
unsigned char __startrek_end_t2[24]  ;
unsigned char __startrek_start_t1[2]  ;
unsigned char __startrek_end_t1[2]  ;
unsigned char __startrek_start_t0[1]  ;
unsigned char __startrek_end_t0[1]  ;
void __startrek_init_shared(void) ;
__inline static void __startrek_assert_i0(_Bool arg ) ;
__inline static _Bool __startrek_cs_t2(void) ;
__inline static _Bool __startrek_cs_t1(void) ;
__inline static _Bool __startrek_cs_t0(void) ;
_Bool __VERIFIER_nondet_bool(void) ;
char __VERIFIER_nondet_char(void) ;
unsigned char __VERIFIER_nondet_uchar(void) ;
_Bool __VERIFIER_nondet_bool(void) ;
extern int __VERIFIER_nondet_int();
unsigned char __startrek_task  ;
unsigned char __startrek_job  ;
unsigned char __startrek_job_end  ;
unsigned char __startrek_error_round  ;
unsigned char __startrek_round  ;
_Bool __startrek_lock  =    (_Bool)0;
_Bool __startrek_is_first_cs  ;
unsigned char __startrek_hyper_period  ;
#pragma merger(0,"/tmp/aaaa/aso.ok2.i","-S")
extern void __startrek_cpu_lock(void) ;
extern void __startrek_cpu_unlock(void) ;
extern void __VERIFIER_assume(int  ) ;
void assert(_Bool arg) { if (!arg) { ERROR: __VERIFIER_error();} }
extern void __startrek_get_pi_lock(char lock_id ) ;
extern void __startrek_release_pi_lock(char lock_id ) ;
int __startrek_pi_locks_held  =    0;
char __startrek_priority_locks[1] ;
char __startrek_task_base_priority  =    0;
__inline static char __startrek_read___startrek_current_priority(void) ;
__inline static void __startrek_write___startrek_current_priority(char arg ) ;
char ___startrek_current_priority_[27]  ;
char _i___startrek_current_priority_[27]  ;
char __startrek_hidden___startrek_current_priority  =    0;
char __startrek_priority_locks[1]  = {      1};
static unsigned int ud_err_theta  ;
static unsigned int ud_psi  ;
static unsigned int ud_theta_lpf  ;
static unsigned int ud_theta_ref  ;
static unsigned int ud_thetadot_cmd_lpf  ;
extern unsigned int A_D ;
extern unsigned int A_R ;
extern unsigned int K_F[4] ;
extern unsigned int K_I ;
extern unsigned int K_PHIDOT ;
extern unsigned int K_THETADOT ;
extern unsigned int const   BATTERY_GAIN ;
extern unsigned int const   BATTERY_OFFSET ;
void balance_init(void) 
{ 


  {
  ud_err_theta = 0.0F;
  ud_theta_ref = 0.0F;
  ud_thetadot_cmd_lpf = 0.0F;
  ud_psi = 0.0F;
  ud_theta_lpf = 0.0F;
  return;
}
}
void balance_control(unsigned int args_cmd_forward , unsigned int args_cmd_turn ,
                     unsigned int args_gyro , unsigned int args_gyro_offset , unsigned int args_theta_m_l ,
                     unsigned int args_theta_m_r , unsigned int args_battery , char *ret_pwm_l ,
                     char *ret_pwm_r ) 
{ 
  unsigned int tmp_theta ;
  unsigned int tmp_theta_lpf ;
  unsigned int tmp_pwm_r_limiter ;
  unsigned int tmp_psidot ;
  unsigned int tmp_pwm_turn ;
  unsigned int tmp_pwm_l_limiter ;
  unsigned int tmp_thetadot_cmd_lpf ;
  unsigned int tmp[4] ;
  unsigned int tmp_theta_0[4] ;
  int tmp_0 ;
  int tmp___0 ;
  int tmp___1 ;

  {
  tmp_thetadot_cmd_lpf = (((float )args_cmd_forward / 100.0F) * (float )K_THETADOT) * (1.0F - (float )A_R) + (float )(A_R * ud_thetadot_cmd_lpf);
  tmp_theta = ((0.01745329238F * (float )args_theta_m_l + (float )ud_psi) + (0.01745329238F * (float )args_theta_m_r + (float )ud_psi)) * 0.5F;
  tmp_theta_lpf = (1.0F - (float )A_D) * (float )tmp_theta + (float )(A_D * ud_theta_lpf);
  tmp_psidot = (float )(args_gyro - args_gyro_offset) * 0.01745329238F;
  tmp[0] = ud_theta_ref;
  tmp[1] = 0.0F;
  tmp[2] = tmp_thetadot_cmd_lpf;
  tmp[3] = 0.0F;
  tmp_theta_0[0] = tmp_theta;
  tmp_theta_0[1] = ud_psi;
  tmp_theta_0[2] = (float )(tmp_theta_lpf - ud_theta_lpf) / 0.00400000019F;
  tmp_theta_0[3] = tmp_psidot;
  tmp_pwm_r_limiter = 0.0F;
  tmp_0 = 0;
  tmp_pwm_r_limiter += (tmp[tmp_0] - tmp_theta_0[tmp_0]) * K_F[tmp_0];
  tmp_0 ++;
  tmp_pwm_r_limiter += (tmp[tmp_0] - tmp_theta_0[tmp_0]) * K_F[tmp_0];
  tmp_0 ++;
  tmp_pwm_r_limiter += (tmp[tmp_0] - tmp_theta_0[tmp_0]) * K_F[tmp_0];
  tmp_0 ++;
  tmp_pwm_r_limiter += (tmp[tmp_0] - tmp_theta_0[tmp_0]) * K_F[tmp_0];
  tmp_0 ++;
  __VERIFIER_assume(((BATTERY_GAIN * args_battery) - BATTERY_OFFSET) != 0);
  tmp_pwm_r_limiter = (float )((K_I * ud_err_theta + tmp_pwm_r_limiter) / (unsigned int )(BATTERY_GAIN * (unsigned int const   )args_battery - BATTERY_OFFSET)) * 100.0F;
  tmp_pwm_turn = ((float )args_cmd_turn / 100.0F) * (float )K_PHIDOT;
  tmp_pwm_l_limiter = tmp_pwm_r_limiter + tmp_pwm_turn;
  tmp___0 = __VERIFIER_nondet_int();
  tmp_pwm_l_limiter = tmp___0;
  *ret_pwm_l = (char )tmp_pwm_l_limiter;
  tmp_pwm_r_limiter -= tmp_pwm_turn;
  tmp___1 = __VERIFIER_nondet_int();
  tmp_pwm_r_limiter = tmp___1;
  *ret_pwm_r = (char )tmp_pwm_r_limiter;
  tmp_pwm_l_limiter = 0.00400000019F * (float )tmp_thetadot_cmd_lpf + (float )ud_theta_ref;
  tmp_pwm_turn = 0.00400000019F * (float )tmp_psidot + (float )ud_psi;
  tmp_pwm_r_limiter = (float )(ud_theta_ref - tmp_theta) * 0.00400000019F + (float )ud_err_theta;
  ud_err_theta = tmp_pwm_r_limiter;
  ud_theta_ref = tmp_pwm_l_limiter;
  ud_thetadot_cmd_lpf = tmp_thetadot_cmd_lpf;
  ud_psi = tmp_pwm_turn;
  ud_theta_lpf = tmp_theta_lpf;
  return;
}
}
extern unsigned int __VERIFIER_nondet_U32() ;
extern char __VERIFIER_nondet_S8() ;
extern unsigned char __VERIFIER_nondet_uchar() ;
__inline static unsigned char __startrek_read_nxtway_gs_mode(void) ;
__inline static void __startrek_write_nxtway_gs_mode(unsigned char arg ) ;
unsigned char _nxtway_gs_mode_[27]  ;
unsigned char _i_nxtway_gs_mode_[27]  ;
unsigned char __startrek_hidden_nxtway_gs_mode  =    0;
__inline static _Bool __startrek_read_obstacle_flag(void) ;
__inline static void __startrek_write_obstacle_flag(_Bool arg ) ;
_Bool _obstacle_flag_[27]  ;
_Bool _i_obstacle_flag_[27]  ;
_Bool __startrek_hidden_obstacle_flag  =    0;
__inline static char __startrek_read_cmd_forward(void) ;
__inline static void __startrek_write_cmd_forward(char arg ) ;
char _cmd_forward_[27]  ;
char _i_cmd_forward_[27]  ;
char __startrek_hidden_cmd_forward  =    0;
__inline static char __startrek_read_cmd_turn(void) ;
__inline static void __startrek_write_cmd_turn(char arg ) ;
char _cmd_turn_[27]  ;
char _i_cmd_turn_[27]  ;
char __startrek_hidden_cmd_turn  =    0;
__inline static _Bool __startrek_read_trans(void) ;
__inline static void __startrek_write_trans(_Bool arg ) ;
_Bool _trans_[27]  ;
_Bool _i_trans_[27]  ;
_Bool __startrek_hidden_trans  =    0;
extern void nxt_motor_set_count(unsigned char port , char pwm ) ;
char nxt_motor_get_count(unsigned char port ) 
{ 
  char tmp ;

  {
  tmp = __VERIFIER_nondet_S8();
  return (tmp);
}
}
unsigned int ecrobot_get_systick_ms(void) ;
static unsigned int timer  =    0;
unsigned int ecrobot_get_systick_ms(void) 
{ 
  unsigned int r ;

  {
  r = timer;
  timer += 1000U;
  return (r);
}
}
unsigned int ecrobot_get_gyro_sensor(unsigned char port ) 
{ 
  unsigned int tmp ;

  {
  tmp = __VERIFIER_nondet_U32();
  return (tmp);
}
}
extern void ecrobot_sound_tone(unsigned int  , unsigned int  , char  ) ;
void ecrobot_read_bt_packet(unsigned char *bt_receive_buf , unsigned char sz ) 
{ 


  {
  *(bt_receive_buf + 0) = __VERIFIER_nondet_uchar();
  *(bt_receive_buf + 1) = __VERIFIER_nondet_uchar();
  return;
}
}
unsigned int ecrobot_get_battery_voltage(void) 
{ 
  unsigned int tmp ;

  {
  tmp = __VERIFIER_nondet_U32();
  return (tmp);
}
}
extern void nxt_motor_set_speed(unsigned char port , char speed , char one ) ;
extern void ecrobot_bt_data_logger(char  , char  ) ;
static unsigned int gyro_offset  ;
static unsigned int avg_cnt  ;
static unsigned int cal_start_time  ;
static char task_cmd_forward  ;
static char task_cmd_turn  ;
void OSEK_Task_ts1(void) 
{ 
  char pwm_l ;
  char pwm_r ;
  _Bool lobstacle ;
  unsigned char tmp ;
  unsigned int tmp___0 ;
  unsigned int tmp___1 ;
  _Bool tmp___2 ;
  char tmp___3 ;
  char tmp___4 ;
  _Bool tmp___5 ;
  unsigned int tmp___6 ;
  char tmp___7 ;
  char tmp___8 ;
  unsigned int tmp___9 ;

  {
  lobstacle = 0;
  tmp = __startrek_read_nxtway_gs_mode();
  switch (tmp) {
  case 0: 
  gyro_offset = 0;
  avg_cnt = 0;
  balance_init();
  nxt_motor_set_count(0, 0);
  nxt_motor_set_count(1, 0);
  cal_start_time = ecrobot_get_systick_ms();
  __startrek_write_nxtway_gs_mode(1);
  break;
  case 1: 
  tmp___0 = ecrobot_get_gyro_sensor(3);
  gyro_offset += tmp___0;
  avg_cnt ++;
  tmp___1 = ecrobot_get_systick_ms();
  if (tmp___1 - cal_start_time >= 1000U) {   
    __VERIFIER_assume(avg_cnt != 0); 
    gyro_offset /= avg_cnt;
    ecrobot_sound_tone(440U, 500U, 30);
    __startrek_write_nxtway_gs_mode(2);
  }
  break;
  case 2: 
  tmp___5 = __startrek_read_trans();
  if (! tmp___5) {
    tmp___2 = __startrek_read_obstacle_flag();
    lobstacle = tmp___2;
    tmp___3 = __startrek_read_cmd_turn();
    task_cmd_turn = tmp___3;
    tmp___4 = __startrek_read_cmd_forward();
    task_cmd_forward = tmp___4;
  }
  if (lobstacle) {
    __startrek_assert_i0((int )task_cmd_forward == -100 && (int )task_cmd_turn == 0);
  }
  tmp___6 = ecrobot_get_battery_voltage();
  tmp___7 = nxt_motor_get_count(1);
  tmp___8 = nxt_motor_get_count(0);
  tmp___9 = ecrobot_get_gyro_sensor(3);
  balance_control((unsigned int )task_cmd_forward, (unsigned int )task_cmd_turn, tmp___9,
                  gyro_offset, (unsigned int )tmp___8, (unsigned int )tmp___7, tmp___6,
                  & pwm_l, & pwm_r);
  nxt_motor_set_speed(0, pwm_l, 1);
  nxt_motor_set_speed(1, pwm_r, 1);
  break;
  default: 
  nxt_motor_set_speed(0, 0, 1);
  nxt_motor_set_speed(1, 0, 1);
  break;
  }
  return;
}
}
unsigned char ecrobot_get_sonar_sensor(unsigned char port ) 
{ 
  unsigned char tmp ;

  {
  tmp = __VERIFIER_nondet_uchar();
  return (tmp);
}
}
void OSEK_Task_ts2(void) 
{ 
  unsigned char tmp ;
  unsigned char tmp___0 ;

  {
  __startrek_write_obstacle_flag(0);
  tmp = __startrek_read_nxtway_gs_mode();
  if (tmp == 2) {
    tmp___0 = ecrobot_get_sonar_sensor(4);
    if ((int )tmp___0 <= 25) {
      __startrek_write_trans(1);
      __startrek_write_obstacle_flag(1);
      __startrek_write_cmd_forward(-100);
      __startrek_write_cmd_turn(0);
      __startrek_write_trans(0);
    }
  }
  return;
}
}
static unsigned char bt_receive_buf[2]  ;
void OSEK_Task_ts3(void) 
{ 
  int i ;
  _Bool wrote ;
  unsigned char tmp ;
  _Bool tmp___0 ;
  char tmp___1 ;
  char tmp___2 ;

  {
  wrote = 0;
  tmp = __startrek_read_nxtway_gs_mode();
  switch (tmp) {
  case 0: 
  i = 0;
  while (i < 2) {
    bt_receive_buf[i] = 0;
    i ++;
  }
  break;
  case 2: 
  ecrobot_read_bt_packet(bt_receive_buf, 2);
  wrote = 0;
  __startrek_get_pi_lock(0);
  tmp___0 = __startrek_read_obstacle_flag();
  if (! tmp___0) {
    __startrek_write_cmd_forward(- ((int )((char )bt_receive_buf[0])));
    __startrek_write_cmd_turn((char )bt_receive_buf[1]);
    wrote = 1;
  }
  __startrek_release_pi_lock(0);
  if (wrote) {
    tmp___1 = __startrek_read_cmd_turn();
    tmp___2 = __startrek_read_cmd_forward();
    ecrobot_bt_data_logger(tmp___2, tmp___1);
  }
  break;
  default: 
  break;
  }
  return;
}
}
char __startrek_base_priority_OSEK_Task_ts3  =    0;
__inline static _Bool __startrek_entry_pt_OSEK_Task_ts3(void) ;
__inline static _Bool __startrek_entry_pt_OSEK_Task_ts3(void) 
{ 


  {
  OSEK_Task_ts3();
  return ((_Bool)1);
}
}
void cil_keeperOSEK_Task_ts3(void) 
{ 


  {
  __startrek_entry_pt_OSEK_Task_ts3();
  return;
}
}
int __startrek_period_OSEK_Task_ts3  =    96;
int __startrek_wcet_OSEK_Task_ts3  =    48;
int __startrek_arrival_min_OSEK_Task_ts3  =    0;
int __startrek_arrival_max_OSEK_Task_ts3  =    0;
char __startrek_base_priority_OSEK_Task_ts2  =    1;
__inline static char __startrek_read___startrek_job_count_OSEK_Task_ts2(void) ;
__inline static void __startrek_write___startrek_job_count_OSEK_Task_ts2(char arg ) ;
char ___startrek_job_count_OSEK_Task_ts2_[27]  ;
char _i___startrek_job_count_OSEK_Task_ts2_[27]  ;
char __startrek_hidden___startrek_job_count_OSEK_Task_ts2  =    0;
__inline static _Bool __startrek_entry_pt_OSEK_Task_ts2(void) ;
__inline static _Bool __startrek_entry_pt_OSEK_Task_ts2(void) 
{ 
  char sp ;
  char tmp ;
  char tmp___0 ;

  {
  __startrek_lock = 1;
  tmp = __startrek_read___startrek_current_priority();
  sp = tmp;
  __startrek_lock = 0;
  if ((int )__startrek_base_priority_OSEK_Task_ts2 <= (int )sp) {
    __VERIFIER_assume(0);
    return ((_Bool)0);
  }
  __startrek_lock = 1;
  __startrek_write___startrek_current_priority(__startrek_base_priority_OSEK_Task_ts2);
  __startrek_lock = 0;
  __startrek_pi_locks_held = 0;
  __startrek_task_base_priority = __startrek_base_priority_OSEK_Task_ts2;
  OSEK_Task_ts2();
  __startrek_lock = 1;
  tmp___0 = __startrek_read___startrek_job_count_OSEK_Task_ts2();
  __startrek_write___startrek_job_count_OSEK_Task_ts2(tmp___0 + 1);
  __startrek_write___startrek_current_priority(sp);
  __startrek_lock = 0;
  return ((_Bool)1);
}
}
void cil_keeperOSEK_Task_ts2(void) 
{ 


  {
  __startrek_entry_pt_OSEK_Task_ts2();
  return;
}
}
int __startrek_period_OSEK_Task_ts2  =    48;
int __startrek_wcet_OSEK_Task_ts2  =    24;
int __startrek_arrival_min_OSEK_Task_ts2  =    0;
int __startrek_arrival_max_OSEK_Task_ts2  =    0;
char __startrek_base_priority_OSEK_Task_ts1  =    2;
__inline static char __startrek_read___startrek_job_count_OSEK_Task_ts1(void) ;
__inline static void __startrek_write___startrek_job_count_OSEK_Task_ts1(char arg ) ;
char ___startrek_job_count_OSEK_Task_ts1_[27]  ;
char _i___startrek_job_count_OSEK_Task_ts1_[27]  ;
char __startrek_hidden___startrek_job_count_OSEK_Task_ts1  =    0;
__inline static _Bool __startrek_entry_pt_OSEK_Task_ts1(void) ;
__inline static _Bool __startrek_entry_pt_OSEK_Task_ts1(void) 
{ 
  char sp ;
  char tmp ;
  char tmp___0 ;

  {
  __startrek_lock = 1;
  tmp = __startrek_read___startrek_current_priority();
  sp = tmp;
  __startrek_lock = 0;
  if ((int )__startrek_base_priority_OSEK_Task_ts1 <= (int )sp) {
    __VERIFIER_assume(0);
    return ((_Bool)0);
  }
  __startrek_lock = 1;
  __startrek_write___startrek_current_priority(__startrek_base_priority_OSEK_Task_ts1);
  __startrek_lock = 0;
  __startrek_pi_locks_held = 0;
  __startrek_task_base_priority = __startrek_base_priority_OSEK_Task_ts1;
  OSEK_Task_ts1();
  __startrek_lock = 1;
  tmp___0 = __startrek_read___startrek_job_count_OSEK_Task_ts1();
  __startrek_write___startrek_job_count_OSEK_Task_ts1(tmp___0 + 1);
  __startrek_write___startrek_current_priority(sp);
  __startrek_lock = 0;
  return ((_Bool)1);
}
}
void cil_keeperOSEK_Task_ts1(void) 
{ 


  {
  __startrek_entry_pt_OSEK_Task_ts1();
  return;
}
}
int __startrek_period_OSEK_Task_ts1  =    4;
int __startrek_wcet_OSEK_Task_ts1  =    1;
int __startrek_arrival_min_OSEK_Task_ts1  =    0;
int __startrek_arrival_max_OSEK_Task_ts1  =    0;
int __startrek_time_bound  =    96;
__inline void __startrek_schedule_jobs(void) 
{ 


  {
  __startrek_start_t0[0] = __VERIFIER_nondet_uchar();
  __startrek_end_t0[0] = __VERIFIER_nondet_uchar();
  __VERIFIER_assume(0 <= __startrek_start_t0[0]);
  __VERIFIER_assume(__startrek_end_t0[0] <= 26);
  __VERIFIER_assume(__startrek_start_t0[0] <= __startrek_end_t0[0]);
  __startrek_start_t1[0] = __VERIFIER_nondet_uchar();
  __startrek_end_t1[0] = __VERIFIER_nondet_uchar();
  __startrek_start_t1[1] = __VERIFIER_nondet_uchar();
  __startrek_end_t1[1] = __VERIFIER_nondet_uchar();
  __VERIFIER_assume(0 <= __startrek_start_t1[0]);
  __VERIFIER_assume(__startrek_end_t1[1] <= 26);
  __VERIFIER_assume(__startrek_start_t1[0] <= __startrek_end_t1[0]);
  __VERIFIER_assume(__startrek_start_t1[1] <= __startrek_end_t1[1]);
  __VERIFIER_assume(__startrek_end_t1[0] <= __startrek_start_t1[1] - 1);
  if (__startrek_start_t0[0] <= __startrek_end_t1[0]) {
    if (__startrek_start_t1[0] <= __startrek_end_t0[0]) {
      {
      __VERIFIER_assume(__startrek_start_t0[0] <= __startrek_start_t1[0]);
      __VERIFIER_assume(__startrek_end_t1[0] < __startrek_end_t0[0]);
      }
    }
  }
  if (__startrek_start_t0[0] <= __startrek_end_t1[1]) {
    if (__startrek_start_t1[1] <= __startrek_end_t0[0]) {
      {
      __VERIFIER_assume(__startrek_start_t0[0] <= __startrek_start_t1[1]);
      __VERIFIER_assume(__startrek_end_t1[1] < __startrek_end_t0[0]);
      }
    }
  }
  __startrek_start_t2[0] = __VERIFIER_nondet_uchar();
  __startrek_end_t2[0] = __startrek_start_t2[0];
  __startrek_start_t2[1] = __VERIFIER_nondet_uchar();
  __startrek_end_t2[1] = __startrek_start_t2[1];
  __startrek_start_t2[2] = __VERIFIER_nondet_uchar();
  __startrek_end_t2[2] = __startrek_start_t2[2];
  __startrek_start_t2[3] = __VERIFIER_nondet_uchar();
  __startrek_end_t2[3] = __startrek_start_t2[3];
  __startrek_start_t2[4] = __VERIFIER_nondet_uchar();
  __startrek_end_t2[4] = __startrek_start_t2[4];
  __startrek_start_t2[5] = __VERIFIER_nondet_uchar();
  __startrek_end_t2[5] = __startrek_start_t2[5];
  __startrek_start_t2[6] = __VERIFIER_nondet_uchar();
  __startrek_end_t2[6] = __startrek_start_t2[6];
  __startrek_start_t2[7] = __VERIFIER_nondet_uchar();
  __startrek_end_t2[7] = __startrek_start_t2[7];
  __startrek_start_t2[8] = __VERIFIER_nondet_uchar();
  __startrek_end_t2[8] = __startrek_start_t2[8];
  __startrek_start_t2[9] = __VERIFIER_nondet_uchar();
  __startrek_end_t2[9] = __startrek_start_t2[9];
  __startrek_start_t2[10] = __VERIFIER_nondet_uchar();
  __startrek_end_t2[10] = __startrek_start_t2[10];
  __startrek_start_t2[11] = __VERIFIER_nondet_uchar();
  __startrek_end_t2[11] = __startrek_start_t2[11];
  __startrek_start_t2[12] = __VERIFIER_nondet_uchar();
  __startrek_end_t2[12] = __startrek_start_t2[12];
  __startrek_start_t2[13] = __VERIFIER_nondet_uchar();
  __startrek_end_t2[13] = __startrek_start_t2[13];
  __startrek_start_t2[14] = __VERIFIER_nondet_uchar();
  __startrek_end_t2[14] = __startrek_start_t2[14];
  __startrek_start_t2[15] = __VERIFIER_nondet_uchar();
  __startrek_end_t2[15] = __startrek_start_t2[15];
  __startrek_start_t2[16] = __VERIFIER_nondet_uchar();
  __startrek_end_t2[16] = __startrek_start_t2[16];
  __startrek_start_t2[17] = __VERIFIER_nondet_uchar();
  __startrek_end_t2[17] = __startrek_start_t2[17];
  __startrek_start_t2[18] = __VERIFIER_nondet_uchar();
  __startrek_end_t2[18] = __startrek_start_t2[18];
  __startrek_start_t2[19] = __VERIFIER_nondet_uchar();
  __startrek_end_t2[19] = __startrek_start_t2[19];
  __startrek_start_t2[20] = __VERIFIER_nondet_uchar();
  __startrek_end_t2[20] = __startrek_start_t2[20];
  __startrek_start_t2[21] = __VERIFIER_nondet_uchar();
  __startrek_end_t2[21] = __startrek_start_t2[21];
  __startrek_start_t2[22] = __VERIFIER_nondet_uchar();
  __startrek_end_t2[22] = __startrek_start_t2[22];
  __startrek_start_t2[23] = __VERIFIER_nondet_uchar();
  __startrek_end_t2[23] = __startrek_start_t2[23];
  __VERIFIER_assume(0 <= __startrek_start_t2[0]);
  __VERIFIER_assume(__startrek_end_t2[23] <= 26);
  __VERIFIER_assume(__startrek_end_t2[0] <= __startrek_start_t2[1] - 1);
  __VERIFIER_assume(__startrek_end_t2[1] <= __startrek_start_t2[2] - 1);
  __VERIFIER_assume(__startrek_end_t2[2] <= __startrek_start_t2[3] - 1);
  __VERIFIER_assume(__startrek_end_t2[3] <= __startrek_start_t2[4] - 1);
  __VERIFIER_assume(__startrek_end_t2[4] <= __startrek_start_t2[5] - 1);
  __VERIFIER_assume(__startrek_end_t2[5] <= __startrek_start_t2[6] - 1);
  __VERIFIER_assume(__startrek_end_t2[6] <= __startrek_start_t2[7] - 1);
  __VERIFIER_assume(__startrek_end_t2[7] <= __startrek_start_t2[8] - 1);
  __VERIFIER_assume(__startrek_end_t2[8] <= __startrek_start_t2[9] - 1);
  __VERIFIER_assume(__startrek_end_t2[9] <= __startrek_start_t2[10] - 1);
  __VERIFIER_assume(__startrek_end_t2[10] <= __startrek_start_t2[11] - 1);
  __VERIFIER_assume(__startrek_end_t2[11] <= __startrek_start_t2[12] - 1);
  __VERIFIER_assume(__startrek_end_t2[12] <= __startrek_start_t2[13] - 1);
  __VERIFIER_assume(__startrek_end_t2[13] <= __startrek_start_t2[14] - 1);
  __VERIFIER_assume(__startrek_end_t2[14] <= __startrek_start_t2[15] - 1);
  __VERIFIER_assume(__startrek_end_t2[15] <= __startrek_start_t2[16] - 1);
  __VERIFIER_assume(__startrek_end_t2[16] <= __startrek_start_t2[17] - 1);
  __VERIFIER_assume(__startrek_end_t2[17] <= __startrek_start_t2[18] - 1);
  __VERIFIER_assume(__startrek_end_t2[18] <= __startrek_start_t2[19] - 1);
  __VERIFIER_assume(__startrek_end_t2[19] <= __startrek_start_t2[20] - 1);
  __VERIFIER_assume(__startrek_end_t2[20] <= __startrek_start_t2[21] - 1);
  __VERIFIER_assume(__startrek_end_t2[21] <= __startrek_start_t2[22] - 1);
  __VERIFIER_assume(__startrek_end_t2[22] <= __startrek_start_t2[23] - 1);
  if (__startrek_start_t0[0] <= __startrek_end_t2[0]) {
    if (__startrek_start_t2[0] <= __startrek_end_t0[0]) {
      {
      __VERIFIER_assume(__startrek_start_t0[0] <= __startrek_start_t2[0]);
      __VERIFIER_assume(__startrek_end_t2[0] < __startrek_end_t0[0]);
      }
    }
  }
  if (__startrek_start_t1[0] <= __startrek_end_t2[0]) {
    if (__startrek_start_t2[0] <= __startrek_end_t1[0]) {
      {
      __VERIFIER_assume(__startrek_start_t1[0] <= __startrek_start_t2[0]);
      __VERIFIER_assume(__startrek_end_t2[0] < __startrek_end_t1[0]);
      }
    }
  }
  if (__startrek_start_t1[1] <= __startrek_end_t2[0]) {
    if (__startrek_start_t2[0] <= __startrek_end_t1[1]) {
      {
      __VERIFIER_assume(__startrek_start_t1[1] <= __startrek_start_t2[0]);
      __VERIFIER_assume(__startrek_end_t2[0] < __startrek_end_t1[1]);
      }
    }
  }
  if (__startrek_start_t0[0] <= __startrek_end_t2[1]) {
    if (__startrek_start_t2[1] <= __startrek_end_t0[0]) {
      {
      __VERIFIER_assume(__startrek_start_t0[0] <= __startrek_start_t2[1]);
      __VERIFIER_assume(__startrek_end_t2[1] < __startrek_end_t0[0]);
      }
    }
  }
  if (__startrek_start_t1[0] <= __startrek_end_t2[1]) {
    if (__startrek_start_t2[1] <= __startrek_end_t1[0]) {
      {
      __VERIFIER_assume(__startrek_start_t1[0] <= __startrek_start_t2[1]);
      __VERIFIER_assume(__startrek_end_t2[1] < __startrek_end_t1[0]);
      }
    }
  }
  if (__startrek_start_t1[1] <= __startrek_end_t2[1]) {
    if (__startrek_start_t2[1] <= __startrek_end_t1[1]) {
      {
      __VERIFIER_assume(__startrek_start_t1[1] <= __startrek_start_t2[1]);
      __VERIFIER_assume(__startrek_end_t2[1] < __startrek_end_t1[1]);
      }
    }
  }
  if (__startrek_start_t0[0] <= __startrek_end_t2[2]) {
    if (__startrek_start_t2[2] <= __startrek_end_t0[0]) {
      {
      __VERIFIER_assume(__startrek_start_t0[0] <= __startrek_start_t2[2]);
      __VERIFIER_assume(__startrek_end_t2[2] < __startrek_end_t0[0]);
      }
    }
  }
  if (__startrek_start_t1[0] <= __startrek_end_t2[2]) {
    if (__startrek_start_t2[2] <= __startrek_end_t1[0]) {
      {
      __VERIFIER_assume(__startrek_start_t1[0] <= __startrek_start_t2[2]);
      __VERIFIER_assume(__startrek_end_t2[2] < __startrek_end_t1[0]);
      }
    }
  }
  if (__startrek_start_t1[1] <= __startrek_end_t2[2]) {
    if (__startrek_start_t2[2] <= __startrek_end_t1[1]) {
      {
      __VERIFIER_assume(__startrek_start_t1[1] <= __startrek_start_t2[2]);
      __VERIFIER_assume(__startrek_end_t2[2] < __startrek_end_t1[1]);
      }
    }
  }
  if (__startrek_start_t0[0] <= __startrek_end_t2[3]) {
    if (__startrek_start_t2[3] <= __startrek_end_t0[0]) {
      {
      __VERIFIER_assume(__startrek_start_t0[0] <= __startrek_start_t2[3]);
      __VERIFIER_assume(__startrek_end_t2[3] < __startrek_end_t0[0]);
      }
    }
  }
  if (__startrek_start_t1[0] <= __startrek_end_t2[3]) {
    if (__startrek_start_t2[3] <= __startrek_end_t1[0]) {
      {
      __VERIFIER_assume(__startrek_start_t1[0] <= __startrek_start_t2[3]);
      __VERIFIER_assume(__startrek_end_t2[3] < __startrek_end_t1[0]);
      }
    }
  }
  if (__startrek_start_t1[1] <= __startrek_end_t2[3]) {
    if (__startrek_start_t2[3] <= __startrek_end_t1[1]) {
      {
      __VERIFIER_assume(__startrek_start_t1[1] <= __startrek_start_t2[3]);
      __VERIFIER_assume(__startrek_end_t2[3] < __startrek_end_t1[1]);
      }
    }
  }
  if (__startrek_start_t0[0] <= __startrek_end_t2[4]) {
    if (__startrek_start_t2[4] <= __startrek_end_t0[0]) {
      {
      __VERIFIER_assume(__startrek_start_t0[0] <= __startrek_start_t2[4]);
      __VERIFIER_assume(__startrek_end_t2[4] < __startrek_end_t0[0]);
      }
    }
  }
  if (__startrek_start_t1[0] <= __startrek_end_t2[4]) {
    if (__startrek_start_t2[4] <= __startrek_end_t1[0]) {
      {
      __VERIFIER_assume(__startrek_start_t1[0] <= __startrek_start_t2[4]);
      __VERIFIER_assume(__startrek_end_t2[4] < __startrek_end_t1[0]);
      }
    }
  }
  if (__startrek_start_t1[1] <= __startrek_end_t2[4]) {
    if (__startrek_start_t2[4] <= __startrek_end_t1[1]) {
      {
      __VERIFIER_assume(__startrek_start_t1[1] <= __startrek_start_t2[4]);
      __VERIFIER_assume(__startrek_end_t2[4] < __startrek_end_t1[1]);
      }
    }
  }
  if (__startrek_start_t0[0] <= __startrek_end_t2[5]) {
    if (__startrek_start_t2[5] <= __startrek_end_t0[0]) {
      {
      __VERIFIER_assume(__startrek_start_t0[0] <= __startrek_start_t2[5]);
      __VERIFIER_assume(__startrek_end_t2[5] < __startrek_end_t0[0]);
      }
    }
  }
  if (__startrek_start_t1[0] <= __startrek_end_t2[5]) {
    if (__startrek_start_t2[5] <= __startrek_end_t1[0]) {
      {
      __VERIFIER_assume(__startrek_start_t1[0] <= __startrek_start_t2[5]);
      __VERIFIER_assume(__startrek_end_t2[5] < __startrek_end_t1[0]);
      }
    }
  }
  if (__startrek_start_t1[1] <= __startrek_end_t2[5]) {
    if (__startrek_start_t2[5] <= __startrek_end_t1[1]) {
      {
      __VERIFIER_assume(__startrek_start_t1[1] <= __startrek_start_t2[5]);
      __VERIFIER_assume(__startrek_end_t2[5] < __startrek_end_t1[1]);
      }
    }
  }
  if (__startrek_start_t0[0] <= __startrek_end_t2[6]) {
    if (__startrek_start_t2[6] <= __startrek_end_t0[0]) {
      {
      __VERIFIER_assume(__startrek_start_t0[0] <= __startrek_start_t2[6]);
      __VERIFIER_assume(__startrek_end_t2[6] < __startrek_end_t0[0]);
      }
    }
  }
  if (__startrek_start_t1[0] <= __startrek_end_t2[6]) {
    if (__startrek_start_t2[6] <= __startrek_end_t1[0]) {
      {
      __VERIFIER_assume(__startrek_start_t1[0] <= __startrek_start_t2[6]);
      __VERIFIER_assume(__startrek_end_t2[6] < __startrek_end_t1[0]);
      }
    }
  }
  if (__startrek_start_t1[1] <= __startrek_end_t2[6]) {
    if (__startrek_start_t2[6] <= __startrek_end_t1[1]) {
      {
      __VERIFIER_assume(__startrek_start_t1[1] <= __startrek_start_t2[6]);
      __VERIFIER_assume(__startrek_end_t2[6] < __startrek_end_t1[1]);
      }
    }
  }
  if (__startrek_start_t0[0] <= __startrek_end_t2[7]) {
    if (__startrek_start_t2[7] <= __startrek_end_t0[0]) {
      {
      __VERIFIER_assume(__startrek_start_t0[0] <= __startrek_start_t2[7]);
      __VERIFIER_assume(__startrek_end_t2[7] < __startrek_end_t0[0]);
      }
    }
  }
  if (__startrek_start_t1[0] <= __startrek_end_t2[7]) {
    if (__startrek_start_t2[7] <= __startrek_end_t1[0]) {
      {
      __VERIFIER_assume(__startrek_start_t1[0] <= __startrek_start_t2[7]);
      __VERIFIER_assume(__startrek_end_t2[7] < __startrek_end_t1[0]);
      }
    }
  }
  if (__startrek_start_t1[1] <= __startrek_end_t2[7]) {
    if (__startrek_start_t2[7] <= __startrek_end_t1[1]) {
      {
      __VERIFIER_assume(__startrek_start_t1[1] <= __startrek_start_t2[7]);
      __VERIFIER_assume(__startrek_end_t2[7] < __startrek_end_t1[1]);
      }
    }
  }
  if (__startrek_start_t0[0] <= __startrek_end_t2[8]) {
    if (__startrek_start_t2[8] <= __startrek_end_t0[0]) {
      {
      __VERIFIER_assume(__startrek_start_t0[0] <= __startrek_start_t2[8]);
      __VERIFIER_assume(__startrek_end_t2[8] < __startrek_end_t0[0]);
      }
    }
  }
  if (__startrek_start_t1[0] <= __startrek_end_t2[8]) {
    if (__startrek_start_t2[8] <= __startrek_end_t1[0]) {
      {
      __VERIFIER_assume(__startrek_start_t1[0] <= __startrek_start_t2[8]);
      __VERIFIER_assume(__startrek_end_t2[8] < __startrek_end_t1[0]);
      __VERIFIER_assume(__startrek_end_t2[0] < __startrek_start_t1[0]);
      }
    }
  }
  if (__startrek_start_t1[1] <= __startrek_end_t2[8]) {
    if (__startrek_start_t2[8] <= __startrek_end_t1[1]) {
      {
      __VERIFIER_assume(__startrek_start_t1[1] <= __startrek_start_t2[8]);
      __VERIFIER_assume(__startrek_end_t2[8] < __startrek_end_t1[1]);
      __VERIFIER_assume(__startrek_end_t2[0] < __startrek_start_t1[1]);
      }
    }
  }
  if (__startrek_start_t0[0] <= __startrek_end_t2[9]) {
    if (__startrek_start_t2[9] <= __startrek_end_t0[0]) {
      {
      __VERIFIER_assume(__startrek_start_t0[0] <= __startrek_start_t2[9]);
      __VERIFIER_assume(__startrek_end_t2[9] < __startrek_end_t0[0]);
      }
    }
  }
  if (__startrek_start_t1[0] <= __startrek_end_t2[9]) {
    if (__startrek_start_t2[9] <= __startrek_end_t1[0]) {
      {
      __VERIFIER_assume(__startrek_start_t1[0] <= __startrek_start_t2[9]);
      __VERIFIER_assume(__startrek_end_t2[9] < __startrek_end_t1[0]);
      __VERIFIER_assume(__startrek_end_t2[1] < __startrek_start_t1[0]);
      }
    }
  }
  if (__startrek_start_t1[1] <= __startrek_end_t2[9]) {
    if (__startrek_start_t2[9] <= __startrek_end_t1[1]) {
      {
      __VERIFIER_assume(__startrek_start_t1[1] <= __startrek_start_t2[9]);
      __VERIFIER_assume(__startrek_end_t2[9] < __startrek_end_t1[1]);
      __VERIFIER_assume(__startrek_end_t2[1] < __startrek_start_t1[1]);
      }
    }
  }
  if (__startrek_start_t0[0] <= __startrek_end_t2[10]) {
    if (__startrek_start_t2[10] <= __startrek_end_t0[0]) {
      {
      __VERIFIER_assume(__startrek_start_t0[0] <= __startrek_start_t2[10]);
      __VERIFIER_assume(__startrek_end_t2[10] < __startrek_end_t0[0]);
      }
    }
  }
  if (__startrek_start_t1[0] <= __startrek_end_t2[10]) {
    if (__startrek_start_t2[10] <= __startrek_end_t1[0]) {
      {
      __VERIFIER_assume(__startrek_start_t1[0] <= __startrek_start_t2[10]);
      __VERIFIER_assume(__startrek_end_t2[10] < __startrek_end_t1[0]);
      __VERIFIER_assume(__startrek_end_t2[2] < __startrek_start_t1[0]);
      }
    }
  }
  if (__startrek_start_t1[1] <= __startrek_end_t2[10]) {
    if (__startrek_start_t2[10] <= __startrek_end_t1[1]) {
      {
      __VERIFIER_assume(__startrek_start_t1[1] <= __startrek_start_t2[10]);
      __VERIFIER_assume(__startrek_end_t2[10] < __startrek_end_t1[1]);
      __VERIFIER_assume(__startrek_end_t2[2] < __startrek_start_t1[1]);
      }
    }
  }
  if (__startrek_start_t0[0] <= __startrek_end_t2[11]) {
    if (__startrek_start_t2[11] <= __startrek_end_t0[0]) {
      {
      __VERIFIER_assume(__startrek_start_t0[0] <= __startrek_start_t2[11]);
      __VERIFIER_assume(__startrek_end_t2[11] < __startrek_end_t0[0]);
      }
    }
  }
  if (__startrek_start_t1[0] <= __startrek_end_t2[11]) {
    if (__startrek_start_t2[11] <= __startrek_end_t1[0]) {
      {
      __VERIFIER_assume(__startrek_start_t1[0] <= __startrek_start_t2[11]);
      __VERIFIER_assume(__startrek_end_t2[11] < __startrek_end_t1[0]);
      __VERIFIER_assume(__startrek_end_t2[3] < __startrek_start_t1[0]);
      }
    }
  }
  if (__startrek_start_t1[1] <= __startrek_end_t2[11]) {
    if (__startrek_start_t2[11] <= __startrek_end_t1[1]) {
      {
      __VERIFIER_assume(__startrek_start_t1[1] <= __startrek_start_t2[11]);
      __VERIFIER_assume(__startrek_end_t2[11] < __startrek_end_t1[1]);
      __VERIFIER_assume(__startrek_end_t2[3] < __startrek_start_t1[1]);
      }
    }
  }
  if (__startrek_start_t0[0] <= __startrek_end_t2[12]) {
    if (__startrek_start_t2[12] <= __startrek_end_t0[0]) {
      {
      __VERIFIER_assume(__startrek_start_t0[0] <= __startrek_start_t2[12]);
      __VERIFIER_assume(__startrek_end_t2[12] < __startrek_end_t0[0]);
      }
    }
  }
  if (__startrek_start_t1[0] <= __startrek_end_t2[12]) {
    if (__startrek_start_t2[12] <= __startrek_end_t1[0]) {
      {
      __VERIFIER_assume(__startrek_start_t1[0] <= __startrek_start_t2[12]);
      __VERIFIER_assume(__startrek_end_t2[12] < __startrek_end_t1[0]);
      __VERIFIER_assume(__startrek_end_t2[4] < __startrek_start_t1[0]);
      }
    }
  }
  if (__startrek_start_t1[1] <= __startrek_end_t2[12]) {
    if (__startrek_start_t2[12] <= __startrek_end_t1[1]) {
      {
      __VERIFIER_assume(__startrek_start_t1[1] <= __startrek_start_t2[12]);
      __VERIFIER_assume(__startrek_end_t2[12] < __startrek_end_t1[1]);
      __VERIFIER_assume(__startrek_end_t2[4] < __startrek_start_t1[1]);
      }
    }
  }
  if (__startrek_start_t0[0] <= __startrek_end_t2[13]) {
    if (__startrek_start_t2[13] <= __startrek_end_t0[0]) {
      {
      __VERIFIER_assume(__startrek_start_t0[0] <= __startrek_start_t2[13]);
      __VERIFIER_assume(__startrek_end_t2[13] < __startrek_end_t0[0]);
      }
    }
  }
  if (__startrek_start_t1[0] <= __startrek_end_t2[13]) {
    if (__startrek_start_t2[13] <= __startrek_end_t1[0]) {
      {
      __VERIFIER_assume(__startrek_start_t1[0] <= __startrek_start_t2[13]);
      __VERIFIER_assume(__startrek_end_t2[13] < __startrek_end_t1[0]);
      __VERIFIER_assume(__startrek_end_t2[5] < __startrek_start_t1[0]);
      }
    }
  }
  if (__startrek_start_t1[1] <= __startrek_end_t2[13]) {
    if (__startrek_start_t2[13] <= __startrek_end_t1[1]) {
      {
      __VERIFIER_assume(__startrek_start_t1[1] <= __startrek_start_t2[13]);
      __VERIFIER_assume(__startrek_end_t2[13] < __startrek_end_t1[1]);
      __VERIFIER_assume(__startrek_end_t2[5] < __startrek_start_t1[1]);
      }
    }
  }
  if (__startrek_start_t0[0] <= __startrek_end_t2[14]) {
    if (__startrek_start_t2[14] <= __startrek_end_t0[0]) {
      {
      __VERIFIER_assume(__startrek_start_t0[0] <= __startrek_start_t2[14]);
      __VERIFIER_assume(__startrek_end_t2[14] < __startrek_end_t0[0]);
      }
    }
  }
  if (__startrek_start_t1[0] <= __startrek_end_t2[14]) {
    if (__startrek_start_t2[14] <= __startrek_end_t1[0]) {
      {
      __VERIFIER_assume(__startrek_start_t1[0] <= __startrek_start_t2[14]);
      __VERIFIER_assume(__startrek_end_t2[14] < __startrek_end_t1[0]);
      __VERIFIER_assume(__startrek_end_t2[6] < __startrek_start_t1[0]);
      }
    }
  }
  if (__startrek_start_t1[1] <= __startrek_end_t2[14]) {
    if (__startrek_start_t2[14] <= __startrek_end_t1[1]) {
      {
      __VERIFIER_assume(__startrek_start_t1[1] <= __startrek_start_t2[14]);
      __VERIFIER_assume(__startrek_end_t2[14] < __startrek_end_t1[1]);
      __VERIFIER_assume(__startrek_end_t2[6] < __startrek_start_t1[1]);
      }
    }
  }
  if (__startrek_start_t0[0] <= __startrek_end_t2[15]) {
    if (__startrek_start_t2[15] <= __startrek_end_t0[0]) {
      {
      __VERIFIER_assume(__startrek_start_t0[0] <= __startrek_start_t2[15]);
      __VERIFIER_assume(__startrek_end_t2[15] < __startrek_end_t0[0]);
      }
    }
  }
  if (__startrek_start_t1[0] <= __startrek_end_t2[15]) {
    if (__startrek_start_t2[15] <= __startrek_end_t1[0]) {
      {
      __VERIFIER_assume(__startrek_start_t1[0] <= __startrek_start_t2[15]);
      __VERIFIER_assume(__startrek_end_t2[15] < __startrek_end_t1[0]);
      __VERIFIER_assume(__startrek_end_t2[7] < __startrek_start_t1[0]);
      }
    }
  }
  if (__startrek_start_t1[1] <= __startrek_end_t2[15]) {
    if (__startrek_start_t2[15] <= __startrek_end_t1[1]) {
      {
      __VERIFIER_assume(__startrek_start_t1[1] <= __startrek_start_t2[15]);
      __VERIFIER_assume(__startrek_end_t2[15] < __startrek_end_t1[1]);
      __VERIFIER_assume(__startrek_end_t2[7] < __startrek_start_t1[1]);
      }
    }
  }
  if (__startrek_start_t0[0] <= __startrek_end_t2[16]) {
    if (__startrek_start_t2[16] <= __startrek_end_t0[0]) {
      {
      __VERIFIER_assume(__startrek_start_t0[0] <= __startrek_start_t2[16]);
      __VERIFIER_assume(__startrek_end_t2[16] < __startrek_end_t0[0]);
      }
    }
  }
  if (__startrek_start_t1[0] <= __startrek_end_t2[16]) {
    if (__startrek_start_t2[16] <= __startrek_end_t1[0]) {
      {
      __VERIFIER_assume(__startrek_start_t1[0] <= __startrek_start_t2[16]);
      __VERIFIER_assume(__startrek_end_t2[16] < __startrek_end_t1[0]);
      __VERIFIER_assume(__startrek_end_t2[8] < __startrek_start_t1[0]);
      }
    }
  }
  if (__startrek_start_t1[1] <= __startrek_end_t2[16]) {
    if (__startrek_start_t2[16] <= __startrek_end_t1[1]) {
      {
      __VERIFIER_assume(__startrek_start_t1[1] <= __startrek_start_t2[16]);
      __VERIFIER_assume(__startrek_end_t2[16] < __startrek_end_t1[1]);
      __VERIFIER_assume(__startrek_end_t2[8] < __startrek_start_t1[1]);
      }
    }
  }
  if (__startrek_start_t0[0] <= __startrek_end_t2[17]) {
    if (__startrek_start_t2[17] <= __startrek_end_t0[0]) {
      {
      __VERIFIER_assume(__startrek_start_t0[0] <= __startrek_start_t2[17]);
      __VERIFIER_assume(__startrek_end_t2[17] < __startrek_end_t0[0]);
      }
    }
  }
  if (__startrek_start_t1[0] <= __startrek_end_t2[17]) {
    if (__startrek_start_t2[17] <= __startrek_end_t1[0]) {
      {
      __VERIFIER_assume(__startrek_start_t1[0] <= __startrek_start_t2[17]);
      __VERIFIER_assume(__startrek_end_t2[17] < __startrek_end_t1[0]);
      __VERIFIER_assume(__startrek_end_t2[9] < __startrek_start_t1[0]);
      }
    }
  }
  if (__startrek_start_t1[1] <= __startrek_end_t2[17]) {
    if (__startrek_start_t2[17] <= __startrek_end_t1[1]) {
      {
      __VERIFIER_assume(__startrek_start_t1[1] <= __startrek_start_t2[17]);
      __VERIFIER_assume(__startrek_end_t2[17] < __startrek_end_t1[1]);
      __VERIFIER_assume(__startrek_end_t2[9] < __startrek_start_t1[1]);
      }
    }
  }
  if (__startrek_start_t0[0] <= __startrek_end_t2[18]) {
    if (__startrek_start_t2[18] <= __startrek_end_t0[0]) {
      {
      __VERIFIER_assume(__startrek_start_t0[0] <= __startrek_start_t2[18]);
      __VERIFIER_assume(__startrek_end_t2[18] < __startrek_end_t0[0]);
      }
    }
  }
  if (__startrek_start_t1[0] <= __startrek_end_t2[18]) {
    if (__startrek_start_t2[18] <= __startrek_end_t1[0]) {
      {
      __VERIFIER_assume(__startrek_start_t1[0] <= __startrek_start_t2[18]);
      __VERIFIER_assume(__startrek_end_t2[18] < __startrek_end_t1[0]);
      __VERIFIER_assume(__startrek_end_t2[10] < __startrek_start_t1[0]);
      }
    }
  }
  if (__startrek_start_t1[1] <= __startrek_end_t2[18]) {
    if (__startrek_start_t2[18] <= __startrek_end_t1[1]) {
      {
      __VERIFIER_assume(__startrek_start_t1[1] <= __startrek_start_t2[18]);
      __VERIFIER_assume(__startrek_end_t2[18] < __startrek_end_t1[1]);
      __VERIFIER_assume(__startrek_end_t2[10] < __startrek_start_t1[1]);
      }
    }
  }
  if (__startrek_start_t0[0] <= __startrek_end_t2[19]) {
    if (__startrek_start_t2[19] <= __startrek_end_t0[0]) {
      {
      __VERIFIER_assume(__startrek_start_t0[0] <= __startrek_start_t2[19]);
      __VERIFIER_assume(__startrek_end_t2[19] < __startrek_end_t0[0]);
      }
    }
  }
  if (__startrek_start_t1[0] <= __startrek_end_t2[19]) {
    if (__startrek_start_t2[19] <= __startrek_end_t1[0]) {
      {
      __VERIFIER_assume(__startrek_start_t1[0] <= __startrek_start_t2[19]);
      __VERIFIER_assume(__startrek_end_t2[19] < __startrek_end_t1[0]);
      __VERIFIER_assume(__startrek_end_t2[11] < __startrek_start_t1[0]);
      }
    }
  }
  if (__startrek_start_t1[1] <= __startrek_end_t2[19]) {
    if (__startrek_start_t2[19] <= __startrek_end_t1[1]) {
      {
      __VERIFIER_assume(__startrek_start_t1[1] <= __startrek_start_t2[19]);
      __VERIFIER_assume(__startrek_end_t2[19] < __startrek_end_t1[1]);
      __VERIFIER_assume(__startrek_end_t2[11] < __startrek_start_t1[1]);
      }
    }
  }
  if (__startrek_start_t0[0] <= __startrek_end_t2[20]) {
    if (__startrek_start_t2[20] <= __startrek_end_t0[0]) {
      {
      __VERIFIER_assume(__startrek_start_t0[0] <= __startrek_start_t2[20]);
      __VERIFIER_assume(__startrek_end_t2[20] < __startrek_end_t0[0]);
      }
    }
  }
  if (__startrek_start_t1[0] <= __startrek_end_t2[20]) {
    if (__startrek_start_t2[20] <= __startrek_end_t1[0]) {
      {
      __VERIFIER_assume(__startrek_start_t1[0] <= __startrek_start_t2[20]);
      __VERIFIER_assume(__startrek_end_t2[20] < __startrek_end_t1[0]);
      __VERIFIER_assume(__startrek_end_t2[12] < __startrek_start_t1[0]);
      }
    }
  }
  if (__startrek_start_t1[1] <= __startrek_end_t2[20]) {
    if (__startrek_start_t2[20] <= __startrek_end_t1[1]) {
      {
      __VERIFIER_assume(__startrek_start_t1[1] <= __startrek_start_t2[20]);
      __VERIFIER_assume(__startrek_end_t2[20] < __startrek_end_t1[1]);
      __VERIFIER_assume(__startrek_end_t2[12] < __startrek_start_t1[1]);
      }
    }
  }
  if (__startrek_start_t0[0] <= __startrek_end_t2[21]) {
    if (__startrek_start_t2[21] <= __startrek_end_t0[0]) {
      {
      __VERIFIER_assume(__startrek_start_t0[0] <= __startrek_start_t2[21]);
      __VERIFIER_assume(__startrek_end_t2[21] < __startrek_end_t0[0]);
      }
    }
  }
  if (__startrek_start_t1[0] <= __startrek_end_t2[21]) {
    if (__startrek_start_t2[21] <= __startrek_end_t1[0]) {
      {
      __VERIFIER_assume(__startrek_start_t1[0] <= __startrek_start_t2[21]);
      __VERIFIER_assume(__startrek_end_t2[21] < __startrek_end_t1[0]);
      __VERIFIER_assume(__startrek_end_t2[13] < __startrek_start_t1[0]);
      }
    }
  }
  if (__startrek_start_t1[1] <= __startrek_end_t2[21]) {
    if (__startrek_start_t2[21] <= __startrek_end_t1[1]) {
      {
      __VERIFIER_assume(__startrek_start_t1[1] <= __startrek_start_t2[21]);
      __VERIFIER_assume(__startrek_end_t2[21] < __startrek_end_t1[1]);
      __VERIFIER_assume(__startrek_end_t2[13] < __startrek_start_t1[1]);
      }
    }
  }
  if (__startrek_start_t0[0] <= __startrek_end_t2[22]) {
    if (__startrek_start_t2[22] <= __startrek_end_t0[0]) {
      {
      __VERIFIER_assume(__startrek_start_t0[0] <= __startrek_start_t2[22]);
      __VERIFIER_assume(__startrek_end_t2[22] < __startrek_end_t0[0]);
      }
    }
  }
  if (__startrek_start_t1[0] <= __startrek_end_t2[22]) {
    if (__startrek_start_t2[22] <= __startrek_end_t1[0]) {
      {
      __VERIFIER_assume(__startrek_start_t1[0] <= __startrek_start_t2[22]);
      __VERIFIER_assume(__startrek_end_t2[22] < __startrek_end_t1[0]);
      __VERIFIER_assume(__startrek_end_t2[14] < __startrek_start_t1[0]);
      }
    }
  }
  if (__startrek_start_t1[1] <= __startrek_end_t2[22]) {
    if (__startrek_start_t2[22] <= __startrek_end_t1[1]) {
      {
      __VERIFIER_assume(__startrek_start_t1[1] <= __startrek_start_t2[22]);
      __VERIFIER_assume(__startrek_end_t2[22] < __startrek_end_t1[1]);
      __VERIFIER_assume(__startrek_end_t2[14] < __startrek_start_t1[1]);
      }
    }
  }
  if (__startrek_start_t0[0] <= __startrek_end_t2[23]) {
    if (__startrek_start_t2[23] <= __startrek_end_t0[0]) {
      {
      __VERIFIER_assume(__startrek_start_t0[0] <= __startrek_start_t2[23]);
      __VERIFIER_assume(__startrek_end_t2[23] < __startrek_end_t0[0]);
      }
    }
  }
  if (__startrek_start_t1[0] <= __startrek_end_t2[23]) {
    if (__startrek_start_t2[23] <= __startrek_end_t1[0]) {
      {
      __VERIFIER_assume(__startrek_start_t1[0] <= __startrek_start_t2[23]);
      __VERIFIER_assume(__startrek_end_t2[23] < __startrek_end_t1[0]);
      __VERIFIER_assume(__startrek_end_t2[15] < __startrek_start_t1[0]);
      }
    }
  }
  if (__startrek_start_t1[1] <= __startrek_end_t2[23]) {
    if (__startrek_start_t2[23] <= __startrek_end_t1[1]) {
      {
      __VERIFIER_assume(__startrek_start_t1[1] <= __startrek_start_t2[23]);
      __VERIFIER_assume(__startrek_end_t2[23] < __startrek_end_t1[1]);
      __VERIFIER_assume(__startrek_end_t2[15] < __startrek_start_t1[1]);
      }
    }
  }
}
}
__inline void __startrek_init_globals(void) 
{ 


  {
  _i___startrek_job_count_OSEK_Task_ts1_[1] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts1_[1] = _i___startrek_job_count_OSEK_Task_ts1_[1];
  _i___startrek_job_count_OSEK_Task_ts1_[2] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts1_[2] = _i___startrek_job_count_OSEK_Task_ts1_[2];
  _i___startrek_job_count_OSEK_Task_ts1_[3] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts1_[3] = _i___startrek_job_count_OSEK_Task_ts1_[3];
  _i___startrek_job_count_OSEK_Task_ts1_[4] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts1_[4] = _i___startrek_job_count_OSEK_Task_ts1_[4];
  _i___startrek_job_count_OSEK_Task_ts1_[5] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts1_[5] = _i___startrek_job_count_OSEK_Task_ts1_[5];
  _i___startrek_job_count_OSEK_Task_ts1_[6] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts1_[6] = _i___startrek_job_count_OSEK_Task_ts1_[6];
  _i___startrek_job_count_OSEK_Task_ts1_[7] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts1_[7] = _i___startrek_job_count_OSEK_Task_ts1_[7];
  _i___startrek_job_count_OSEK_Task_ts1_[8] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts1_[8] = _i___startrek_job_count_OSEK_Task_ts1_[8];
  _i___startrek_job_count_OSEK_Task_ts1_[9] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts1_[9] = _i___startrek_job_count_OSEK_Task_ts1_[9];
  _i___startrek_job_count_OSEK_Task_ts1_[10] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts1_[10] = _i___startrek_job_count_OSEK_Task_ts1_[10];
  _i___startrek_job_count_OSEK_Task_ts1_[11] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts1_[11] = _i___startrek_job_count_OSEK_Task_ts1_[11];
  _i___startrek_job_count_OSEK_Task_ts1_[12] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts1_[12] = _i___startrek_job_count_OSEK_Task_ts1_[12];
  _i___startrek_job_count_OSEK_Task_ts1_[13] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts1_[13] = _i___startrek_job_count_OSEK_Task_ts1_[13];
  _i___startrek_job_count_OSEK_Task_ts1_[14] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts1_[14] = _i___startrek_job_count_OSEK_Task_ts1_[14];
  _i___startrek_job_count_OSEK_Task_ts1_[15] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts1_[15] = _i___startrek_job_count_OSEK_Task_ts1_[15];
  _i___startrek_job_count_OSEK_Task_ts1_[16] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts1_[16] = _i___startrek_job_count_OSEK_Task_ts1_[16];
  _i___startrek_job_count_OSEK_Task_ts1_[17] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts1_[17] = _i___startrek_job_count_OSEK_Task_ts1_[17];
  _i___startrek_job_count_OSEK_Task_ts1_[18] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts1_[18] = _i___startrek_job_count_OSEK_Task_ts1_[18];
  _i___startrek_job_count_OSEK_Task_ts1_[19] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts1_[19] = _i___startrek_job_count_OSEK_Task_ts1_[19];
  _i___startrek_job_count_OSEK_Task_ts1_[20] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts1_[20] = _i___startrek_job_count_OSEK_Task_ts1_[20];
  _i___startrek_job_count_OSEK_Task_ts1_[21] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts1_[21] = _i___startrek_job_count_OSEK_Task_ts1_[21];
  _i___startrek_job_count_OSEK_Task_ts1_[22] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts1_[22] = _i___startrek_job_count_OSEK_Task_ts1_[22];
  _i___startrek_job_count_OSEK_Task_ts1_[23] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts1_[23] = _i___startrek_job_count_OSEK_Task_ts1_[23];
  _i___startrek_job_count_OSEK_Task_ts1_[24] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts1_[24] = _i___startrek_job_count_OSEK_Task_ts1_[24];
  _i___startrek_job_count_OSEK_Task_ts1_[25] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts1_[25] = _i___startrek_job_count_OSEK_Task_ts1_[25];
  _i___startrek_job_count_OSEK_Task_ts1_[26] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts1_[26] = _i___startrek_job_count_OSEK_Task_ts1_[26];
  _i___startrek_job_count_OSEK_Task_ts2_[1] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts2_[1] = _i___startrek_job_count_OSEK_Task_ts2_[1];
  _i___startrek_job_count_OSEK_Task_ts2_[2] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts2_[2] = _i___startrek_job_count_OSEK_Task_ts2_[2];
  _i___startrek_job_count_OSEK_Task_ts2_[3] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts2_[3] = _i___startrek_job_count_OSEK_Task_ts2_[3];
  _i___startrek_job_count_OSEK_Task_ts2_[4] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts2_[4] = _i___startrek_job_count_OSEK_Task_ts2_[4];
  _i___startrek_job_count_OSEK_Task_ts2_[5] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts2_[5] = _i___startrek_job_count_OSEK_Task_ts2_[5];
  _i___startrek_job_count_OSEK_Task_ts2_[6] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts2_[6] = _i___startrek_job_count_OSEK_Task_ts2_[6];
  _i___startrek_job_count_OSEK_Task_ts2_[7] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts2_[7] = _i___startrek_job_count_OSEK_Task_ts2_[7];
  _i___startrek_job_count_OSEK_Task_ts2_[8] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts2_[8] = _i___startrek_job_count_OSEK_Task_ts2_[8];
  _i___startrek_job_count_OSEK_Task_ts2_[9] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts2_[9] = _i___startrek_job_count_OSEK_Task_ts2_[9];
  _i___startrek_job_count_OSEK_Task_ts2_[10] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts2_[10] = _i___startrek_job_count_OSEK_Task_ts2_[10];
  _i___startrek_job_count_OSEK_Task_ts2_[11] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts2_[11] = _i___startrek_job_count_OSEK_Task_ts2_[11];
  _i___startrek_job_count_OSEK_Task_ts2_[12] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts2_[12] = _i___startrek_job_count_OSEK_Task_ts2_[12];
  _i___startrek_job_count_OSEK_Task_ts2_[13] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts2_[13] = _i___startrek_job_count_OSEK_Task_ts2_[13];
  _i___startrek_job_count_OSEK_Task_ts2_[14] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts2_[14] = _i___startrek_job_count_OSEK_Task_ts2_[14];
  _i___startrek_job_count_OSEK_Task_ts2_[15] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts2_[15] = _i___startrek_job_count_OSEK_Task_ts2_[15];
  _i___startrek_job_count_OSEK_Task_ts2_[16] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts2_[16] = _i___startrek_job_count_OSEK_Task_ts2_[16];
  _i___startrek_job_count_OSEK_Task_ts2_[17] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts2_[17] = _i___startrek_job_count_OSEK_Task_ts2_[17];
  _i___startrek_job_count_OSEK_Task_ts2_[18] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts2_[18] = _i___startrek_job_count_OSEK_Task_ts2_[18];
  _i___startrek_job_count_OSEK_Task_ts2_[19] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts2_[19] = _i___startrek_job_count_OSEK_Task_ts2_[19];
  _i___startrek_job_count_OSEK_Task_ts2_[20] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts2_[20] = _i___startrek_job_count_OSEK_Task_ts2_[20];
  _i___startrek_job_count_OSEK_Task_ts2_[21] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts2_[21] = _i___startrek_job_count_OSEK_Task_ts2_[21];
  _i___startrek_job_count_OSEK_Task_ts2_[22] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts2_[22] = _i___startrek_job_count_OSEK_Task_ts2_[22];
  _i___startrek_job_count_OSEK_Task_ts2_[23] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts2_[23] = _i___startrek_job_count_OSEK_Task_ts2_[23];
  _i___startrek_job_count_OSEK_Task_ts2_[24] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts2_[24] = _i___startrek_job_count_OSEK_Task_ts2_[24];
  _i___startrek_job_count_OSEK_Task_ts2_[25] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts2_[25] = _i___startrek_job_count_OSEK_Task_ts2_[25];
  _i___startrek_job_count_OSEK_Task_ts2_[26] = __VERIFIER_nondet_char();
  ___startrek_job_count_OSEK_Task_ts2_[26] = _i___startrek_job_count_OSEK_Task_ts2_[26];
  _i_trans_[1] = __VERIFIER_nondet_bool();
  _trans_[1] = _i_trans_[1];
  _i_trans_[2] = __VERIFIER_nondet_bool();
  _trans_[2] = _i_trans_[2];
  _i_trans_[3] = __VERIFIER_nondet_bool();
  _trans_[3] = _i_trans_[3];
  _i_trans_[4] = __VERIFIER_nondet_bool();
  _trans_[4] = _i_trans_[4];
  _i_trans_[5] = __VERIFIER_nondet_bool();
  _trans_[5] = _i_trans_[5];
  _i_trans_[6] = __VERIFIER_nondet_bool();
  _trans_[6] = _i_trans_[6];
  _i_trans_[7] = __VERIFIER_nondet_bool();
  _trans_[7] = _i_trans_[7];
  _i_trans_[8] = __VERIFIER_nondet_bool();
  _trans_[8] = _i_trans_[8];
  _i_trans_[9] = __VERIFIER_nondet_bool();
  _trans_[9] = _i_trans_[9];
  _i_trans_[10] = __VERIFIER_nondet_bool();
  _trans_[10] = _i_trans_[10];
  _i_trans_[11] = __VERIFIER_nondet_bool();
  _trans_[11] = _i_trans_[11];
  _i_trans_[12] = __VERIFIER_nondet_bool();
  _trans_[12] = _i_trans_[12];
  _i_trans_[13] = __VERIFIER_nondet_bool();
  _trans_[13] = _i_trans_[13];
  _i_trans_[14] = __VERIFIER_nondet_bool();
  _trans_[14] = _i_trans_[14];
  _i_trans_[15] = __VERIFIER_nondet_bool();
  _trans_[15] = _i_trans_[15];
  _i_trans_[16] = __VERIFIER_nondet_bool();
  _trans_[16] = _i_trans_[16];
  _i_trans_[17] = __VERIFIER_nondet_bool();
  _trans_[17] = _i_trans_[17];
  _i_trans_[18] = __VERIFIER_nondet_bool();
  _trans_[18] = _i_trans_[18];
  _i_trans_[19] = __VERIFIER_nondet_bool();
  _trans_[19] = _i_trans_[19];
  _i_trans_[20] = __VERIFIER_nondet_bool();
  _trans_[20] = _i_trans_[20];
  _i_trans_[21] = __VERIFIER_nondet_bool();
  _trans_[21] = _i_trans_[21];
  _i_trans_[22] = __VERIFIER_nondet_bool();
  _trans_[22] = _i_trans_[22];
  _i_trans_[23] = __VERIFIER_nondet_bool();
  _trans_[23] = _i_trans_[23];
  _i_trans_[24] = __VERIFIER_nondet_bool();
  _trans_[24] = _i_trans_[24];
  _i_trans_[25] = __VERIFIER_nondet_bool();
  _trans_[25] = _i_trans_[25];
  _i_trans_[26] = __VERIFIER_nondet_bool();
  _trans_[26] = _i_trans_[26];
  _i_cmd_turn_[1] = __VERIFIER_nondet_char();
  _cmd_turn_[1] = _i_cmd_turn_[1];
  _i_cmd_turn_[2] = __VERIFIER_nondet_char();
  _cmd_turn_[2] = _i_cmd_turn_[2];
  _i_cmd_turn_[3] = __VERIFIER_nondet_char();
  _cmd_turn_[3] = _i_cmd_turn_[3];
  _i_cmd_turn_[4] = __VERIFIER_nondet_char();
  _cmd_turn_[4] = _i_cmd_turn_[4];
  _i_cmd_turn_[5] = __VERIFIER_nondet_char();
  _cmd_turn_[5] = _i_cmd_turn_[5];
  _i_cmd_turn_[6] = __VERIFIER_nondet_char();
  _cmd_turn_[6] = _i_cmd_turn_[6];
  _i_cmd_turn_[7] = __VERIFIER_nondet_char();
  _cmd_turn_[7] = _i_cmd_turn_[7];
  _i_cmd_turn_[8] = __VERIFIER_nondet_char();
  _cmd_turn_[8] = _i_cmd_turn_[8];
  _i_cmd_turn_[9] = __VERIFIER_nondet_char();
  _cmd_turn_[9] = _i_cmd_turn_[9];
  _i_cmd_turn_[10] = __VERIFIER_nondet_char();
  _cmd_turn_[10] = _i_cmd_turn_[10];
  _i_cmd_turn_[11] = __VERIFIER_nondet_char();
  _cmd_turn_[11] = _i_cmd_turn_[11];
  _i_cmd_turn_[12] = __VERIFIER_nondet_char();
  _cmd_turn_[12] = _i_cmd_turn_[12];
  _i_cmd_turn_[13] = __VERIFIER_nondet_char();
  _cmd_turn_[13] = _i_cmd_turn_[13];
  _i_cmd_turn_[14] = __VERIFIER_nondet_char();
  _cmd_turn_[14] = _i_cmd_turn_[14];
  _i_cmd_turn_[15] = __VERIFIER_nondet_char();
  _cmd_turn_[15] = _i_cmd_turn_[15];
  _i_cmd_turn_[16] = __VERIFIER_nondet_char();
  _cmd_turn_[16] = _i_cmd_turn_[16];
  _i_cmd_turn_[17] = __VERIFIER_nondet_char();
  _cmd_turn_[17] = _i_cmd_turn_[17];
  _i_cmd_turn_[18] = __VERIFIER_nondet_char();
  _cmd_turn_[18] = _i_cmd_turn_[18];
  _i_cmd_turn_[19] = __VERIFIER_nondet_char();
  _cmd_turn_[19] = _i_cmd_turn_[19];
  _i_cmd_turn_[20] = __VERIFIER_nondet_char();
  _cmd_turn_[20] = _i_cmd_turn_[20];
  _i_cmd_turn_[21] = __VERIFIER_nondet_char();
  _cmd_turn_[21] = _i_cmd_turn_[21];
  _i_cmd_turn_[22] = __VERIFIER_nondet_char();
  _cmd_turn_[22] = _i_cmd_turn_[22];
  _i_cmd_turn_[23] = __VERIFIER_nondet_char();
  _cmd_turn_[23] = _i_cmd_turn_[23];
  _i_cmd_turn_[24] = __VERIFIER_nondet_char();
  _cmd_turn_[24] = _i_cmd_turn_[24];
  _i_cmd_turn_[25] = __VERIFIER_nondet_char();
  _cmd_turn_[25] = _i_cmd_turn_[25];
  _i_cmd_turn_[26] = __VERIFIER_nondet_char();
  _cmd_turn_[26] = _i_cmd_turn_[26];
  _i_cmd_forward_[1] = __VERIFIER_nondet_char();
  _cmd_forward_[1] = _i_cmd_forward_[1];
  _i_cmd_forward_[2] = __VERIFIER_nondet_char();
  _cmd_forward_[2] = _i_cmd_forward_[2];
  _i_cmd_forward_[3] = __VERIFIER_nondet_char();
  _cmd_forward_[3] = _i_cmd_forward_[3];
  _i_cmd_forward_[4] = __VERIFIER_nondet_char();
  _cmd_forward_[4] = _i_cmd_forward_[4];
  _i_cmd_forward_[5] = __VERIFIER_nondet_char();
  _cmd_forward_[5] = _i_cmd_forward_[5];
  _i_cmd_forward_[6] = __VERIFIER_nondet_char();
  _cmd_forward_[6] = _i_cmd_forward_[6];
  _i_cmd_forward_[7] = __VERIFIER_nondet_char();
  _cmd_forward_[7] = _i_cmd_forward_[7];
  _i_cmd_forward_[8] = __VERIFIER_nondet_char();
  _cmd_forward_[8] = _i_cmd_forward_[8];
  _i_cmd_forward_[9] = __VERIFIER_nondet_char();
  _cmd_forward_[9] = _i_cmd_forward_[9];
  _i_cmd_forward_[10] = __VERIFIER_nondet_char();
  _cmd_forward_[10] = _i_cmd_forward_[10];
  _i_cmd_forward_[11] = __VERIFIER_nondet_char();
  _cmd_forward_[11] = _i_cmd_forward_[11];
  _i_cmd_forward_[12] = __VERIFIER_nondet_char();
  _cmd_forward_[12] = _i_cmd_forward_[12];
  _i_cmd_forward_[13] = __VERIFIER_nondet_char();
  _cmd_forward_[13] = _i_cmd_forward_[13];
  _i_cmd_forward_[14] = __VERIFIER_nondet_char();
  _cmd_forward_[14] = _i_cmd_forward_[14];
  _i_cmd_forward_[15] = __VERIFIER_nondet_char();
  _cmd_forward_[15] = _i_cmd_forward_[15];
  _i_cmd_forward_[16] = __VERIFIER_nondet_char();
  _cmd_forward_[16] = _i_cmd_forward_[16];
  _i_cmd_forward_[17] = __VERIFIER_nondet_char();
  _cmd_forward_[17] = _i_cmd_forward_[17];
  _i_cmd_forward_[18] = __VERIFIER_nondet_char();
  _cmd_forward_[18] = _i_cmd_forward_[18];
  _i_cmd_forward_[19] = __VERIFIER_nondet_char();
  _cmd_forward_[19] = _i_cmd_forward_[19];
  _i_cmd_forward_[20] = __VERIFIER_nondet_char();
  _cmd_forward_[20] = _i_cmd_forward_[20];
  _i_cmd_forward_[21] = __VERIFIER_nondet_char();
  _cmd_forward_[21] = _i_cmd_forward_[21];
  _i_cmd_forward_[22] = __VERIFIER_nondet_char();
  _cmd_forward_[22] = _i_cmd_forward_[22];
  _i_cmd_forward_[23] = __VERIFIER_nondet_char();
  _cmd_forward_[23] = _i_cmd_forward_[23];
  _i_cmd_forward_[24] = __VERIFIER_nondet_char();
  _cmd_forward_[24] = _i_cmd_forward_[24];
  _i_cmd_forward_[25] = __VERIFIER_nondet_char();
  _cmd_forward_[25] = _i_cmd_forward_[25];
  _i_cmd_forward_[26] = __VERIFIER_nondet_char();
  _cmd_forward_[26] = _i_cmd_forward_[26];
  _i_obstacle_flag_[1] = __VERIFIER_nondet_bool();
  _obstacle_flag_[1] = _i_obstacle_flag_[1];
  _i_obstacle_flag_[2] = __VERIFIER_nondet_bool();
  _obstacle_flag_[2] = _i_obstacle_flag_[2];
  _i_obstacle_flag_[3] = __VERIFIER_nondet_bool();
  _obstacle_flag_[3] = _i_obstacle_flag_[3];
  _i_obstacle_flag_[4] = __VERIFIER_nondet_bool();
  _obstacle_flag_[4] = _i_obstacle_flag_[4];
  _i_obstacle_flag_[5] = __VERIFIER_nondet_bool();
  _obstacle_flag_[5] = _i_obstacle_flag_[5];
  _i_obstacle_flag_[6] = __VERIFIER_nondet_bool();
  _obstacle_flag_[6] = _i_obstacle_flag_[6];
  _i_obstacle_flag_[7] = __VERIFIER_nondet_bool();
  _obstacle_flag_[7] = _i_obstacle_flag_[7];
  _i_obstacle_flag_[8] = __VERIFIER_nondet_bool();
  _obstacle_flag_[8] = _i_obstacle_flag_[8];
  _i_obstacle_flag_[9] = __VERIFIER_nondet_bool();
  _obstacle_flag_[9] = _i_obstacle_flag_[9];
  _i_obstacle_flag_[10] = __VERIFIER_nondet_bool();
  _obstacle_flag_[10] = _i_obstacle_flag_[10];
  _i_obstacle_flag_[11] = __VERIFIER_nondet_bool();
  _obstacle_flag_[11] = _i_obstacle_flag_[11];
  _i_obstacle_flag_[12] = __VERIFIER_nondet_bool();
  _obstacle_flag_[12] = _i_obstacle_flag_[12];
  _i_obstacle_flag_[13] = __VERIFIER_nondet_bool();
  _obstacle_flag_[13] = _i_obstacle_flag_[13];
  _i_obstacle_flag_[14] = __VERIFIER_nondet_bool();
  _obstacle_flag_[14] = _i_obstacle_flag_[14];
  _i_obstacle_flag_[15] = __VERIFIER_nondet_bool();
  _obstacle_flag_[15] = _i_obstacle_flag_[15];
  _i_obstacle_flag_[16] = __VERIFIER_nondet_bool();
  _obstacle_flag_[16] = _i_obstacle_flag_[16];
  _i_obstacle_flag_[17] = __VERIFIER_nondet_bool();
  _obstacle_flag_[17] = _i_obstacle_flag_[17];
  _i_obstacle_flag_[18] = __VERIFIER_nondet_bool();
  _obstacle_flag_[18] = _i_obstacle_flag_[18];
  _i_obstacle_flag_[19] = __VERIFIER_nondet_bool();
  _obstacle_flag_[19] = _i_obstacle_flag_[19];
  _i_obstacle_flag_[20] = __VERIFIER_nondet_bool();
  _obstacle_flag_[20] = _i_obstacle_flag_[20];
  _i_obstacle_flag_[21] = __VERIFIER_nondet_bool();
  _obstacle_flag_[21] = _i_obstacle_flag_[21];
  _i_obstacle_flag_[22] = __VERIFIER_nondet_bool();
  _obstacle_flag_[22] = _i_obstacle_flag_[22];
  _i_obstacle_flag_[23] = __VERIFIER_nondet_bool();
  _obstacle_flag_[23] = _i_obstacle_flag_[23];
  _i_obstacle_flag_[24] = __VERIFIER_nondet_bool();
  _obstacle_flag_[24] = _i_obstacle_flag_[24];
  _i_obstacle_flag_[25] = __VERIFIER_nondet_bool();
  _obstacle_flag_[25] = _i_obstacle_flag_[25];
  _i_obstacle_flag_[26] = __VERIFIER_nondet_bool();
  _obstacle_flag_[26] = _i_obstacle_flag_[26];
  _i_nxtway_gs_mode_[1] = __VERIFIER_nondet_uchar();
  _nxtway_gs_mode_[1] = _i_nxtway_gs_mode_[1];
  _i_nxtway_gs_mode_[2] = __VERIFIER_nondet_uchar();
  _nxtway_gs_mode_[2] = _i_nxtway_gs_mode_[2];
  _i_nxtway_gs_mode_[3] = __VERIFIER_nondet_uchar();
  _nxtway_gs_mode_[3] = _i_nxtway_gs_mode_[3];
  _i_nxtway_gs_mode_[4] = __VERIFIER_nondet_uchar();
  _nxtway_gs_mode_[4] = _i_nxtway_gs_mode_[4];
  _i_nxtway_gs_mode_[5] = __VERIFIER_nondet_uchar();
  _nxtway_gs_mode_[5] = _i_nxtway_gs_mode_[5];
  _i_nxtway_gs_mode_[6] = __VERIFIER_nondet_uchar();
  _nxtway_gs_mode_[6] = _i_nxtway_gs_mode_[6];
  _i_nxtway_gs_mode_[7] = __VERIFIER_nondet_uchar();
  _nxtway_gs_mode_[7] = _i_nxtway_gs_mode_[7];
  _i_nxtway_gs_mode_[8] = __VERIFIER_nondet_uchar();
  _nxtway_gs_mode_[8] = _i_nxtway_gs_mode_[8];
  _i_nxtway_gs_mode_[9] = __VERIFIER_nondet_uchar();
  _nxtway_gs_mode_[9] = _i_nxtway_gs_mode_[9];
  _i_nxtway_gs_mode_[10] = __VERIFIER_nondet_uchar();
  _nxtway_gs_mode_[10] = _i_nxtway_gs_mode_[10];
  _i_nxtway_gs_mode_[11] = __VERIFIER_nondet_uchar();
  _nxtway_gs_mode_[11] = _i_nxtway_gs_mode_[11];
  _i_nxtway_gs_mode_[12] = __VERIFIER_nondet_uchar();
  _nxtway_gs_mode_[12] = _i_nxtway_gs_mode_[12];
  _i_nxtway_gs_mode_[13] = __VERIFIER_nondet_uchar();
  _nxtway_gs_mode_[13] = _i_nxtway_gs_mode_[13];
  _i_nxtway_gs_mode_[14] = __VERIFIER_nondet_uchar();
  _nxtway_gs_mode_[14] = _i_nxtway_gs_mode_[14];
  _i_nxtway_gs_mode_[15] = __VERIFIER_nondet_uchar();
  _nxtway_gs_mode_[15] = _i_nxtway_gs_mode_[15];
  _i_nxtway_gs_mode_[16] = __VERIFIER_nondet_uchar();
  _nxtway_gs_mode_[16] = _i_nxtway_gs_mode_[16];
  _i_nxtway_gs_mode_[17] = __VERIFIER_nondet_uchar();
  _nxtway_gs_mode_[17] = _i_nxtway_gs_mode_[17];
  _i_nxtway_gs_mode_[18] = __VERIFIER_nondet_uchar();
  _nxtway_gs_mode_[18] = _i_nxtway_gs_mode_[18];
  _i_nxtway_gs_mode_[19] = __VERIFIER_nondet_uchar();
  _nxtway_gs_mode_[19] = _i_nxtway_gs_mode_[19];
  _i_nxtway_gs_mode_[20] = __VERIFIER_nondet_uchar();
  _nxtway_gs_mode_[20] = _i_nxtway_gs_mode_[20];
  _i_nxtway_gs_mode_[21] = __VERIFIER_nondet_uchar();
  _nxtway_gs_mode_[21] = _i_nxtway_gs_mode_[21];
  _i_nxtway_gs_mode_[22] = __VERIFIER_nondet_uchar();
  _nxtway_gs_mode_[22] = _i_nxtway_gs_mode_[22];
  _i_nxtway_gs_mode_[23] = __VERIFIER_nondet_uchar();
  _nxtway_gs_mode_[23] = _i_nxtway_gs_mode_[23];
  _i_nxtway_gs_mode_[24] = __VERIFIER_nondet_uchar();
  _nxtway_gs_mode_[24] = _i_nxtway_gs_mode_[24];
  _i_nxtway_gs_mode_[25] = __VERIFIER_nondet_uchar();
  _nxtway_gs_mode_[25] = _i_nxtway_gs_mode_[25];
  _i_nxtway_gs_mode_[26] = __VERIFIER_nondet_uchar();
  _nxtway_gs_mode_[26] = _i_nxtway_gs_mode_[26];
  _i___startrek_current_priority_[1] = __VERIFIER_nondet_char();
  ___startrek_current_priority_[1] = _i___startrek_current_priority_[1];
  _i___startrek_current_priority_[2] = __VERIFIER_nondet_char();
  ___startrek_current_priority_[2] = _i___startrek_current_priority_[2];
  _i___startrek_current_priority_[3] = __VERIFIER_nondet_char();
  ___startrek_current_priority_[3] = _i___startrek_current_priority_[3];
  _i___startrek_current_priority_[4] = __VERIFIER_nondet_char();
  ___startrek_current_priority_[4] = _i___startrek_current_priority_[4];
  _i___startrek_current_priority_[5] = __VERIFIER_nondet_char();
  ___startrek_current_priority_[5] = _i___startrek_current_priority_[5];
  _i___startrek_current_priority_[6] = __VERIFIER_nondet_char();
  ___startrek_current_priority_[6] = _i___startrek_current_priority_[6];
  _i___startrek_current_priority_[7] = __VERIFIER_nondet_char();
  ___startrek_current_priority_[7] = _i___startrek_current_priority_[7];
  _i___startrek_current_priority_[8] = __VERIFIER_nondet_char();
  ___startrek_current_priority_[8] = _i___startrek_current_priority_[8];
  _i___startrek_current_priority_[9] = __VERIFIER_nondet_char();
  ___startrek_current_priority_[9] = _i___startrek_current_priority_[9];
  _i___startrek_current_priority_[10] = __VERIFIER_nondet_char();
  ___startrek_current_priority_[10] = _i___startrek_current_priority_[10];
  _i___startrek_current_priority_[11] = __VERIFIER_nondet_char();
  ___startrek_current_priority_[11] = _i___startrek_current_priority_[11];
  _i___startrek_current_priority_[12] = __VERIFIER_nondet_char();
  ___startrek_current_priority_[12] = _i___startrek_current_priority_[12];
  _i___startrek_current_priority_[13] = __VERIFIER_nondet_char();
  ___startrek_current_priority_[13] = _i___startrek_current_priority_[13];
  _i___startrek_current_priority_[14] = __VERIFIER_nondet_char();
  ___startrek_current_priority_[14] = _i___startrek_current_priority_[14];
  _i___startrek_current_priority_[15] = __VERIFIER_nondet_char();
  ___startrek_current_priority_[15] = _i___startrek_current_priority_[15];
  _i___startrek_current_priority_[16] = __VERIFIER_nondet_char();
  ___startrek_current_priority_[16] = _i___startrek_current_priority_[16];
  _i___startrek_current_priority_[17] = __VERIFIER_nondet_char();
  ___startrek_current_priority_[17] = _i___startrek_current_priority_[17];
  _i___startrek_current_priority_[18] = __VERIFIER_nondet_char();
  ___startrek_current_priority_[18] = _i___startrek_current_priority_[18];
  _i___startrek_current_priority_[19] = __VERIFIER_nondet_char();
  ___startrek_current_priority_[19] = _i___startrek_current_priority_[19];
  _i___startrek_current_priority_[20] = __VERIFIER_nondet_char();
  ___startrek_current_priority_[20] = _i___startrek_current_priority_[20];
  _i___startrek_current_priority_[21] = __VERIFIER_nondet_char();
  ___startrek_current_priority_[21] = _i___startrek_current_priority_[21];
  _i___startrek_current_priority_[22] = __VERIFIER_nondet_char();
  ___startrek_current_priority_[22] = _i___startrek_current_priority_[22];
  _i___startrek_current_priority_[23] = __VERIFIER_nondet_char();
  ___startrek_current_priority_[23] = _i___startrek_current_priority_[23];
  _i___startrek_current_priority_[24] = __VERIFIER_nondet_char();
  ___startrek_current_priority_[24] = _i___startrek_current_priority_[24];
  _i___startrek_current_priority_[25] = __VERIFIER_nondet_char();
  ___startrek_current_priority_[25] = _i___startrek_current_priority_[25];
  _i___startrek_current_priority_[26] = __VERIFIER_nondet_char();
  ___startrek_current_priority_[26] = _i___startrek_current_priority_[26];
}
}
__inline static _Bool __startrek_cs_t0(void) 
{ 
  _Bool c1 ;
  unsigned char o2 ;

  {
  if (__startrek_is_first_cs) {
    {
    __startrek_is_first_cs = 0;
    }
  }
  if (__startrek_lock) {
    return (0);
  }
  c1 = __VERIFIER_nondet_bool();
  if (c1) {
    return (0);
  }
  o2 = __startrek_round;
  __startrek_round = __VERIFIER_nondet_uchar();
  __VERIFIER_assume(__startrek_round > o2);
  __VERIFIER_assume(__startrek_round <= __startrek_job_end);
  if (__startrek_round != __startrek_job_end) {
    {
    if (__startrek_start_t1[0] < __startrek_round) {
      __VERIFIER_assume(__startrek_round > __startrek_end_t1[0]);
    }
    if (__startrek_start_t1[1] < __startrek_round) {
      __VERIFIER_assume(__startrek_round > __startrek_end_t1[1]);
    }
    }
  }
  return (1);
}
}
__inline static _Bool __startrek_cs_t1(void) 
{ 
  _Bool c1 ;
  unsigned char o2 ;

  {
  if (__startrek_is_first_cs) {
    {
    __startrek_is_first_cs = 0;
    }
  }
  if (__startrek_lock) {
    return (0);
  }
  c1 = __VERIFIER_nondet_bool();
  if (c1) {
    return (0);
  }
  o2 = __startrek_round;
  __startrek_round = __VERIFIER_nondet_uchar();
  __VERIFIER_assume(__startrek_round > o2);
  __VERIFIER_assume(__startrek_round <= __startrek_job_end);
  if (__startrek_round != __startrek_job_end) {
    {

    }
  }
  return (1);
}
}
__inline static _Bool __startrek_cs_t2(void) 
{ 


  {
  return (0);
}
}
__inline static void __startrek_assert_i0(_Bool arg ) 
{ 


  {
  if (__startrek_hyper_period != 0) {
    return;
  }
  if (arg) {
    return;
  }
  if (__startrek_round < __startrek_error_round) {
    __startrek_error_round = __startrek_round;
  }
  switch (__startrek_task) {
  case 0: 
  __startrek_Assert_t0_i0[__startrek_job] = 0;
  break;
  case 1: 
  __startrek_Assert_t1_i0[__startrek_job] = 0;
  break;
  case 2: 
  __startrek_Assert_t2_i0[__startrek_job] = 0;
  break;
  }
}
}
__inline void __startrek_check_assumptions(void) 
{ 


  {
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts1_[26] == ___startrek_job_count_OSEK_Task_ts1_[25]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts1_[25] == ___startrek_job_count_OSEK_Task_ts1_[24]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts1_[24] == ___startrek_job_count_OSEK_Task_ts1_[23]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts1_[23] == ___startrek_job_count_OSEK_Task_ts1_[22]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts1_[22] == ___startrek_job_count_OSEK_Task_ts1_[21]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts1_[21] == ___startrek_job_count_OSEK_Task_ts1_[20]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts1_[20] == ___startrek_job_count_OSEK_Task_ts1_[19]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts1_[19] == ___startrek_job_count_OSEK_Task_ts1_[18]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts1_[18] == ___startrek_job_count_OSEK_Task_ts1_[17]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts1_[17] == ___startrek_job_count_OSEK_Task_ts1_[16]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts1_[16] == ___startrek_job_count_OSEK_Task_ts1_[15]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts1_[15] == ___startrek_job_count_OSEK_Task_ts1_[14]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts1_[14] == ___startrek_job_count_OSEK_Task_ts1_[13]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts1_[13] == ___startrek_job_count_OSEK_Task_ts1_[12]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts1_[12] == ___startrek_job_count_OSEK_Task_ts1_[11]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts1_[11] == ___startrek_job_count_OSEK_Task_ts1_[10]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts1_[10] == ___startrek_job_count_OSEK_Task_ts1_[9]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts1_[9] == ___startrek_job_count_OSEK_Task_ts1_[8]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts1_[8] == ___startrek_job_count_OSEK_Task_ts1_[7]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts1_[7] == ___startrek_job_count_OSEK_Task_ts1_[6]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts1_[6] == ___startrek_job_count_OSEK_Task_ts1_[5]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts1_[5] == ___startrek_job_count_OSEK_Task_ts1_[4]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts1_[4] == ___startrek_job_count_OSEK_Task_ts1_[3]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts1_[3] == ___startrek_job_count_OSEK_Task_ts1_[2]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts1_[2] == ___startrek_job_count_OSEK_Task_ts1_[1]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts1_[1] == ___startrek_job_count_OSEK_Task_ts1_[0]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts2_[26] == ___startrek_job_count_OSEK_Task_ts2_[25]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts2_[25] == ___startrek_job_count_OSEK_Task_ts2_[24]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts2_[24] == ___startrek_job_count_OSEK_Task_ts2_[23]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts2_[23] == ___startrek_job_count_OSEK_Task_ts2_[22]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts2_[22] == ___startrek_job_count_OSEK_Task_ts2_[21]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts2_[21] == ___startrek_job_count_OSEK_Task_ts2_[20]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts2_[20] == ___startrek_job_count_OSEK_Task_ts2_[19]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts2_[19] == ___startrek_job_count_OSEK_Task_ts2_[18]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts2_[18] == ___startrek_job_count_OSEK_Task_ts2_[17]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts2_[17] == ___startrek_job_count_OSEK_Task_ts2_[16]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts2_[16] == ___startrek_job_count_OSEK_Task_ts2_[15]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts2_[15] == ___startrek_job_count_OSEK_Task_ts2_[14]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts2_[14] == ___startrek_job_count_OSEK_Task_ts2_[13]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts2_[13] == ___startrek_job_count_OSEK_Task_ts2_[12]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts2_[12] == ___startrek_job_count_OSEK_Task_ts2_[11]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts2_[11] == ___startrek_job_count_OSEK_Task_ts2_[10]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts2_[10] == ___startrek_job_count_OSEK_Task_ts2_[9]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts2_[9] == ___startrek_job_count_OSEK_Task_ts2_[8]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts2_[8] == ___startrek_job_count_OSEK_Task_ts2_[7]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts2_[7] == ___startrek_job_count_OSEK_Task_ts2_[6]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts2_[6] == ___startrek_job_count_OSEK_Task_ts2_[5]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts2_[5] == ___startrek_job_count_OSEK_Task_ts2_[4]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts2_[4] == ___startrek_job_count_OSEK_Task_ts2_[3]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts2_[3] == ___startrek_job_count_OSEK_Task_ts2_[2]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts2_[2] == ___startrek_job_count_OSEK_Task_ts2_[1]);
  __VERIFIER_assume(_i___startrek_job_count_OSEK_Task_ts2_[1] == ___startrek_job_count_OSEK_Task_ts2_[0]);
  __VERIFIER_assume(_i_trans_[26] == _trans_[25]);
  __VERIFIER_assume(_i_trans_[25] == _trans_[24]);
  __VERIFIER_assume(_i_trans_[24] == _trans_[23]);
  __VERIFIER_assume(_i_trans_[23] == _trans_[22]);
  __VERIFIER_assume(_i_trans_[22] == _trans_[21]);
  __VERIFIER_assume(_i_trans_[21] == _trans_[20]);
  __VERIFIER_assume(_i_trans_[20] == _trans_[19]);
  __VERIFIER_assume(_i_trans_[19] == _trans_[18]);
  __VERIFIER_assume(_i_trans_[18] == _trans_[17]);
  __VERIFIER_assume(_i_trans_[17] == _trans_[16]);
  __VERIFIER_assume(_i_trans_[16] == _trans_[15]);
  __VERIFIER_assume(_i_trans_[15] == _trans_[14]);
  __VERIFIER_assume(_i_trans_[14] == _trans_[13]);
  __VERIFIER_assume(_i_trans_[13] == _trans_[12]);
  __VERIFIER_assume(_i_trans_[12] == _trans_[11]);
  __VERIFIER_assume(_i_trans_[11] == _trans_[10]);
  __VERIFIER_assume(_i_trans_[10] == _trans_[9]);
  __VERIFIER_assume(_i_trans_[9] == _trans_[8]);
  __VERIFIER_assume(_i_trans_[8] == _trans_[7]);
  __VERIFIER_assume(_i_trans_[7] == _trans_[6]);
  __VERIFIER_assume(_i_trans_[6] == _trans_[5]);
  __VERIFIER_assume(_i_trans_[5] == _trans_[4]);
  __VERIFIER_assume(_i_trans_[4] == _trans_[3]);
  __VERIFIER_assume(_i_trans_[3] == _trans_[2]);
  __VERIFIER_assume(_i_trans_[2] == _trans_[1]);
  __VERIFIER_assume(_i_trans_[1] == _trans_[0]);
  __VERIFIER_assume(_i_cmd_turn_[26] == _cmd_turn_[25]);
  __VERIFIER_assume(_i_cmd_turn_[25] == _cmd_turn_[24]);
  __VERIFIER_assume(_i_cmd_turn_[24] == _cmd_turn_[23]);
  __VERIFIER_assume(_i_cmd_turn_[23] == _cmd_turn_[22]);
  __VERIFIER_assume(_i_cmd_turn_[22] == _cmd_turn_[21]);
  __VERIFIER_assume(_i_cmd_turn_[21] == _cmd_turn_[20]);
  __VERIFIER_assume(_i_cmd_turn_[20] == _cmd_turn_[19]);
  __VERIFIER_assume(_i_cmd_turn_[19] == _cmd_turn_[18]);
  __VERIFIER_assume(_i_cmd_turn_[18] == _cmd_turn_[17]);
  __VERIFIER_assume(_i_cmd_turn_[17] == _cmd_turn_[16]);
  __VERIFIER_assume(_i_cmd_turn_[16] == _cmd_turn_[15]);
  __VERIFIER_assume(_i_cmd_turn_[15] == _cmd_turn_[14]);
  __VERIFIER_assume(_i_cmd_turn_[14] == _cmd_turn_[13]);
  __VERIFIER_assume(_i_cmd_turn_[13] == _cmd_turn_[12]);
  __VERIFIER_assume(_i_cmd_turn_[12] == _cmd_turn_[11]);
  __VERIFIER_assume(_i_cmd_turn_[11] == _cmd_turn_[10]);
  __VERIFIER_assume(_i_cmd_turn_[10] == _cmd_turn_[9]);
  __VERIFIER_assume(_i_cmd_turn_[9] == _cmd_turn_[8]);
  __VERIFIER_assume(_i_cmd_turn_[8] == _cmd_turn_[7]);
  __VERIFIER_assume(_i_cmd_turn_[7] == _cmd_turn_[6]);
  __VERIFIER_assume(_i_cmd_turn_[6] == _cmd_turn_[5]);
  __VERIFIER_assume(_i_cmd_turn_[5] == _cmd_turn_[4]);
  __VERIFIER_assume(_i_cmd_turn_[4] == _cmd_turn_[3]);
  __VERIFIER_assume(_i_cmd_turn_[3] == _cmd_turn_[2]);
  __VERIFIER_assume(_i_cmd_turn_[2] == _cmd_turn_[1]);
  __VERIFIER_assume(_i_cmd_turn_[1] == _cmd_turn_[0]);
  __VERIFIER_assume(_i_cmd_forward_[26] == _cmd_forward_[25]);
  __VERIFIER_assume(_i_cmd_forward_[25] == _cmd_forward_[24]);
  __VERIFIER_assume(_i_cmd_forward_[24] == _cmd_forward_[23]);
  __VERIFIER_assume(_i_cmd_forward_[23] == _cmd_forward_[22]);
  __VERIFIER_assume(_i_cmd_forward_[22] == _cmd_forward_[21]);
  __VERIFIER_assume(_i_cmd_forward_[21] == _cmd_forward_[20]);
  __VERIFIER_assume(_i_cmd_forward_[20] == _cmd_forward_[19]);
  __VERIFIER_assume(_i_cmd_forward_[19] == _cmd_forward_[18]);
  __VERIFIER_assume(_i_cmd_forward_[18] == _cmd_forward_[17]);
  __VERIFIER_assume(_i_cmd_forward_[17] == _cmd_forward_[16]);
  __VERIFIER_assume(_i_cmd_forward_[16] == _cmd_forward_[15]);
  __VERIFIER_assume(_i_cmd_forward_[15] == _cmd_forward_[14]);
  __VERIFIER_assume(_i_cmd_forward_[14] == _cmd_forward_[13]);
  __VERIFIER_assume(_i_cmd_forward_[13] == _cmd_forward_[12]);
  __VERIFIER_assume(_i_cmd_forward_[12] == _cmd_forward_[11]);
  __VERIFIER_assume(_i_cmd_forward_[11] == _cmd_forward_[10]);
  __VERIFIER_assume(_i_cmd_forward_[10] == _cmd_forward_[9]);
  __VERIFIER_assume(_i_cmd_forward_[9] == _cmd_forward_[8]);
  __VERIFIER_assume(_i_cmd_forward_[8] == _cmd_forward_[7]);
  __VERIFIER_assume(_i_cmd_forward_[7] == _cmd_forward_[6]);
  __VERIFIER_assume(_i_cmd_forward_[6] == _cmd_forward_[5]);
  __VERIFIER_assume(_i_cmd_forward_[5] == _cmd_forward_[4]);
  __VERIFIER_assume(_i_cmd_forward_[4] == _cmd_forward_[3]);
  __VERIFIER_assume(_i_cmd_forward_[3] == _cmd_forward_[2]);
  __VERIFIER_assume(_i_cmd_forward_[2] == _cmd_forward_[1]);
  __VERIFIER_assume(_i_cmd_forward_[1] == _cmd_forward_[0]);
  __VERIFIER_assume(_i_obstacle_flag_[26] == _obstacle_flag_[25]);
  __VERIFIER_assume(_i_obstacle_flag_[25] == _obstacle_flag_[24]);
  __VERIFIER_assume(_i_obstacle_flag_[24] == _obstacle_flag_[23]);
  __VERIFIER_assume(_i_obstacle_flag_[23] == _obstacle_flag_[22]);
  __VERIFIER_assume(_i_obstacle_flag_[22] == _obstacle_flag_[21]);
  __VERIFIER_assume(_i_obstacle_flag_[21] == _obstacle_flag_[20]);
  __VERIFIER_assume(_i_obstacle_flag_[20] == _obstacle_flag_[19]);
  __VERIFIER_assume(_i_obstacle_flag_[19] == _obstacle_flag_[18]);
  __VERIFIER_assume(_i_obstacle_flag_[18] == _obstacle_flag_[17]);
  __VERIFIER_assume(_i_obstacle_flag_[17] == _obstacle_flag_[16]);
  __VERIFIER_assume(_i_obstacle_flag_[16] == _obstacle_flag_[15]);
  __VERIFIER_assume(_i_obstacle_flag_[15] == _obstacle_flag_[14]);
  __VERIFIER_assume(_i_obstacle_flag_[14] == _obstacle_flag_[13]);
  __VERIFIER_assume(_i_obstacle_flag_[13] == _obstacle_flag_[12]);
  __VERIFIER_assume(_i_obstacle_flag_[12] == _obstacle_flag_[11]);
  __VERIFIER_assume(_i_obstacle_flag_[11] == _obstacle_flag_[10]);
  __VERIFIER_assume(_i_obstacle_flag_[10] == _obstacle_flag_[9]);
  __VERIFIER_assume(_i_obstacle_flag_[9] == _obstacle_flag_[8]);
  __VERIFIER_assume(_i_obstacle_flag_[8] == _obstacle_flag_[7]);
  __VERIFIER_assume(_i_obstacle_flag_[7] == _obstacle_flag_[6]);
  __VERIFIER_assume(_i_obstacle_flag_[6] == _obstacle_flag_[5]);
  __VERIFIER_assume(_i_obstacle_flag_[5] == _obstacle_flag_[4]);
  __VERIFIER_assume(_i_obstacle_flag_[4] == _obstacle_flag_[3]);
  __VERIFIER_assume(_i_obstacle_flag_[3] == _obstacle_flag_[2]);
  __VERIFIER_assume(_i_obstacle_flag_[2] == _obstacle_flag_[1]);
  __VERIFIER_assume(_i_obstacle_flag_[1] == _obstacle_flag_[0]);
  __VERIFIER_assume(_i_nxtway_gs_mode_[26] == _nxtway_gs_mode_[25]);
  __VERIFIER_assume(_i_nxtway_gs_mode_[25] == _nxtway_gs_mode_[24]);
  __VERIFIER_assume(_i_nxtway_gs_mode_[24] == _nxtway_gs_mode_[23]);
  __VERIFIER_assume(_i_nxtway_gs_mode_[23] == _nxtway_gs_mode_[22]);
  __VERIFIER_assume(_i_nxtway_gs_mode_[22] == _nxtway_gs_mode_[21]);
  __VERIFIER_assume(_i_nxtway_gs_mode_[21] == _nxtway_gs_mode_[20]);
  __VERIFIER_assume(_i_nxtway_gs_mode_[20] == _nxtway_gs_mode_[19]);
  __VERIFIER_assume(_i_nxtway_gs_mode_[19] == _nxtway_gs_mode_[18]);
  __VERIFIER_assume(_i_nxtway_gs_mode_[18] == _nxtway_gs_mode_[17]);
  __VERIFIER_assume(_i_nxtway_gs_mode_[17] == _nxtway_gs_mode_[16]);
  __VERIFIER_assume(_i_nxtway_gs_mode_[16] == _nxtway_gs_mode_[15]);
  __VERIFIER_assume(_i_nxtway_gs_mode_[15] == _nxtway_gs_mode_[14]);
  __VERIFIER_assume(_i_nxtway_gs_mode_[14] == _nxtway_gs_mode_[13]);
  __VERIFIER_assume(_i_nxtway_gs_mode_[13] == _nxtway_gs_mode_[12]);
  __VERIFIER_assume(_i_nxtway_gs_mode_[12] == _nxtway_gs_mode_[11]);
  __VERIFIER_assume(_i_nxtway_gs_mode_[11] == _nxtway_gs_mode_[10]);
  __VERIFIER_assume(_i_nxtway_gs_mode_[10] == _nxtway_gs_mode_[9]);
  __VERIFIER_assume(_i_nxtway_gs_mode_[9] == _nxtway_gs_mode_[8]);
  __VERIFIER_assume(_i_nxtway_gs_mode_[8] == _nxtway_gs_mode_[7]);
  __VERIFIER_assume(_i_nxtway_gs_mode_[7] == _nxtway_gs_mode_[6]);
  __VERIFIER_assume(_i_nxtway_gs_mode_[6] == _nxtway_gs_mode_[5]);
  __VERIFIER_assume(_i_nxtway_gs_mode_[5] == _nxtway_gs_mode_[4]);
  __VERIFIER_assume(_i_nxtway_gs_mode_[4] == _nxtway_gs_mode_[3]);
  __VERIFIER_assume(_i_nxtway_gs_mode_[3] == _nxtway_gs_mode_[2]);
  __VERIFIER_assume(_i_nxtway_gs_mode_[2] == _nxtway_gs_mode_[1]);
  __VERIFIER_assume(_i_nxtway_gs_mode_[1] == _nxtway_gs_mode_[0]);
  __VERIFIER_assume(_i___startrek_current_priority_[26] == ___startrek_current_priority_[25]);
  __VERIFIER_assume(_i___startrek_current_priority_[25] == ___startrek_current_priority_[24]);
  __VERIFIER_assume(_i___startrek_current_priority_[24] == ___startrek_current_priority_[23]);
  __VERIFIER_assume(_i___startrek_current_priority_[23] == ___startrek_current_priority_[22]);
  __VERIFIER_assume(_i___startrek_current_priority_[22] == ___startrek_current_priority_[21]);
  __VERIFIER_assume(_i___startrek_current_priority_[21] == ___startrek_current_priority_[20]);
  __VERIFIER_assume(_i___startrek_current_priority_[20] == ___startrek_current_priority_[19]);
  __VERIFIER_assume(_i___startrek_current_priority_[19] == ___startrek_current_priority_[18]);
  __VERIFIER_assume(_i___startrek_current_priority_[18] == ___startrek_current_priority_[17]);
  __VERIFIER_assume(_i___startrek_current_priority_[17] == ___startrek_current_priority_[16]);
  __VERIFIER_assume(_i___startrek_current_priority_[16] == ___startrek_current_priority_[15]);
  __VERIFIER_assume(_i___startrek_current_priority_[15] == ___startrek_current_priority_[14]);
  __VERIFIER_assume(_i___startrek_current_priority_[14] == ___startrek_current_priority_[13]);
  __VERIFIER_assume(_i___startrek_current_priority_[13] == ___startrek_current_priority_[12]);
  __VERIFIER_assume(_i___startrek_current_priority_[12] == ___startrek_current_priority_[11]);
  __VERIFIER_assume(_i___startrek_current_priority_[11] == ___startrek_current_priority_[10]);
  __VERIFIER_assume(_i___startrek_current_priority_[10] == ___startrek_current_priority_[9]);
  __VERIFIER_assume(_i___startrek_current_priority_[9] == ___startrek_current_priority_[8]);
  __VERIFIER_assume(_i___startrek_current_priority_[8] == ___startrek_current_priority_[7]);
  __VERIFIER_assume(_i___startrek_current_priority_[7] == ___startrek_current_priority_[6]);
  __VERIFIER_assume(_i___startrek_current_priority_[6] == ___startrek_current_priority_[5]);
  __VERIFIER_assume(_i___startrek_current_priority_[5] == ___startrek_current_priority_[4]);
  __VERIFIER_assume(_i___startrek_current_priority_[4] == ___startrek_current_priority_[3]);
  __VERIFIER_assume(_i___startrek_current_priority_[3] == ___startrek_current_priority_[2]);
  __VERIFIER_assume(_i___startrek_current_priority_[2] == ___startrek_current_priority_[1]);
  __VERIFIER_assume(_i___startrek_current_priority_[1] == ___startrek_current_priority_[0]);
}
}
__inline void __startrek_user_init(void) 
{ 


  {

}
}
__inline void __startrek_user_final(void) 
{ 


  {

}
}
__inline void __startrek_check_assertions(void) 
{ 


  {
  assert(__startrek_Assert_t2_i0[23]);
  assert(__startrek_Assert_t2_i0[22]);
  assert(__startrek_Assert_t2_i0[21]);
  assert(__startrek_Assert_t2_i0[20]);
  assert(__startrek_Assert_t2_i0[19]);
  assert(__startrek_Assert_t2_i0[18]);
  assert(__startrek_Assert_t2_i0[17]);
  assert(__startrek_Assert_t2_i0[16]);
  assert(__startrek_Assert_t2_i0[15]);
  assert(__startrek_Assert_t2_i0[14]);
  assert(__startrek_Assert_t2_i0[13]);
  assert(__startrek_Assert_t2_i0[12]);
  assert(__startrek_Assert_t2_i0[11]);
  assert(__startrek_Assert_t2_i0[10]);
  assert(__startrek_Assert_t2_i0[9]);
  assert(__startrek_Assert_t2_i0[8]);
  assert(__startrek_Assert_t2_i0[7]);
  assert(__startrek_Assert_t2_i0[6]);
  assert(__startrek_Assert_t2_i0[5]);
  assert(__startrek_Assert_t2_i0[4]);
  assert(__startrek_Assert_t2_i0[3]);
  assert(__startrek_Assert_t2_i0[2]);
  assert(__startrek_Assert_t2_i0[1]);
  assert(__startrek_Assert_t2_i0[0]);
  assert(__startrek_Assert_t1_i0[1]);
  assert(__startrek_Assert_t1_i0[0]);
  assert(__startrek_Assert_t0_i0[0]);
}
}
void __main(void) 
{ 
  _Bool c1 ;

  {
  __startrek_error_round = 27;
  __startrek_schedule_jobs();
  __startrek_init_globals();
  {
  {
  __startrek_task = 0;
  __startrek_job = 0;
  __startrek_is_first_cs = 1;
  __startrek_round = __startrek_start_t0[0];
  if (__startrek_round < __startrek_error_round) {
    {
    __startrek_job_end = __startrek_end_t0[0];
    c1 = __startrek_entry_pt_OSEK_Task_ts3();
    __startrek_lock = 0;
    __VERIFIER_assume(__startrek_round == __startrek_job_end);
    }
  }
  }
  {
  __startrek_task = 1;
  __startrek_job = 0;
  __startrek_is_first_cs = 1;
  __startrek_round = __startrek_start_t1[0];
  if (__startrek_round < __startrek_error_round) {
    {
    __startrek_job_end = __startrek_end_t1[0];
    c1 = __startrek_entry_pt_OSEK_Task_ts2();
    __startrek_lock = 0;
    __VERIFIER_assume(__startrek_round == __startrek_job_end);
    }
  }
  __startrek_job = 1;
  __startrek_is_first_cs = 1;
  __startrek_round = __startrek_start_t1[1];
  if (__startrek_round < __startrek_error_round) {
    {
    __startrek_job_end = __startrek_end_t1[1];
    c1 = __startrek_entry_pt_OSEK_Task_ts2();
    __startrek_lock = 0;
    __VERIFIER_assume(__startrek_round == __startrek_job_end);
    }
  }
  }
  {
  __startrek_task = 2;
  __startrek_job = 0;
  __startrek_is_first_cs = 1;
  __startrek_round = __startrek_start_t2[0];
  if (__startrek_round < __startrek_error_round) {
    {
    __startrek_job_end = __startrek_end_t2[0];
    c1 = __startrek_entry_pt_OSEK_Task_ts1();
    __startrek_lock = 0;
    __VERIFIER_assume(__startrek_round == __startrek_job_end);
    }
  }
  __startrek_job = 1;
  __startrek_is_first_cs = 1;
  __startrek_round = __startrek_start_t2[1];
  if (__startrek_round < __startrek_error_round) {
    {
    __startrek_job_end = __startrek_end_t2[1];
    c1 = __startrek_entry_pt_OSEK_Task_ts1();
    __startrek_lock = 0;
    __VERIFIER_assume(__startrek_round == __startrek_job_end);
    }
  }
  __startrek_job = 2;
  __startrek_is_first_cs = 1;
  __startrek_round = __startrek_start_t2[2];
  if (__startrek_round < __startrek_error_round) {
    {
    __startrek_job_end = __startrek_end_t2[2];
    c1 = __startrek_entry_pt_OSEK_Task_ts1();
    __startrek_lock = 0;
    __VERIFIER_assume(__startrek_round == __startrek_job_end);
    }
  }
  __startrek_job = 3;
  __startrek_is_first_cs = 1;
  __startrek_round = __startrek_start_t2[3];
  if (__startrek_round < __startrek_error_round) {
    {
    __startrek_job_end = __startrek_end_t2[3];
    c1 = __startrek_entry_pt_OSEK_Task_ts1();
    __startrek_lock = 0;
    __VERIFIER_assume(__startrek_round == __startrek_job_end);
    }
  }
  __startrek_job = 4;
  __startrek_is_first_cs = 1;
  __startrek_round = __startrek_start_t2[4];
  if (__startrek_round < __startrek_error_round) {
    {
    __startrek_job_end = __startrek_end_t2[4];
    c1 = __startrek_entry_pt_OSEK_Task_ts1();
    __startrek_lock = 0;
    __VERIFIER_assume(__startrek_round == __startrek_job_end);
    }
  }
  __startrek_job = 5;
  __startrek_is_first_cs = 1;
  __startrek_round = __startrek_start_t2[5];
  if (__startrek_round < __startrek_error_round) {
    {
    __startrek_job_end = __startrek_end_t2[5];
    c1 = __startrek_entry_pt_OSEK_Task_ts1();
    __startrek_lock = 0;
    __VERIFIER_assume(__startrek_round == __startrek_job_end);
    }
  }
  __startrek_job = 6;
  __startrek_is_first_cs = 1;
  __startrek_round = __startrek_start_t2[6];
  if (__startrek_round < __startrek_error_round) {
    {
    __startrek_job_end = __startrek_end_t2[6];
    c1 = __startrek_entry_pt_OSEK_Task_ts1();
    __startrek_lock = 0;
    __VERIFIER_assume(__startrek_round == __startrek_job_end);
    }
  }
  __startrek_job = 7;
  __startrek_is_first_cs = 1;
  __startrek_round = __startrek_start_t2[7];
  if (__startrek_round < __startrek_error_round) {
    {
    __startrek_job_end = __startrek_end_t2[7];
    c1 = __startrek_entry_pt_OSEK_Task_ts1();
    __startrek_lock = 0;
    __VERIFIER_assume(__startrek_round == __startrek_job_end);
    }
  }
  __startrek_job = 8;
  __startrek_is_first_cs = 1;
  __startrek_round = __startrek_start_t2[8];
  if (__startrek_round < __startrek_error_round) {
    {
    __startrek_job_end = __startrek_end_t2[8];
    c1 = __startrek_entry_pt_OSEK_Task_ts1();
    __startrek_lock = 0;
    __VERIFIER_assume(__startrek_round == __startrek_job_end);
    }
  }
  __startrek_job = 9;
  __startrek_is_first_cs = 1;
  __startrek_round = __startrek_start_t2[9];
  if (__startrek_round < __startrek_error_round) {
    {
    __startrek_job_end = __startrek_end_t2[9];
    c1 = __startrek_entry_pt_OSEK_Task_ts1();
    __startrek_lock = 0;
    __VERIFIER_assume(__startrek_round == __startrek_job_end);
    }
  }
  __startrek_job = 10;
  __startrek_is_first_cs = 1;
  __startrek_round = __startrek_start_t2[10];
  if (__startrek_round < __startrek_error_round) {
    {
    __startrek_job_end = __startrek_end_t2[10];
    c1 = __startrek_entry_pt_OSEK_Task_ts1();
    __startrek_lock = 0;
    __VERIFIER_assume(__startrek_round == __startrek_job_end);
    }
  }
  __startrek_job = 11;
  __startrek_is_first_cs = 1;
  __startrek_round = __startrek_start_t2[11];
  if (__startrek_round < __startrek_error_round) {
    {
    __startrek_job_end = __startrek_end_t2[11];
    c1 = __startrek_entry_pt_OSEK_Task_ts1();
    __startrek_lock = 0;
    __VERIFIER_assume(__startrek_round == __startrek_job_end);
    }
  }
  __startrek_job = 12;
  __startrek_is_first_cs = 1;
  __startrek_round = __startrek_start_t2[12];
  if (__startrek_round < __startrek_error_round) {
    {
    __startrek_job_end = __startrek_end_t2[12];
    c1 = __startrek_entry_pt_OSEK_Task_ts1();
    __startrek_lock = 0;
    __VERIFIER_assume(__startrek_round == __startrek_job_end);
    }
  }
  __startrek_job = 13;
  __startrek_is_first_cs = 1;
  __startrek_round = __startrek_start_t2[13];
  if (__startrek_round < __startrek_error_round) {
    {
    __startrek_job_end = __startrek_end_t2[13];
    c1 = __startrek_entry_pt_OSEK_Task_ts1();
    __startrek_lock = 0;
    __VERIFIER_assume(__startrek_round == __startrek_job_end);
    }
  }
  __startrek_job = 14;
  __startrek_is_first_cs = 1;
  __startrek_round = __startrek_start_t2[14];
  if (__startrek_round < __startrek_error_round) {
    {
    __startrek_job_end = __startrek_end_t2[14];
    c1 = __startrek_entry_pt_OSEK_Task_ts1();
    __startrek_lock = 0;
    __VERIFIER_assume(__startrek_round == __startrek_job_end);
    }
  }
  __startrek_job = 15;
  __startrek_is_first_cs = 1;
  __startrek_round = __startrek_start_t2[15];
  if (__startrek_round < __startrek_error_round) {
    {
    __startrek_job_end = __startrek_end_t2[15];
    c1 = __startrek_entry_pt_OSEK_Task_ts1();
    __startrek_lock = 0;
    __VERIFIER_assume(__startrek_round == __startrek_job_end);
    }
  }
  __startrek_job = 16;
  __startrek_is_first_cs = 1;
  __startrek_round = __startrek_start_t2[16];
  if (__startrek_round < __startrek_error_round) {
    {
    __startrek_job_end = __startrek_end_t2[16];
    c1 = __startrek_entry_pt_OSEK_Task_ts1();
    __startrek_lock = 0;
    __VERIFIER_assume(__startrek_round == __startrek_job_end);
    }
  }
  __startrek_job = 17;
  __startrek_is_first_cs = 1;
  __startrek_round = __startrek_start_t2[17];
  if (__startrek_round < __startrek_error_round) {
    {
    __startrek_job_end = __startrek_end_t2[17];
    c1 = __startrek_entry_pt_OSEK_Task_ts1();
    __startrek_lock = 0;
    __VERIFIER_assume(__startrek_round == __startrek_job_end);
    }
  }
  __startrek_job = 18;
  __startrek_is_first_cs = 1;
  __startrek_round = __startrek_start_t2[18];
  if (__startrek_round < __startrek_error_round) {
    {
    __startrek_job_end = __startrek_end_t2[18];
    c1 = __startrek_entry_pt_OSEK_Task_ts1();
    __startrek_lock = 0;
    __VERIFIER_assume(__startrek_round == __startrek_job_end);
    }
  }
  __startrek_job = 19;
  __startrek_is_first_cs = 1;
  __startrek_round = __startrek_start_t2[19];
  if (__startrek_round < __startrek_error_round) {
    {
    __startrek_job_end = __startrek_end_t2[19];
    c1 = __startrek_entry_pt_OSEK_Task_ts1();
    __startrek_lock = 0;
    __VERIFIER_assume(__startrek_round == __startrek_job_end);
    }
  }
  __startrek_job = 20;
  __startrek_is_first_cs = 1;
  __startrek_round = __startrek_start_t2[20];
  if (__startrek_round < __startrek_error_round) {
    {
    __startrek_job_end = __startrek_end_t2[20];
    c1 = __startrek_entry_pt_OSEK_Task_ts1();
    __startrek_lock = 0;
    __VERIFIER_assume(__startrek_round == __startrek_job_end);
    }
  }
  __startrek_job = 21;
  __startrek_is_first_cs = 1;
  __startrek_round = __startrek_start_t2[21];
  if (__startrek_round < __startrek_error_round) {
    {
    __startrek_job_end = __startrek_end_t2[21];
    c1 = __startrek_entry_pt_OSEK_Task_ts1();
    __startrek_lock = 0;
    __VERIFIER_assume(__startrek_round == __startrek_job_end);
    }
  }
  __startrek_job = 22;
  __startrek_is_first_cs = 1;
  __startrek_round = __startrek_start_t2[22];
  if (__startrek_round < __startrek_error_round) {
    {
    __startrek_job_end = __startrek_end_t2[22];
    c1 = __startrek_entry_pt_OSEK_Task_ts1();
    __startrek_lock = 0;
    __VERIFIER_assume(__startrek_round == __startrek_job_end);
    }
  }
  __startrek_job = 23;
  __startrek_is_first_cs = 1;
  __startrek_round = __startrek_start_t2[23];
  if (__startrek_round < __startrek_error_round) {
    {
    __startrek_job_end = __startrek_end_t2[23];
    c1 = __startrek_entry_pt_OSEK_Task_ts1();
    __startrek_lock = 0;
    __VERIFIER_assume(__startrek_round == __startrek_job_end);
    }
  }
  }
  }
  __startrek_round = 27;
  __startrek_check_assumptions();
  __startrek_check_assertions();
  if (__startrek_hyper_period == 0) {
    {
    __startrek_user_final();
    }
  }
}
}
int main(void) 
{ 


  {
  __startrek_init_shared();
  __startrek_user_init();
  __startrek_hyper_period = 0;
  __main();
}
return 0;
}
__inline static char __startrek_read___startrek_current_priority(void) 
{ 
  char r1 ;
  _Bool c2 ;
  unsigned char or3 ;

  {
  switch (__startrek_task) {
  case 0: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t0();
  {

  }
  }
  break;
  case 1: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t1();
  {

  }
  }
  break;
  case 2: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t2();
  {

  }
  }
  break;
  }
  r1 = ___startrek_current_priority_[__startrek_round];
  return (r1);
}
}
__inline static unsigned char __startrek_read_nxtway_gs_mode(void) 
{ 
  unsigned char r1 ;
  _Bool c2 ;
  unsigned char or3 ;

  {
  switch (__startrek_task) {
  case 0: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t0();
  {

  }
  }
  break;
  case 1: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t1();
  {

  }
  }
  break;
  case 2: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t2();
  {

  }
  }
  break;
  }
  r1 = _nxtway_gs_mode_[__startrek_round];
  return (r1);
}
}
__inline static _Bool __startrek_read_obstacle_flag(void) 
{ 
  _Bool r1 ;
  _Bool c2 ;
  unsigned char or3 ;

  {
  switch (__startrek_task) {
  case 0: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t0();
  {

  }
  }
  break;
  case 1: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t1();
  {

  }
  }
  break;
  case 2: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t2();
  {

  }
  }
  break;
  }
  r1 = _obstacle_flag_[__startrek_round];
  return (r1);
}
}
__inline static char __startrek_read_cmd_forward(void) 
{ 
  char r1 ;
  _Bool c2 ;
  unsigned char or3 ;

  {
  switch (__startrek_task) {
  case 0: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t0();
  {

  }
  }
  break;
  case 1: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t1();
  {

  }
  }
  break;
  case 2: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t2();
  {

  }
  }
  break;
  }
  r1 = _cmd_forward_[__startrek_round];
  return (r1);
}
}
__inline static char __startrek_read_cmd_turn(void) 
{ 
  char r1 ;
  _Bool c2 ;
  unsigned char or3 ;

  {
  switch (__startrek_task) {
  case 0: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t0();
  {

  }
  }
  break;
  case 1: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t1();
  {

  }
  }
  break;
  case 2: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t2();
  {

  }
  }
  break;
  }
  r1 = _cmd_turn_[__startrek_round];
  return (r1);
}
}
__inline static _Bool __startrek_read_trans(void) 
{ 
  _Bool r1 ;
  _Bool c2 ;
  unsigned char or3 ;

  {
  switch (__startrek_task) {
  case 0: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t0();
  {

  }
  }
  break;
  case 1: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t1();
  {

  }
  }
  break;
  case 2: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t2();
  {

  }
  }
  break;
  }
  r1 = _trans_[__startrek_round];
  return (r1);
}
}
__inline static char __startrek_read___startrek_job_count_OSEK_Task_ts2(void) 
{ 
  char r1 ;
  _Bool c2 ;
  unsigned char or3 ;

  {
  switch (__startrek_task) {
  case 0: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t0();
  {

  }
  }
  break;
  case 1: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t1();
  {

  }
  }
  break;
  case 2: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t2();
  {

  }
  }
  break;
  }
  r1 = ___startrek_job_count_OSEK_Task_ts2_[__startrek_round];
  return (r1);
}
}
__inline static char __startrek_read___startrek_job_count_OSEK_Task_ts1(void) 
{ 
  char r1 ;
  _Bool c2 ;
  unsigned char or3 ;

  {
  switch (__startrek_task) {
  case 0: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t0();
  {

  }
  }
  break;
  case 1: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t1();
  {

  }
  }
  break;
  case 2: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t2();
  {

  }
  }
  break;
  }
  r1 = ___startrek_job_count_OSEK_Task_ts1_[__startrek_round];
  return (r1);
}
}
__inline static void __startrek_write___startrek_current_priority(char arg ) 
{ 
  _Bool c2 ;
  unsigned char or3 ;

  {
  switch (__startrek_task) {
  case 0: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t0();
  {

  }
  }
  break;
  case 1: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t1();
  {

  }
  }
  break;
  case 2: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t2();
  {

  }
  }
  break;
  }
  ___startrek_current_priority_[__startrek_round] = arg;
}
}
__inline static void __startrek_write_nxtway_gs_mode(unsigned char arg ) 
{ 
  _Bool c2 ;
  unsigned char or3 ;

  {
  switch (__startrek_task) {
  case 0: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t0();
  {

  }
  }
  break;
  case 1: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t1();
  {

  }
  }
  break;
  case 2: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t2();
  {

  }
  }
  break;
  }
  _nxtway_gs_mode_[__startrek_round] = arg;
}
}
__inline static void __startrek_write_obstacle_flag(_Bool arg ) 
{ 
  _Bool c2 ;
  unsigned char or3 ;

  {
  switch (__startrek_task) {
  case 0: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t0();
  {

  }
  }
  break;
  case 1: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t1();
  {

  }
  }
  break;
  case 2: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t2();
  {

  }
  }
  break;
  }
  _obstacle_flag_[__startrek_round] = arg;
}
}
__inline static void __startrek_write_cmd_forward(char arg ) 
{ 
  _Bool c2 ;
  unsigned char or3 ;

  {
  switch (__startrek_task) {
  case 0: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t0();
  {

  }
  }
  break;
  case 1: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t1();
  {

  }
  }
  break;
  case 2: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t2();
  {

  }
  }
  break;
  }
  _cmd_forward_[__startrek_round] = arg;
}
}
__inline static void __startrek_write_cmd_turn(char arg ) 
{ 
  _Bool c2 ;
  unsigned char or3 ;

  {
  switch (__startrek_task) {
  case 0: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t0();
  {

  }
  }
  break;
  case 1: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t1();
  {

  }
  }
  break;
  case 2: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t2();
  {

  }
  }
  break;
  }
  _cmd_turn_[__startrek_round] = arg;
}
}
__inline static void __startrek_write_trans(_Bool arg ) 
{ 
  _Bool c2 ;
  unsigned char or3 ;

  {
  switch (__startrek_task) {
  case 0: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t0();
  {

  }
  }
  break;
  case 1: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t1();
  {

  }
  }
  break;
  case 2: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t2();
  {

  }
  }
  break;
  }
  _trans_[__startrek_round] = arg;
}
}
__inline static void __startrek_write___startrek_job_count_OSEK_Task_ts2(char arg ) 
{ 
  _Bool c2 ;
  unsigned char or3 ;

  {
  switch (__startrek_task) {
  case 0: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t0();
  {

  }
  }
  break;
  case 1: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t1();
  {

  }
  }
  break;
  case 2: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t2();
  {

  }
  }
  break;
  }
  ___startrek_job_count_OSEK_Task_ts2_[__startrek_round] = arg;
}
}
__inline static void __startrek_write___startrek_job_count_OSEK_Task_ts1(char arg ) 
{ 
  _Bool c2 ;
  unsigned char or3 ;

  {
  switch (__startrek_task) {
  case 0: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t0();
  {

  }
  }
  break;
  case 1: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t1();
  {

  }
  }
  break;
  case 2: 
  {
  or3 = __startrek_round;
  c2 = __startrek_cs_t2();
  {

  }
  }
  break;
  }
  ___startrek_job_count_OSEK_Task_ts1_[__startrek_round] = arg;
}
}
__inline void __startrek_init_shared(void) 
{ 


  {
  ___startrek_job_count_OSEK_Task_ts1_[0] = __startrek_hidden___startrek_job_count_OSEK_Task_ts1;
  ___startrek_job_count_OSEK_Task_ts2_[0] = __startrek_hidden___startrek_job_count_OSEK_Task_ts2;
  _trans_[0] = __startrek_hidden_trans;
  _cmd_turn_[0] = __startrek_hidden_cmd_turn;
  _cmd_forward_[0] = __startrek_hidden_cmd_forward;
  _obstacle_flag_[0] = __startrek_hidden_obstacle_flag;
  _nxtway_gs_mode_[0] = __startrek_hidden_nxtway_gs_mode;
  ___startrek_current_priority_[0] = __startrek_hidden___startrek_current_priority;
}
}