/* Generated by CIL v. 1.3.5 */
/* print_CIL_Input is false */

#define CCURED_SPLIT_ARGUMENTS
// #define CCURED_ALLOW_PARTIAL_ELEMENTS_IN_SEQUENCE
// #define CCURED_LOG_NON_POINTERS
#define CCURED_USE_STRINGS
// #define CCURED_FAIL_IS_TERSE
// #define CCURED_ALWAYS_STOP_ON_ERROR
// Include the definition of the checkers
#define CCURED
#define CCURED_POST
#include "ccuredcheck.h"
struct printf_arguments {
   int i ;
   double d ;
   char * __ROSTRING  s ;
   long long ll ;
};
extern void __ccuredInit(void) ;
extern  __attribute__((__noreturn__)) void abort_deepcopy(char *errmsg ) ;
int ( __SEQ  g)[8]  ;
struct meta_seq_void {
   void *_b ;
   void *_e ;
}   ;
struct meta_seq_int {
   void *_b ;
   void *_e ;
}   ;
int main(void) ;
int main(void) 
{ int *pg ;
  int * __SEQ  sg ;
  int * __SEQ  tmp ;
  int pg1 ;
  int * __SEQ  sg1 ;
  int * __SEQ  tmp___0 ;
  int __retres7 ;
  void * __SEQ  __cil_tmp8 ;
  void * __SEQ  __cil_tmp9 ;
  int * __SEQ  __cil_tmp10 ;
  int * __SEQ  __cil_tmp11 ;
  void * __SEQ  __cil_tmp12 ;
  void * __SEQ  __cil_tmp13 ;
  int * __SEQ  __cil_tmp14 ;
  int * __SEQ  __cil_tmp15 ;
  void *sg_b28 ;
  void *sg_e29 ;
  void *tmp_b30 ;
  void *tmp_e31 ;
  void *sg1_b32 ;
  void *sg1_e33 ;
  void *tmp___0_b34 ;
  void *tmp___0_e35 ;
  void *__cil_tmp8_b36 ;
  void *__cil_tmp8_e37 ;
  void *__cil_tmp9_b38 ;
  void *__cil_tmp9_e39 ;
  void *__cil_tmp10_b40 ;
  void *__cil_tmp10_e41 ;
  void *__cil_tmp11_b42 ;
  void *__cil_tmp11_e43 ;
  void *__cil_tmp12_b44 ;
  void *__cil_tmp12_e45 ;
  void *__cil_tmp13_b46 ;
  void *__cil_tmp13_e47 ;
  void *__cil_tmp14_b48 ;
  void *__cil_tmp14_e49 ;
  void *__cil_tmp15_b50 ;
  void *__cil_tmp15_e51 ;

  {
  tmp___0_e35 = (void *)0;
  tmp___0_b34 = (void *)0;
  tmp___0 = (int */* __SEQ  */)0;
  sg1_e33 = (void *)0;
  sg1_b32 = (void *)0;
  sg1 = (int */* __SEQ  */)0;
  tmp_e31 = (void *)0;
  tmp_b30 = (void *)0;
  tmp = (int */* __SEQ  */)0;
  sg_e29 = (void *)0;
  sg_b28 = (void *)0;
  sg = (int */* __SEQ  */)0;
  pg = (int *)0;
  __ccuredAlwaysStopOnError = 0;
  __ccuredUseStrings = 1;
  __ccuredLogNonPointers = 0;
  __ccuredInit();
  pg = (int *)((int *)(& g[2]));
  __cil_tmp9 = (void *)((void *)pg);
  __cil_tmp9_b38 = g;
  __cil_tmp9_e39 = g + 8;
  __cil_tmp8_e37 = __cil_tmp9_e39;
  __cil_tmp8_b36 = __cil_tmp9_b38;
  __cil_tmp8 = __cil_tmp9;
  CHECK_SEQALIGN(sizeof(int ), (void *)((int */* __SEQ  */)__cil_tmp8), __cil_tmp8_b36,
                 __cil_tmp8_e37);
  __cil_tmp10 = (int */* __SEQ  */)__cil_tmp8;
  __cil_tmp10_b40 = __cil_tmp8_b36;
  __cil_tmp10_e41 = __cil_tmp8_e37;
  tmp_e31 = __cil_tmp10_e41;
  tmp_b30 = __cil_tmp10_b40;
  tmp = __cil_tmp10;
  __cil_tmp11 = tmp;
  __cil_tmp11_b42 = tmp_b30;
  __cil_tmp11_e43 = tmp_e31;
  sg_e29 = __cil_tmp11_e43;
  sg_b28 = __cil_tmp11_b42;
  sg = __cil_tmp11;
  pg1 = (int )(& g[3]);
  __cil_tmp13 = (void *)((void *)pg1);
  __cil_tmp13_b46 = g;
  __cil_tmp13_e47 = g + 8;
  __cil_tmp12_e45 = __cil_tmp13_e47;
  __cil_tmp12_b44 = __cil_tmp13_b46;
  __cil_tmp12 = __cil_tmp13;
  CHECK_SEQALIGN(sizeof(int ), (void *)((int */* __SEQ  */)__cil_tmp12), __cil_tmp12_b44,
                 __cil_tmp12_e45);
  __cil_tmp14 = (int */* __SEQ  */)__cil_tmp12;
  __cil_tmp14_b48 = __cil_tmp12_b44;
  __cil_tmp14_e49 = __cil_tmp12_e45;
  tmp___0_e35 = __cil_tmp14_e49;
  tmp___0_b34 = __cil_tmp14_b48;
  tmp___0 = __cil_tmp14;
  __cil_tmp15 = tmp___0;
  __cil_tmp15_b50 = tmp___0_b34;
  __cil_tmp15_e51 = tmp___0_e35;
  sg1_e33 = __cil_tmp15_e51;
  sg1_b32 = __cil_tmp15_b50;
  sg1 = __cil_tmp15;
  CHECK_SEQ2SAFE(sg_b28, sg_e29, (void *)(sg + 1), sizeof(int ), sizeof(int ), 1,
                 0);
  CHECK_SEQ2SAFE(sg1_b32, sg1_e33, (void *)(sg1 + 1), sizeof(int ), sizeof(int ),
                 1, 0);
  __retres7 = *(sg + 1) + *(sg1 + 1);
  return (__retres7);
}
}
