text: /* Generated by CIL v. 1.7.3 */
  /* print_CIL_Input is false */
  
  struct l_struct___bss_start_type;
  struct l_struct___bss_start_type;
  struct l_struct_union_OC_anon;
  struct l_struct_union_OC_anon;
  struct l_struct_struct_OC_ArchState;
  struct l_struct_struct_OC_ArchState;
  struct l_struct_struct_OC_uint64v8_t;
  struct l_struct_struct_OC_uint64v8_t;
  struct l_struct_union_OC_vec512_t;
  struct l_struct_union_OC_vec512_t;
  struct l_struct_union_OC_VectorReg;
  struct l_struct_union_OC_VectorReg;
  struct l_struct_struct_OC_ArithFlags;
  struct l_struct_struct_OC_ArithFlags;
  struct l_struct_union_OC_SegmentSelector;
  struct l_struct_union_OC_SegmentSelector;
  struct l_struct_struct_OC_Segments;
  struct l_struct_struct_OC_Segments;
  struct l_struct_struct_OC_Reg;
  struct l_struct_struct_OC_Reg;
  struct l_struct_struct_OC_AddressSpace;
  struct l_struct_struct_OC_AddressSpace;
  struct l_struct_struct_OC_GPR;
  struct l_struct_struct_OC_GPR;
  struct l_struct_struct_OC_anon_OC_3;
  struct l_struct_struct_OC_anon_OC_3;
  struct l_struct_struct_OC_X87Stack;
  struct l_struct_struct_OC_X87Stack;
  struct l_struct_struct_OC_uint64v1_t;
  struct l_struct_struct_OC_uint64v1_t;
  struct l_struct_union_OC_vec64_t;
  struct l_struct_union_OC_vec64_t;
  struct l_struct_struct_OC_anon_OC_4;
  struct l_struct_struct_OC_anon_OC_4;
  struct l_struct_struct_OC_MMX;
  struct l_struct_struct_OC_MMX;
  struct l_struct_struct_OC_FPUStatusFlags;
  struct l_struct_struct_OC_FPUStatusFlags;
  struct l_struct_union_OC_FPUAbridgedTagWord;
  struct l_struct_union_OC_FPUAbridgedTagWord;
  struct l_struct_union_OC_FPUControlStatus;
  struct l_struct_union_OC_FPUControlStatus;
  struct l_struct_struct_OC_float80_t;
  struct l_struct_struct_OC_float80_t;
  struct l_struct_union_OC_anon_OC_11;
  struct l_struct_union_OC_anon_OC_11;
  struct l_struct_struct_OC_FPUStackElem;
  struct l_struct_struct_OC_FPUStackElem;
  struct l_struct_struct_OC_uint128v1_t;
  struct l_struct_struct_OC_uint128v1_t;
  struct l_struct_union_OC_vec128_t;
  struct l_struct_union_OC_vec128_t;
  struct l_struct_struct_OC_FpuFXSAVE;
  struct l_struct_struct_OC_FpuFXSAVE;
  struct l_array_8_ureplace_u8int {
     int array[8] ;
  };
  struct l_struct___bss_start_type {
     struct l_array_8_ureplace_u8int field0 ;
  };
  struct l_struct_union_OC_anon {
     int field0 ;
  };
  struct l_struct_struct_OC_ArchState {
     int field0 ;
     int field1 ;
     struct l_struct_union_OC_anon field2 ;
  };
  struct l_array_8_ureplace_u64int {
     int array[8] ;
  };
  struct l_struct_struct_OC_uint64v8_t {
     struct l_array_8_ureplace_u64int field0 ;
  };
  struct l_struct_union_OC_vec512_t {
     struct l_struct_struct_OC_uint64v8_t field0 ;
  };
  struct l_struct_union_OC_VectorReg {
     struct l_struct_union_OC_vec512_t field0 ;
  };
  struct l_array_32_struct_AC_l_struct_union_OC_VectorReg {
     struct l_struct_union_OC_VectorReg array[32] ;
  };
  struct l_struct_struct_OC_ArithFlags {
     int field0 ;
     int field1 ;
     int field2 ;
     int field3 ;
     int field4 ;
     int field5 ;
     int field6 ;
     int field7 ;
     int field8 ;
     int field9 ;
     int field10 ;
     int field11 ;
     int field12 ;
     int field13 ;
     int field14 ;
     int field15 ;
  };
  struct l_struct_union_OC_SegmentSelector {
     int field0 ;
  };
  struct l_struct_struct_OC_Segments {
     int field0 ;
     struct l_struct_union_OC_SegmentSelector field1 ;
     int field2 ;
     struct l_struct_union_OC_SegmentSelector field3 ;
     int field4 ;
     struct l_struct_union_OC_SegmentSelector field5 ;
     int field6 ;
     struct l_struct_union_OC_SegmentSelector field7 ;
     int field8 ;
     struct l_struct_union_OC_SegmentSelector field9 ;
     int field10 ;
     struct l_struct_union_OC_SegmentSelector field11 ;
  };
  struct l_struct_struct_OC_Reg {
     struct l_struct_union_OC_anon field0 ;
  };
  struct l_struct_struct_OC_AddressSpace {
     int field0 ;
     struct l_struct_struct_OC_Reg field1 ;
     int field2 ;
     struct l_struct_struct_OC_Reg field3 ;
     int field4 ;
     struct l_struct_struct_OC_Reg field5 ;
     int field6 ;
     struct l_struct_struct_OC_Reg field7 ;
     int field8 ;
     struct l_struct_struct_OC_Reg field9 ;
     int field10 ;
     struct l_struct_struct_OC_Reg field11 ;
  };
  struct l_struct_struct_OC_GPR {
     int field0 ;
     struct l_struct_struct_OC_Reg field1 ;
     int field2 ;
     struct l_struct_struct_OC_Reg field3 ;
     int field4 ;
     struct l_struct_struct_OC_Reg field5 ;
     int field6 ;
     struct l_struct_struct_OC_Reg field7 ;
     int field8 ;
     struct l_struct_struct_OC_Reg field9 ;
     int field10 ;
     struct l_struct_struct_OC_Reg field11 ;
     int field12 ;
     struct l_struct_struct_OC_Reg field13 ;
     int field14 ;
     struct l_struct_struct_OC_Reg field15 ;
     int field16 ;
     struct l_struct_struct_OC_Reg field17 ;
     int field18 ;
     struct l_struct_struct_OC_Reg field19 ;
     int field20 ;
     struct l_struct_struct_OC_Reg field21 ;
     int field22 ;
     struct l_struct_struct_OC_Reg field23 ;
     int field24 ;
     struct l_struct_struct_OC_Reg field25 ;
     int field26 ;
     struct l_struct_struct_OC_Reg field27 ;
     int field28 ;
     struct l_struct_struct_OC_Reg field29 ;
     int field30 ;
     struct l_struct_struct_OC_Reg field31 ;
     int field32 ;
     struct l_struct_struct_OC_Reg field33 ;
  };
  struct l_struct_struct_OC_anon_OC_3 {
     int field0 ;
     double field1 ;
  };
  struct l_array_8_struct_AC_l_struct_struct_OC_anon_OC_3 {
     struct l_struct_struct_OC_anon_OC_3 array[8] ;
  };
  struct l_struct_struct_OC_X87Stack {
     struct l_array_8_struct_AC_l_struct_struct_OC_anon_OC_3 field0 ;
  };
  struct l_array_1_ureplace_u64int {
     int array[1] ;
  };
  struct l_struct_struct_OC_uint64v1_t {
     struct l_array_1_ureplace_u64int field0 ;
  };
  struct l_struct_union_OC_vec64_t {
     struct l_struct_struct_OC_uint64v1_t field0 ;
  };
  struct l_struct_struct_OC_anon_OC_4 {
     int field0 ;
     struct l_struct_union_OC_vec64_t field1 ;
  };
  struct l_array_8_struct_AC_l_struct_struct_OC_anon_OC_4 {
     struct l_struct_struct_OC_anon_OC_4 array[8] ;
  };
  struct l_struct_struct_OC_MMX {
     struct l_array_8_struct_AC_l_struct_struct_OC_anon_OC_4 field0 ;
  };
  struct l_array_4_ureplace_u8int {
     int array[4] ;
  };
  struct l_struct_struct_OC_FPUStatusFlags {
     int field0 ;
     int field1 ;
     int field2 ;
     int field3 ;
     int field4 ;
     int field5 ;
     int field6 ;
     int field7 ;
     int field8 ;
     int field9 ;
     int field10 ;
     int field11 ;
     int field12 ;
     int field13 ;
     int field14 ;
     int field15 ;
     int field16 ;
     int field17 ;
     int field18 ;
     int field19 ;
     struct l_array_4_ureplace_u8int field20 ;
  };
  struct l_struct_union_OC_FPUAbridgedTagWord {
     int field0 ;
  };
  struct l_struct_union_OC_FPUControlStatus {
     int field0 ;
  };
  struct l_array_10_ureplace_u8int {
     int array[10] ;
  };
  struct l_struct_struct_OC_float80_t {
     struct l_array_10_ureplace_u8int field0 ;
  };
  struct l_struct_union_OC_anon_OC_11 {
     struct l_struct_struct_OC_float80_t field0 ;
  };
  struct l_array_6_ureplace_u8int {
     int array[6] ;
  };
  struct l_struct_struct_OC_FPUStackElem {
     struct l_struct_union_OC_anon_OC_11 field0 ;
     struct l_array_6_ureplace_u8int field1 ;
  };
  struct l_array_8_struct_AC_l_struct_struct_OC_FPUStackElem {
     struct l_struct_struct_OC_FPUStackElem array[8] ;
  };
  struct l_array_96_ureplace_u8int {
     int array[96] ;
  };
  struct l_struct_struct_OC_SegmentShadow {
     struct l_struct_union_OC_anon field0 ;
     int field1 ;
     int field2 ;
  };
  struct l_struct_struct_OC_SegmentCaches {
     struct l_struct_struct_OC_SegmentShadow field0 ;
     struct l_struct_struct_OC_SegmentShadow field1 ;
     struct l_struct_struct_OC_SegmentShadow field2 ;
     struct l_struct_struct_OC_SegmentShadow field3 ;
     struct l_struct_struct_OC_SegmentShadow field4 ;
     struct l_struct_struct_OC_SegmentShadow field5 ;
  };
  struct l_struct_struct_OC_State {
     struct l_struct_struct_OC_ArchState field0 ;
     struct l_array_32_struct_AC_l_struct_union_OC_VectorReg field1 ;
     struct l_struct_struct_OC_ArithFlags field2 ;
     struct l_struct_union_OC_anon field3 ;
     struct l_struct_struct_OC_Segments field4 ;
     struct l_struct_struct_OC_AddressSpace field5 ;
     struct l_struct_struct_OC_GPR field6 ;
     struct l_struct_struct_OC_X87Stack field7 ;
     struct l_struct_struct_OC_MMX field8 ;
     struct l_struct_struct_OC_FPUStatusFlags field9 ;
     struct l_struct_union_OC_anon field10 ;
     struct l_struct_struct_OC_SegmentCaches field12 ;
  };
  /* compiler builtin: 
     void __builtin_va_copy(__builtin_va_list  , __builtin_va_list  ) ;  */
  /* compiler builtin: 
     double __builtin_huge_val(void) ;  */
  /* compiler builtin: 
     int __builtin_clzl(unsigned long  ) ;  */
  /* compiler builtin: 
     float __builtin_frexpf(float  , int * ) ;  */
  /* compiler builtin: 
     long double __builtin_fmodl(long double  ) ;  */
  /* compiler builtin: 
     double __builtin_atan(double  ) ;  */
  /* compiler builtin: 
     int __builtin___fprintf_chk(void * , int  , char const   *  , ...) ;  */
  /* compiler builtin: 
     float __builtin_ceilf(float  ) ;  */
  /* compiler builtin: 
     void __attribute__((__overloaded__))  __sync_and_and_fetch(...) ;  */
  /* compiler builtin: 
     void __attribute__((__overloaded__))  __sync_fetch_and_or(...) ;  */
  /* compiler builtin: 
     void __builtin_return(void const   * ) ;  */
  /* compiler builtin: 
     int __builtin_popcountll(unsigned long long  ) ;  */
  /* compiler builtin: 
     long double __builtin_asinl(long double  ) ;  */
  /* compiler builtin: 
     float __builtin_atanf(float  ) ;  */
  /* compiler builtin: 
     int __builtin_ffsll(unsigned long long  ) ;  */
  /* compiler builtin: 
     float __attribute__((____vector_size____(16)))  __builtin_ia32_addps(float __attribute__((____vector_size____(16)))   ,
                                                                          float __attribute__((____vector_size____(16)))   ) ;  */
  /* compiler builtin: 
     unsigned long __builtin_strcspn(char const   * , char const   * ) ;  */
  /* compiler builtin: 
     float __builtin_asinf(float  ) ;  */
  /* compiler builtin: 
     float __attribute__((____vector_size____(16)))  __builtin_ia32_maxps(float __attribute__((____vector_size____(16)))   ,
                                                                          float __attribute__((____vector_size____(16)))   ) ;  */
  /* compiler builtin: 
     float __attribute__((____vector_size____(16)))  __builtin_ia32_unpckhps(float __attribute__((____vector_size____(16)))   ,
                                                                             float __attribute__((____vector_size____(16)))   ) ;  */
  /* compiler builtin: 
     double __builtin_acos(double  ) ;  */
  /* compiler builtin: 
     int __builtin_va_arg_pack(void) ;  */
  /* compiler builtin: 
     char *__builtin___strncpy_chk(char * , char const   * , unsigned long  , unsigned long  ) ;  */
  /* compiler builtin: 
     int __builtin___sprintf_chk(char * , int  , unsigned long  , char const   *  , ...) ;  */
  /* compiler builtin: 
     double __builtin_powi(double  , int  ) ;  */
  /* compiler builtin: 
     char *__builtin_strchr(char * , int  ) ;  */
  /* compiler builtin: 
     char *__builtin___strncat_chk(char * , char const   * , unsigned long  , unsigned long  ) ;  */
  /* compiler builtin: 
     long double __builtin_huge_vall(void) ;  */
  /* compiler builtin: 
     int __builtin_ffsl(unsigned long  ) ;  */
  /* compiler builtin: 
     int __builtin___vprintf_chk(int  , char const   * , __builtin_va_list  ) ;  */
  /* compiler builtin: 
     float __attribute__((____vector_size____(16)))  __builtin_ia32_unpcklps(float __attribute__((____vector_size____(16)))   ,
                                                                             float __attribute__((____vector_size____(16)))   ) ;  */
  /* compiler builtin: 
     char *__builtin_strncat(char * , char const   * , unsigned long  ) ;  */
  /* compiler builtin: 
     int __builtin_ctzll(unsigned long long  ) ;  */
  /* compiler builtin: 
     double __builtin_cosh(double  ) ;  */
  /* compiler builtin: 
     void __builtin_stdarg_start(__builtin_va_list  ) ;  */
  /* compiler builtin: 
     float __builtin_tanhf(float  ) ;  */
  /* compiler builtin: 
     void __attribute__((__overloaded__))  __sync_fetch_and_xor(...) ;  */
  /* compiler builtin: 
     void *__builtin_mempcpy(void * , void const   * , unsigned long  ) ;  */
  /* compiler builtin: 
     long double __builtin_frexpl(long double  , int * ) ;  */
  /* compiler builtin: 
     float __builtin_tanf(float  ) ;  */
  /* compiler builtin: 
     long double __builtin_logl(long double  ) ;  */
  /* compiler builtin: 
     long double __builtin_sqrtl(long double  ) ;  */
  /* compiler builtin: 
     int __builtin_parity(unsigned int  ) ;  */
  /* compiler builtin: 
     void __builtin_va_arg(__builtin_va_list  , unsigned long  , void * ) ;  */
  /* compiler builtin: 
     long __builtin_expect(long  , long  ) ;  */
  /* compiler builtin: 
     long double __builtin_coshl(long double  ) ;  */
  /* compiler builtin: 
     long double __builtin_cosl(long double  ) ;  */
  /* compiler builtin: 
     float __builtin_cosf(float  ) ;  */
  /* compiler builtin: 
     int __builtin___printf_chk(int  , char const   *  , ...) ;  */
  /* compiler builtin: 
     void __sync_synchronize(...) ;  */
  /* compiler builtin: 
     long double __builtin_acosl(long double  ) ;  */
  /* compiler builtin: 
     int __builtin___vfprintf_chk(void * , int  , char const   * , __builtin_va_list  ) ;  */
  /* compiler builtin: 
     void *__builtin___mempcpy_chk(void * , void const   * , unsigned long  , unsigned long  ) ;  */
  /* compiler builtin: 
     void __attribute__((__overloaded__))  __sync_or_and_fetch(...) ;  */
  /* compiler builtin: 
     void __builtin_prefetch(void const   *  , ...) ;  */
  /* compiler builtin: 
     long double __builtin_nansl(char const   * ) ;  */
  /* compiler builtin: 
     double __builtin_fmod(double  ) ;  */
  /* compiler builtin: 
     int __builtin_clz(unsigned int  ) ;  */
  /* compiler builtin: 
     void __attribute__((__overloaded__))  __sync_val_compare_and_swap(...) ;  */
  /* compiler builtin: 
     double __builtin_log10(double  ) ;  */
  /* compiler builtin: 
     char *__builtin___strcat_chk(char * , char const   * , unsigned long  ) ;  */
  /* compiler builtin: 
     double __builtin_tanh(double  ) ;  */
  /* compiler builtin: 
     float __builtin_modff(float  , float * ) ;  */
  /* compiler builtin: 
     double __builtin_sin(double  ) ;  */
  /* compiler builtin: 
     double __builtin_frexp(double  , int * ) ;  */
  /* compiler builtin: 
     float __builtin_acosf(float  ) ;  */
  /* compiler builtin: 
     void __attribute__((__overloaded__))  __sync_add_and_fetch(...) ;  */
  /* compiler builtin: 
     long double __builtin_sinhl(long double  ) ;  */
  /* compiler builtin: 
     char *__builtin___stpcpy_chk(char * , char const   * , unsigned long  ) ;  */
  /* compiler builtin: 
     long double __builtin_ldexpl(long double  , int  ) ;  */
  /* compiler builtin: 
     double __builtin_fabs(double  ) ;  */
  /* compiler builtin: 
     void __attribute__((__overloaded__))  __sync_fetch_and_nand(...) ;  */
  /* compiler builtin: 
     void *__builtin_apply(void (*)() , void * , unsigned long  ) ;  */
  /* compiler builtin: 
     float __builtin_sinf(float  ) ;  */
  /* compiler builtin: 
     double __builtin_ceil(double  ) ;  */
  /* compiler builtin: 
     long double __builtin_powil(long double  , int  ) ;  */
  /* compiler builtin: 
     void __builtin_va_start(__builtin_va_list  ) ;  */
  /* compiler builtin: 
     long double __builtin_expl(long double  ) ;  */
  /* compiler builtin: 
     int __builtin_constant_p(int  ) ;  */
  /* compiler builtin: 
     double __builtin_log(double  ) ;  */
  /* compiler builtin: 
     float __builtin_expf(float  ) ;  */
  /* compiler builtin: 
     int __builtin_types_compatible_p(unsigned long  , unsigned long  ) ;  */
  /* compiler builtin: 
     int __builtin_ctz(unsigned int  ) ;  */
  /* compiler builtin: 
     long double __builtin_atan2l(long double  , long double  ) ;  */
  /* compiler builtin: 
     void *__builtin_apply_args(void) ;  */
  /* compiler builtin: 
     char *__builtin_strpbrk(char const   * , char const   * ) ;  */
  /* compiler builtin: 
     char *__builtin_strcpy(char * , char const   * ) ;  */
  /* compiler builtin: 
     double __builtin_sqrt(double  ) ;  */
  /* compiler builtin: 
     __builtin_va_list __builtin_next_arg(void) ;  */
  /* compiler builtin: 
     float __builtin_logf(float  ) ;  */
  /* compiler builtin: 
     float __builtin_log10f(float  ) ;  */
  /* compiler builtin: 
     long double __builtin_fabsl(long double  ) ;  */
  /* compiler builtin: 
     unsigned long __builtin_strlen(char const   * ) ;  */
  /* compiler builtin: 
     long double __builtin_floorl(long double  ) ;  */
  /* compiler builtin: 
     int __builtin_ffs(unsigned int  ) ;  */
  /* compiler builtin: 
     double __builtin_inf(void) ;  */
  /* compiler builtin: 
     float __builtin_floorf(float  ) ;  */
  /* compiler builtin: 
     void *__builtin_memcpy(void * , void const   * , unsigned long  ) ;  */
  /* compiler builtin: 
     void *__builtin___memcpy_chk(void * , void const   * , unsigned long  , unsigned long  ) ;  */
  /* compiler builtin: 
     void __attribute__((__overloaded__))  __sync_sub_and_fetch(...) ;  */
  /* compiler builtin: 
     int __builtin_parityl(unsigned long  ) ;  */
  /* compiler builtin: 
     void __attribute__((__overloaded__))  __sync_nand_and_fetch(...) ;  */
  /* compiler builtin: 
     float __attribute__((____vector_size____(16)))  __builtin_ia32_subps(float __attribute__((____vector_size____(16)))   ,
                                                                          float __attribute__((____vector_size____(16)))   ) ;  */
  /* compiler builtin: 
     void __attribute__((__overloaded__))  __sync_lock_test_and_set(...) ;  */
  /* compiler builtin: 
     unsigned long __builtin_strspn(char const   * , char const   * ) ;  */
  /* compiler builtin: 
     void __builtin_varargs_start(__builtin_va_list  ) ;  */
  /* compiler builtin: 
     int __builtin_parityll(unsigned long long  ) ;  */
  /* compiler builtin: 
     void __builtin_va_end(__builtin_va_list  ) ;  */
  /* compiler builtin: 
     void __builtin_bzero(void * , unsigned long  ) ;  */
  /* compiler builtin: 
     int __builtin_strncmp(char const   * , char const   * , unsigned long  ) ;  */
  /* compiler builtin: 
     double __builtin_nan(char const   * ) ;  */
  /* compiler builtin: 
     void __attribute__((__overloaded__))  __sync_xor_and_fetch(...) ;  */
  /* compiler builtin: 
     int __builtin___vsprintf_chk(char * , int  , unsigned long  , char const   * ,
                                  __builtin_va_list  ) ;  */
  /* compiler builtin: 
     int __builtin___snprintf_chk(char * , unsigned long  , int  , unsigned long  ,
                                  char const   *  , ...) ;  */
  /* compiler builtin: 
     float __builtin_sqrtf(float  ) ;  */
  /* compiler builtin: 
     double __builtin_nans(char const   * ) ;  */
  /* compiler builtin: 
     long double __builtin_atanl(long double  ) ;  */
  /* compiler builtin: 
     double __builtin_exp(double  ) ;  */
  /* compiler builtin: 
     int __builtin_clzll(unsigned long long  ) ;  */
  /* compiler builtin: 
     float __builtin_huge_valf(void) ;  */
  /* compiler builtin: 
     float __builtin_coshf(float  ) ;  */
  /* compiler builtin: 
     float __builtin_nansf(char const   * ) ;  */
  /* compiler builtin: 
     void __attribute__((__overloaded__))  __sync_fetch_and_add(...) ;  */
  /* compiler builtin: 
     int __builtin___vsnprintf_chk(char * , unsigned long  , int  , unsigned long  ,
                                   char const   * , __builtin_va_list  ) ;  */
  /* compiler builtin: 
     float __builtin_nanf(char const   * ) ;  */
  /* compiler builtin: 
     int __builtin_strcmp(char const   * , char const   * ) ;  */
  /* compiler builtin: 
     _Bool __sync_bool_compare_and_swap(...) ;  */
  /* compiler builtin: 
     float __builtin_ldexpf(float  , int  ) ;  */
  /* compiler builtin: 
     double __builtin_atan2(double  , double  ) ;  */
  /* compiler builtin: 
     int __builtin_popcountl(unsigned long  ) ;  */
  /* compiler builtin: 
     float __builtin_powif(float  , int  ) ;  */
  /* compiler builtin: 
     long double __builtin_ceill(long double  ) ;  */
  /* compiler builtin: 
     char *__builtin___strcpy_chk(char * , char const   * , unsigned long  ) ;  */
  /* compiler builtin: 
     long double __builtin_log10l(long double  ) ;  */
  /* compiler builtin: 
     void *__builtin___memmove_chk(void * , void const   * , unsigned long  , unsigned long  ) ;  */
  /* compiler builtin: 
     void __attribute__((__overloaded__))  __sync_fetch_and_and(...) ;  */
  /* compiler builtin: 
     void *__builtin_return_address(unsigned int  ) ;  */
  /* compiler builtin: 
     float __builtin_fabsf(float  ) ;  */
  /* compiler builtin: 
     double __builtin_floor(double  ) ;  */
  /* compiler builtin: 
     double __builtin_cos(double  ) ;  */
  /* compiler builtin: 
     void __attribute__((__overloaded__))  __sync_fetch_and_sub(...) ;  */
  /* compiler builtin: 
     unsigned long __builtin_object_size(void * , int  ) ;  */
  /* compiler builtin: 
     void *__builtin_memset(void * , int  , int  ) ;  */
  /* compiler builtin: 
     void *__builtin_alloca(unsigned long  ) ;  */
  /* compiler builtin: 
     long double __builtin_nanl(char const   * ) ;  */
  /* compiler builtin: 
     float __builtin_atan2f(float  , float  ) ;  */
  /* compiler builtin: 
     int __builtin_popcount(unsigned int  ) ;  */
  /* compiler builtin: 
     int __builtin_va_arg_pack_len(void) ;  */
  /* compiler builtin: 
     long double __builtin_tanl(long double  ) ;  */
  /* compiler builtin: 
     double __builtin_sinh(double  ) ;  */
  /* compiler builtin: 
     void __builtin_bcopy(void const   * , void * , unsigned long  ) ;  */
  /* compiler builtin: 
     void __sync_lock_release(...) ;  */
  /* compiler builtin: 
     long double __builtin_modfl(long double  , long double * ) ;  */
  /* compiler builtin: 
     char *__builtin_stpcpy(char * , char const   * ) ;  */
  /* compiler builtin: 
     long double __builtin_sinl(long double  ) ;  */
  /* compiler builtin: 
     double __builtin_asin(double  ) ;  */
  /* compiler builtin: 
     float __builtin_sinhf(float  ) ;  */
  /* compiler builtin: 
     int __builtin_ctzl(unsigned long  ) ;  */
  /* compiler builtin: 
     long double __builtin_tanhl(long double  ) ;  */
  /* compiler builtin: 
     int __builtin_bswap32(int  ) ;  */
  /* compiler builtin: 
     double __builtin_ldexp(double  , int  ) ;  */
  /* compiler builtin: 
     long double __builtin_infl(void) ;  */
  /* compiler builtin: 
     long __builtin_bswap64(long  ) ;  */
  /* compiler builtin: 
     float __builtin_fmodf(float  ) ;  */
  /* compiler builtin: 
     float __attribute__((____vector_size____(16)))  __builtin_ia32_mulps(float __attribute__((____vector_size____(16)))   ,
                                                                          float __attribute__((____vector_size____(16)))   ) ;  */
  /* compiler builtin: 
     double __builtin_tan(double  ) ;  */
  /* compiler builtin: 
     char *__builtin_strncpy(char * , char const   * , unsigned long  ) ;  */
  /* compiler builtin: 
     float __builtin_inff(void) ;  */
  /* compiler builtin: 
     void *__builtin___memset_chk(void * , int  , unsigned long  , unsigned long  ) ;  */
  /* compiler builtin: 
     void *__builtin_frame_address(unsigned int  ) ;  */
  struct l_struct_struct_OC_State *globalState ;
  extern void __VERIFIER_error() ;
  int __VERIFIER_nondet_int() { int x; return x; };
  extern void __mcsema_constructor(void) ;
  extern void __mcsema_destructor(void) ;
  struct l_struct___bss_start_type __bss_start  ;
  int STATE_REG_RAX  ;
  int STATE_REG_RBX  ;
  int STATE_REG_RCX  ;
  int STATE_REG_RDX  ;
  int STATE_REG_RSI  ;
  int STATE_REG_RDI  ;
  int STATE_REG_RSP  ;
  int STATE_REG_RBP  ;
  int STATE_REG_R8  ;
  int STATE_REG_R9  ;
  int STATE_REG_R10  ;
  int STATE_REG_R11  ;
  int STATE_REG_R12  ;
  int STATE_REG_R13  ;
  int STATE_REG_R14  ;
  int STATE_REG_R15  ;
  int STATE_REG_IP  ;
  static int llvm_OC_ctpop_OC_i32(int x ) 
  { 
    int c ;
  
    {
    c = 0;
    while (x != 0) {
      if (x & 1) {
        c ++;
      }
      x >>= 1;
    }
    return (c);
  }
  }
  static int llvm_select_u32(int condition , int iftrue , int ifnot ) 
  { 
    int r ;
  
    {
    r = condition ? iftrue : ifnot;
    return (r);
  }
  }
  static int llvm_add_u32(int a , int b ) 
  { 
    int r ;
  
    {
    r = a + b;
    return (r);
  }
  }
  static int llvm_add_u64(int a , int b ) 
  { 
    int r ;
  
    {
    r = a + b;
    return (r);
  }
  }
  static int llvm_lshr_u32(int a , int b ) 
  { 
    int r ;
  
    {
    r = a >> b;
    return (r);
  }
  }
  static int llvm_lshr_u64(int a , int b ) 
  { 
    int r ;
  
    {
    r = a >> b;
    return (r);
  }
  }
  static int llvm_and_u8(int a , int b ) 
  { 
    int r ;
  
    {
    r = a & b;
    return (r);
  }
  }
  static int llvm_xor_u8(int a , int b ) 
  { 
    int r ;
  
    {
    r = a ^ b;
    return (r);
  }
  }
  struct l_struct_struct_OC_State global_state  ;
  struct l_struct_struct_OC_State *globalState  =    & global_state;
  int main() 
  { 
    struct l_struct_struct_OC_State *tmp__1; 
    int tmp__2;
    void *tmp__3; 
    struct l_struct_struct_OC_State *tmp__4 ;
    int tmp__5 ;
    int tmp__6 ;
    int tmp__7 ;
    int tmp__8 ;
    int *tmp__9 ;
    int tmp__10 ;
    int *tmp__11 ;
    int *tmp__12 ;
    int *tmp__13 ;
    int tmp__14 ;
    int *tmp__15 ;
    int tmp__16 ;
    int *tmp__17 ;
    int tmp__18 ;
    void *tmp__19 ;
    int tmp__20 ;
    int tmp__21 ;
    int *tmp__22 ;
    int *tmp__23 ;
    int tmp__24 ;
    int tmp__25 ;
    int tmp__26 ;
    int tmp__27 ;
    int tmp__28 ;
    int tmp__29 ;
    int tmp__30 ;
    int tmp__31 ;
    int tmp__32 ;
    int tmp__32__PHI_TEMPORARY ;
    int _2e_pre ;
    int tmp__33 ;
    int tmp__34 ;
    int tmp__35 ;
    int tmp__36 ;
    int _2e_lcssa3 ;
    int _2e_lcssa3__PHI_TEMPORARY ;
    int _2e_lcssa2 ;
    int _2e_lcssa2__PHI_TEMPORARY ;
    int _2e_lcssa1 ;
    int _2e_lcssa1__PHI_TEMPORARY ;
    int _2e_lcssa ;
    int _2e_lcssa__PHI_TEMPORARY ;
    int tmp__37 ;
    int tmp__38 ;
    int tmp__39 ;
    int tmp ;
    int tmp___0 ;
    int tmp___1 ;
    int tmp___2 ;
    int tmp___3 ;
    int tmp___4 ;
    int tmp___5 ;
    int tmp___6 ;
    int tmp___7 ;
    int tmp___8 ;
    int tmp___9 ;
    int tmp___10 ;
    int tmp___11 ;
    int tmp___12 ;
    int tmp___13 ;
    int tmp___14 ;
    int tmp___15 ;
    int tmp___16 ;
  
    {
    tmp__4 = globalState;
    tmp__5 = STATE_REG_RBP;
    tmp__6 = STATE_REG_RSP;
    tmp__7 = tmp__6 + -8;
    *((int *)tmp__7) = tmp__5;
    STATE_REG_RBP = tmp__7;
    tmp__8 = tmp__6 + -24;
    tmp__9 = & tmp__4->field2.field1;
    *tmp__9 = (tmp__7 < 16) & 1;
    tmp__10 = llvm_OC_ctpop_OC_i32(tmp__8 & 255);
    tmp__11 = & tmp__4->field2.field3;
    tmp = tmp__10 & 1;
    *tmp__11 = tmp ^ 1;
    tmp__12 = & tmp__4->field2.field5;
    tmp___0 = (int )(((unsigned long )tmp__7 ^ 16UL) ^ (unsigned long )tmp__8) >> 4;
    *tmp__12 = tmp___0 & 1;
    tmp__13 = & tmp__4->field2.field7;
    *tmp__13 = ((unsigned long )tmp__8 == 0UL) & 1;
    tmp__14 = tmp__8 >> 63;
    tmp__15 = & tmp__4->field2.field9;
    *tmp__15 = tmp__14;
    tmp__16 = tmp__7 >> 63;
    tmp__17 = & tmp__4->field2.field13;
    tmp___1 = (tmp__14 ^ tmp__16) + tmp__16;
    *tmp__17 = ((unsigned long )tmp___1 == 2UL) & 1;
    tmp___2 = tmp__6 + -12;
    *((int *)tmp___2) = 0;
    tmp___3 = tmp__6 + -16;
    *((int *)tmp___3) = 100;
    STATE_REG_RAX = 0;
    tmp__18 = tmp__6 + -32;
    *((int *)tmp__18) = tmp__2 + 36;
    STATE_REG_RSP = tmp__18;
    STATE_REG_RAX = __VERIFIER_nondet_int();
    tmp__20 = STATE_REG_RBP;
    tmp__21 = STATE_REG_RAX;
    tmp___4 = tmp__20 + -12;
    tmp__22 = (int *)tmp___4;
    *tmp__22 = tmp__21;
    tmp___5 = tmp__20 + -4;
    tmp__23 = (int *)tmp___5;
    tmp__24 = *tmp__23;
    tmp__25 = tmp__24 + -39;
    tmp__26 = tmp__25 >> 31;
    tmp__27 = tmp__24 >> 31;
    tmp___7 = (tmp__26 ^ tmp__27) + tmp__27;
    if (! (((((unsigned int )tmp__25 == 0U) & 1) | (((((unsigned int )tmp__26 != 0U) & 1) ^ (((unsigned int )tmp___7 == 2U) & 1)) & 1)) & 1)) {
      _2e_lcssa3__PHI_TEMPORARY = tmp__24;
      _2e_lcssa2__PHI_TEMPORARY = tmp__25;
      _2e_lcssa1__PHI_TEMPORARY = tmp__26;
      tmp___6 = (tmp__26 ^ tmp__27) + tmp__27;
      _2e_lcssa__PHI_TEMPORARY = ((unsigned int )tmp___6 == 2U) & 1;
      goto block_401150;
    }
    block_40113a_2e_preheader: 
    tmp___8 = llvm_select_u32(((unsigned int )tmp__21 == 0U) & 1, 1, 2);
    tmp__28 = tmp___8 + tmp__24;
    *tmp__23 = tmp__28;
    tmp__29 = tmp__28 + -39;
    tmp__30 = tmp__29 >> 31;
    tmp__31 = tmp__28 >> 31;
    tmp___10 = (tmp__30 ^ tmp__31) + tmp__31;
    if (((((unsigned int )tmp__29 == 0U) & 1) | (((((unsigned int )tmp__30 != 0U) & 1) ^ (((unsigned int )tmp___10 == 2U) & 1)) & 1)) & 1) {
      tmp__32__PHI_TEMPORARY = tmp__28;
      goto block_40113a_2e_block_40113a_crit_edge;
    } else {
      _2e_lcssa3__PHI_TEMPORARY = tmp__28;
      _2e_lcssa2__PHI_TEMPORARY = tmp__29;
      _2e_lcssa1__PHI_TEMPORARY = tmp__30;
      tmp___9 = (tmp__30 ^ tmp__31) + tmp__31;
      _2e_lcssa__PHI_TEMPORARY = ((unsigned int )tmp___9 == 2U) & 1;
      goto block_401150;
    }
    while (1) {
      block_40113a_2e_block_40113a_crit_edge: 
      tmp__32 = tmp__32__PHI_TEMPORARY;
      _2e_pre = *tmp__22;
      tmp___11 = llvm_select_u32(((unsigned int )_2e_pre == 0U) & 1, 1, 2);
      tmp__33 = tmp___11 + tmp__32;
      *tmp__23 = tmp__33;
      tmp__34 = tmp__33 + -39;
      tmp__35 = tmp__34 >> 31;
      tmp__36 = tmp__33 >> 31;
      tmp___13 = (tmp__35 ^ tmp__36) + tmp__36;
      if (((((unsigned int )tmp__34 == 0U) & 1) | (((((unsigned int )tmp__35 != 0U) & 1) ^ (((unsigned int )tmp___13 == 2U) & 1)) & 1)) & 1) {
        tmp__32__PHI_TEMPORARY = tmp__33;
        goto block_40113a_2e_block_40113a_crit_edge;
      } else {
        _2e_lcssa3__PHI_TEMPORARY = tmp__33;
        _2e_lcssa2__PHI_TEMPORARY = tmp__34;
        _2e_lcssa1__PHI_TEMPORARY = tmp__35;
        tmp___12 = (tmp__35 ^ tmp__36) + tmp__36;
        _2e_lcssa__PHI_TEMPORARY = ((unsigned int )tmp___12 == 2U) & 1;
        goto block_401150;
      }
    }
    block_401150: 
    _2e_lcssa3 = _2e_lcssa3__PHI_TEMPORARY;
    _2e_lcssa2 = _2e_lcssa2__PHI_TEMPORARY;
    _2e_lcssa1 = _2e_lcssa1__PHI_TEMPORARY;
    _2e_lcssa = _2e_lcssa__PHI_TEMPORARY & 1;
    tmp__37 = llvm_OC_ctpop_OC_i32(_2e_lcssa2 & 255);
    *tmp__9 = (_2e_lcssa3 < 39) & 1;
    tmp___14 = tmp__37 & 1;
    *tmp__11 = tmp___14 ^ 1;
    tmp___15 = (_2e_lcssa2 ^ _2e_lcssa3) >> 4;
    *tmp__12 = tmp___15 & 1;
    *tmp__13 = 0;
    *tmp__15 = _2e_lcssa1;
    *tmp__17 = _2e_lcssa;
    STATE_REG_RAX = 0;
    tmp__38 = *((int *)tmp__20);
    STATE_REG_RBP = tmp__38;
    tmp___16 = tmp__20 + 8;
    tmp__39 = *((int *)tmp___16);
    STATE_REG_IP = tmp__39;
    STATE_REG_RSP = tmp__20 + 16;
    return (tmp__19);
  }
  }
  