text: //@ ltl invariant positive: []AP(error == 0);
  
  /* Generated by CIL v. 1.7.3 */
  /* print_CIL_Input is false */
  
  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_union_OC_anon_OC_1;
  struct l_struct_union_OC_anon_OC_1;
  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_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_4_int {
     int array[4] ;
  };
  struct l_struct_seg_804964c__bss_type {
     struct l_array_4_int field0 ;
     struct l_array_4_int field1 ;
     struct l_array_4_int field2 ;
  };
  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_int {
     int array[8] ;
  };
  struct l_struct_struct_OC_uint64v8_t {
     struct l_array_8_int 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_union_OC_anon_OC_1 {
     int field0 ;
  };
  struct l_struct_struct_OC_Reg {
     struct l_struct_union_OC_anon_OC_1 field0 ;
     int field1 ;
  };
  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_int {
     int array[1] ;
  };
  struct l_struct_struct_OC_uint64v1_t {
     struct l_array_1_int 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_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_int field20 ;
  };
  struct l_struct_union_OC_FPUAbridgedTagWord {
     int field0 ;
  };
  struct l_array_10_int {
     int array[10] ;
  };
  struct l_struct_struct_OC_float80_t {
     struct l_array_10_int field0 ;
  };
  struct l_struct_union_OC_anon_OC_11 {
     struct l_struct_struct_OC_float80_t field0 ;
  };
  struct l_array_6_int {
     int array[6] ;
  };
  struct l_struct_struct_OC_FPUStackElem {
     struct l_struct_union_OC_anon_OC_11 field0 ;
     struct l_array_6_int field1 ;
  };
  struct l_array_8_struct_AC_l_struct_struct_OC_FPUStackElem {
     struct l_struct_struct_OC_FPUStackElem array[8] ;
  };
  struct l_array_96_int {
     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  ) ;  */
  extern void __VERIFIER_error() ;
  extern void *sub_8048380___VERIFIER_error(struct l_struct_struct_OC_State * , int  ,
                                            void * ) ;
  void *main(struct l_struct_struct_OC_State *tmp__1 , int tmp__2 , void *tmp__3 ) ;
  extern void __mcsema_constructor(void) ;
  extern void __mcsema_destructor(void) ;
  static struct l_struct_seg_804964c__bss_type seg_804964c__bss  ;
  
  int error = 0;
  void *main(struct l_struct_struct_OC_State *tmp__1 , int tmp__2 , void *tmp__3 ) 
  {
    int tmp__4 ;
    void *tmp__5 ;
    int tmp__6 = 0;
  
    {
    /* tmp__4 = *((int *)((int )(& seg_804964c__bss) + 8)); */
    tmp__4 = tmp__6;
    if (((unsigned int )tmp__4 == 0U) & 1) {
      goto safe_return;
    }
    block_804839f: 
    tmp__5 = sub_8048380___VERIFIER_error((struct l_struct_struct_OC_State *)0, 0, tmp__3);
    error = 1;
    goto safe_return;
    safe_return: 
    return ((void *)0);
  }
  }
  