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 */

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 _Bool __startrek_cs_t2(void) ;
__inline static _Bool __startrek_cs_t1(void) ;
__inline static _Bool __startrek_cs_t0(void) ;
_Bool __VERIFIER_nondet_bool(void) ;
unsigned char __VERIFIER_nondet_uchar(void) ;
_Bool __VERIFIER_nondet_bool(void) ;
extern int __VERIFIER_nondet_int();
void __VERIFIER_assume(int arg ) ;
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/nxt.ok1.i","-S")
void assert(_Bool arg) { if (!arg) { ERROR: __VERIFIER_error();} }
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;
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  ) ;
extern void ecrobot_status_monitor(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 unsigned char bt_receive_buf[2]  ;
void OSEK_Task_ts1(void) 
{ 
  int i ;
  char cmd_forward ;
  char cmd_turn ;
  char pwm_l ;
  char pwm_r ;
  unsigned char tmp ;
  unsigned int tmp___0 ;
  unsigned int tmp___1 ;
  _Bool tmp___2 ;
  unsigned int tmp___3 ;
  char tmp___4 ;
  char tmp___5 ;
  unsigned int tmp___6 ;

  {
  tmp = __startrek_read_nxtway_gs_mode();
  switch (tmp) {
  case 0: 
  gyro_offset = 0;
  avg_cnt = 0;
  i = 0;
  while (i < 2) {
    bt_receive_buf[i] = 0;
    i ++;
  }
  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: 
  ecrobot_read_bt_packet(bt_receive_buf, 2);
  cmd_forward = - ((int )((char )bt_receive_buf[0]));
  cmd_turn = (char )bt_receive_buf[1];
  tmp___2 = __startrek_read_obstacle_flag();
  if (tmp___2) {
    cmd_forward = -100;
    cmd_turn = 0;
  }
  tmp___3 = ecrobot_get_battery_voltage();
  tmp___4 = nxt_motor_get_count(1);
  tmp___5 = nxt_motor_get_count(0);
  tmp___6 = ecrobot_get_gyro_sensor(3);
  balance_control((unsigned int )cmd_forward, (unsigned int )cmd_turn, tmp___6, gyro_offset,
                  (unsigned int )tmp___5, (unsigned int )tmp___4, tmp___3, & pwm_l,
                  & pwm_r);
  nxt_motor_set_speed(0, pwm_l, 1);
  nxt_motor_set_speed(1, pwm_r, 1);
  ecrobot_bt_data_logger(cmd_forward, cmd_turn);
  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_obstacle_flag(1);
    }
  }
  return;
}
}
__inline void __startrek_user_final(void) 
{ 
  int tmp ;

  {
  tmp = _nxtway_gs_mode_[26];
  assert(tmp == 2);
  return;
}
}
char __startrek_base_priority_OSEK_Task_ts2  =    1;
__inline static _Bool __startrek_entry_pt_OSEK_Task_ts2(void) ;
__inline static _Bool __startrek_entry_pt_OSEK_Task_ts2(void) 
{ 


  {
  OSEK_Task_ts2();
  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  =    4;
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 _Bool __startrek_entry_pt_OSEK_Task_ts1(void) ;
__inline static _Bool __startrek_entry_pt_OSEK_Task_ts1(void) 
{ 


  {
  OSEK_Task_ts1();
  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;
extern void write_mode_on_lcd(unsigned char m ) ;
void OSEK_Task_Background(void) 
{ 
  unsigned char m ;
  unsigned char tmp ;

  {
  tmp = __startrek_read_nxtway_gs_mode();
  m = tmp;
  ecrobot_status_monitor("NXTway-GS");
  write_mode_on_lcd(m);
  return;
}
}
char __startrek_base_priority_OSEK_Task_Background  =    0;
__inline static _Bool __startrek_entry_pt_OSEK_Task_Background(void) ;
__inline static _Bool __startrek_entry_pt_OSEK_Task_Background(void) 
{ 


  {
  OSEK_Task_Background();
  return ((_Bool)1);
}
}
void cil_keeperOSEK_Task_Background(void) 
{ 


  {
  __startrek_entry_pt_OSEK_Task_Background();
  return;
}
}
int __startrek_period_OSEK_Task_Background  =    96;
int __startrek_wcet_OSEK_Task_Background  =    3;
int __startrek_arrival_min_OSEK_Task_Background  =    0;
int __startrek_arrival_max_OSEK_Task_Background  =    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]);
      __VERIFIER_assume(__startrek_end_t1[0] < __startrek_start_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]);
      __VERIFIER_assume(__startrek_end_t2[0] < __startrek_start_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]);
      __VERIFIER_assume(__startrek_end_t2[0] < __startrek_start_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]);
      __VERIFIER_assume(__startrek_end_t2[0] < __startrek_start_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]);
      __VERIFIER_assume(__startrek_end_t2[1] < __startrek_start_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]);
      __VERIFIER_assume(__startrek_end_t2[1] < __startrek_start_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]);
      __VERIFIER_assume(__startrek_end_t2[1] < __startrek_start_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]);
      __VERIFIER_assume(__startrek_end_t2[2] < __startrek_start_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]);
      __VERIFIER_assume(__startrek_end_t2[2] < __startrek_start_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]);
      __VERIFIER_assume(__startrek_end_t2[2] < __startrek_start_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]);
      __VERIFIER_assume(__startrek_end_t2[3] < __startrek_start_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]);
      __VERIFIER_assume(__startrek_end_t2[3] < __startrek_start_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]);
      __VERIFIER_assume(__startrek_end_t2[3] < __startrek_start_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]);
      __VERIFIER_assume(__startrek_end_t2[4] < __startrek_start_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]);
      __VERIFIER_assume(__startrek_end_t2[4] < __startrek_start_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]);
      __VERIFIER_assume(__startrek_end_t2[4] < __startrek_start_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]);
      __VERIFIER_assume(__startrek_end_t2[5] < __startrek_start_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]);
      __VERIFIER_assume(__startrek_end_t2[5] < __startrek_start_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]);
      __VERIFIER_assume(__startrek_end_t2[5] < __startrek_start_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[6] < __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[6] < __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]);
      __VERIFIER_assume(__startrek_end_t2[6] < __startrek_start_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[7] < __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[7] < __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]);
      __VERIFIER_assume(__startrek_end_t2[7] < __startrek_start_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[8] < __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[8] < __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]);
      __VERIFIER_assume(__startrek_end_t2[8] < __startrek_start_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[9] < __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[9] < __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]);
      __VERIFIER_assume(__startrek_end_t2[9] < __startrek_start_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[10] < __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[10] < __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]);
      __VERIFIER_assume(__startrek_end_t2[10] < __startrek_start_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[11] < __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[11] < __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]);
      __VERIFIER_assume(__startrek_end_t2[11] < __startrek_start_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[12] < __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[12] < __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]);
      __VERIFIER_assume(__startrek_end_t2[12] < __startrek_start_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[13] < __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[13] < __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]);
      __VERIFIER_assume(__startrek_end_t2[13] < __startrek_start_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[14] < __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[14] < __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]);
      __VERIFIER_assume(__startrek_end_t2[14] < __startrek_start_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[15] < __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[15] < __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]);
      __VERIFIER_assume(__startrek_end_t2[15] < __startrek_start_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[16] < __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[16] < __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]);
      __VERIFIER_assume(__startrek_end_t2[16] < __startrek_start_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[17] < __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[17] < __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]);
      __VERIFIER_assume(__startrek_end_t2[17] < __startrek_start_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[18] < __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[18] < __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]);
      __VERIFIER_assume(__startrek_end_t2[18] < __startrek_start_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[19] < __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[19] < __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]);
      __VERIFIER_assume(__startrek_end_t2[19] < __startrek_start_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[20] < __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[20] < __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]);
      __VERIFIER_assume(__startrek_end_t2[20] < __startrek_start_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[21] < __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[21] < __startrek_start_t1[1]);
      }
    }
  }
}
}
__inline void __startrek_init_globals(void) 
{ 


  {
  _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];
}
}
__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 void __startrek_check_assumptions(void) 
{ 


  {
  __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]);
}
}
__inline void __startrek_user_init(void) 
{ 


  {

}
}
__inline void __startrek_check_assertions(void) 
{ 


  {

}
}
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_Background();
    __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 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 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 void __startrek_init_shared(void) 
{ 


  {
  _obstacle_flag_[0] = __startrek_hidden_obstacle_flag;
  _nxtway_gs_mode_[0] = __startrek_hidden_nxtway_gs_mode;
}
}