max.test.c

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

#include <stdio.h>
#include "klee/klee.h"
/* compiler builtin: 
   void __builtin_va_copy(__builtin_va_list  , __builtin_va_list  ) ;  */
/* compiler builtin: 
   void *__builtin_frob_return_address(void * ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __sync_and_and_fetch(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __sync_fetch_and_or(...) ;  */
/* compiler builtin: 
   int __builtin_popcountll(unsigned long long  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_or_fetch(...) ;  */
/* compiler builtin: 
   float __builtin_atanf(float  ) ;  */
/* 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___sprintf_chk(char * , int  , unsigned long  , char const   *  , ...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_nand_fetch_8(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_and(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_xor_fetch_16(...) ;  */
/* compiler builtin: 
   double __builtin_cosh(double  ) ;  */
/* compiler builtin: 
   float __builtin_tanhf(float  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_nand_16(...) ;  */
/* compiler builtin: 
   void *__builtin_mempcpy(void * , void const   * , unsigned long  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_sub_fetch_1(...) ;  */
/* compiler builtin: 
   long double __builtin_sqrtl(long double  ) ;  */
/* compiler builtin: 
   int __builtin_parity(unsigned int  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_or(...) ;  */
/* compiler builtin: 
   long double __builtin_coshl(long double  ) ;  */
/* compiler builtin: 
   long double __builtin_cosl(long double  ) ;  */
/* compiler builtin: 
   float __builtin_cosf(float  ) ;  */
/* compiler builtin: 
   void __sync_synchronize(...) ;  */
/* compiler builtin: 
   long double __builtin_acosl(long double  ) ;  */
/* compiler builtin: 
   void *__builtin___mempcpy_chk(void * , void const   * , unsigned long  , unsigned long  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __sync_or_and_fetch(...) ;  */
/* compiler builtin: 
   int __builtin_clz(unsigned int  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_nand_fetch_4(...) ;  */
/* compiler builtin: 
   double __builtin_log10(double  ) ;  */
/* compiler builtin: 
   char *__builtin___strcat_chk(char * , char const   * , unsigned long  ) ;  */
/* compiler builtin: 
   float __builtin_modff(float  , float * ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_sub_fetch_4(...) ;  */
/* compiler builtin: 
   _Bool __atomic_compare_exchange_n(...) ;  */
/* 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: 
   void __atomic_signal_fence(int  ) ;  */
/* compiler builtin: 
   double __builtin_fabs(double  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_nand_1(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_and_fetch_16(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __sync_fetch_and_nand(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_xor_fetch_8(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_xor_fetch_2(...) ;  */
/* compiler builtin: 
   void __atomic_thread_fence(int  ) ;  */
/* compiler builtin: 
   void __atomic_store_16(...) ;  */
/* compiler builtin: 
   void __builtin_va_start(__builtin_va_list  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_and_8(...) ;  */
/* compiler builtin: 
   short __builtin_bswap16(short  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_and_fetch_2(...) ;  */
/* compiler builtin: 
   _Bool __atomic_test_and_set(void * , int  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_add_8(...) ;  */
/* compiler builtin: 
   int __builtin_ctz(unsigned int  ) ;  */
/* 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: 
   void __attribute__((__overloaded__))  __atomic_fetch_nand(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_exchange_16(...) ;  */
/* compiler builtin: 
   void __atomic_clear(_Bool * , int  ) ;  */
/* compiler builtin: 
   void __atomic_store(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_add_fetch_2(...) ;  */
/* compiler builtin: 
   float __builtin_log10f(float  ) ;  */
/* compiler builtin: 
   long double __builtin_fabsl(long double  ) ;  */
/* compiler builtin: 
   long double __builtin_floorl(long double  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_xor_1(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_and_fetch(...) ;  */
/* compiler builtin: 
   float __builtin_floorf(float  ) ;  */
/* compiler builtin: 
   _Bool __atomic_compare_exchange_4(...) ;  */
/* compiler builtin: 
   void *__builtin_memcpy(void * , void const   * , unsigned long  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __sync_sub_and_fetch(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __sync_nand_and_fetch(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_load_16(...) ;  */
/* compiler builtin: 
   float __attribute__((____vector_size____(16)))  __builtin_ia32_subps(float __attribute__((____vector_size____(16)))   ,
                                                                        float __attribute__((____vector_size____(16)))   ) ;  */
/* 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: 
   _Bool __atomic_always_lock_free(unsigned long  , void * ) ;  */
/* compiler builtin: 
   int __builtin_strncmp(char const   * , char const   * , unsigned long  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_nand_fetch_16(...) ;  */
/* 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: 
   float __builtin_sqrtf(float  ) ;  */
/* compiler builtin: 
   double __builtin_nans(char const   * ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_xor_8(...) ;  */
/* compiler builtin: 
   double __builtin_exp(double  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_exchange_8(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_exchange_1(...) ;  */
/* compiler builtin: 
   int __builtin_strcmp(char const   * , char const   * ) ;  */
/* compiler builtin: 
   float __builtin_ldexpf(float  , int  ) ;  */
/* compiler builtin: 
   float __builtin_powif(float  , int  ) ;  */
/* 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: 
   void __atomic_feraiseexcept(int  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_and_fetch_4(...) ;  */
/* compiler builtin: 
   float __builtin_fabsf(float  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_or_fetch_8(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_or_fetch_4(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_or_fetch_1(...) ;  */
/* compiler builtin: 
   unsigned long __builtin_object_size(void * , int  ) ;  */
/* compiler builtin: 
   void *__builtin_alloca(unsigned long  ) ;  */
/* compiler builtin: 
   int __builtin_va_arg_pack_len(void) ;  */
/* compiler builtin: 
   long double __builtin_tanl(long double  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_and_2(...) ;  */
/* compiler builtin: 
   void __sync_lock_release(...) ;  */
/* compiler builtin: 
   long double __builtin_modfl(long double  , long double * ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_nand_8(...) ;  */
/* 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: 
   void __attribute__((__overloaded__))  __atomic_fetch_add(...) ;  */
/* compiler builtin: 
   long __builtin_bswap64(long  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_nand_fetch_1(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_nand_2(...) ;  */
/* 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 __attribute__((__overloaded__))  __atomic_load_n(...) ;  */
/* compiler builtin: 
   double __builtin_huge_val(void) ;  */
/* compiler builtin: 
   int __builtin_clzl(unsigned long  ) ;  */
/* compiler builtin: 
   _Bool __atomic_compare_exchange_16(...) ;  */
/* compiler builtin: 
   float __builtin_frexpf(float  , int * ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_exchange_n(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_or_1(...) ;  */
/* 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__))  __atomic_fetch_or_8(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_add_1(...) ;  */
/* compiler builtin: 
   void __builtin_return(void const   * ) ;  */
/* compiler builtin: 
   long double __builtin_asinl(long double  ) ;  */
/* compiler builtin: 
   int __builtin_ffsll(unsigned long long  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_sub_1(...) ;  */
/* compiler builtin: 
   int __builtin_va_arg_pack(void) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_or_4(...) ;  */
/* compiler builtin: 
   char *__builtin___strncpy_chk(char * , char const   * , unsigned long  , unsigned long  ) ;  */
/* compiler builtin: 
   double __builtin_powi(double  , int  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_load_2(...) ;  */
/* compiler builtin: 
   char *__builtin_strchr(char * , int  ) ;  */
/* compiler builtin: 
   char *__builtin___strncat_chk(char * , char const   * , unsigned long  , unsigned long  ) ;  */
/* compiler builtin: 
   void __atomic_store_2(...) ;  */
/* 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: 
   void __builtin_stdarg_start(__builtin_va_list  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_exchange_4(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __sync_fetch_and_xor(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_sub_4(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_and_4(...) ;  */
/* compiler builtin: 
   long double __builtin_frexpl(long double  , int * ) ;  */
/* compiler builtin: 
   _Bool __atomic_compare_exchange(...) ;  */
/* compiler builtin: 
   float __builtin_tanf(float  ) ;  */
/* compiler builtin: 
   long double __builtin_logl(long double  ) ;  */
/* compiler builtin: 
   void __builtin_va_arg(__builtin_va_list  , unsigned long  , void * ) ;  */
/* compiler builtin: 
   long __builtin_expect(long  , long  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_load_1(...) ;  */
/* compiler builtin: 
   _Bool __atomic_compare_exchange_1(...) ;  */
/* compiler builtin: 
   int __builtin___printf_chk(int  , char const   *  , ...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_xor_2(...) ;  */
/* compiler builtin: 
   int __builtin___vfprintf_chk(void * , int  , char const   * , __builtin_va_list  ) ;  */
/* compiler builtin: 
   void __builtin_prefetch(void const   *  , ...) ;  */
/* compiler builtin: 
   long double __builtin_nansl(char const   * ) ;  */
/* compiler builtin: 
   double __builtin_fmod(double  ) ;  */
/* compiler builtin: 
   void __atomic_load(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_or_fetch_16(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_add_fetch_16(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __sync_val_compare_and_swap(...) ;  */
/* compiler builtin: 
   void __atomic_store_4(...) ;  */
/* compiler builtin: 
   double __builtin_tanh(double  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_and_1(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_nand_4(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_add_16(...) ;  */
/* compiler builtin: 
   void __builtin_unreachable(void) ;  */
/* compiler builtin: 
   _Bool __atomic_compare_exchange_2(...) ;  */
/* compiler builtin: 
   long double __builtin_ldexpl(long double  , int  ) ;  */
/* compiler builtin: 
   void *__builtin_apply(void (*)() , void * , unsigned long  ) ;  */
/* compiler builtin: 
   float __builtin_sinf(float  ) ;  */
/* compiler builtin: 
   double __builtin_ceil(double  ) ;  */
/* compiler builtin: 
   void __atomic_exchange(...) ;  */
/* compiler builtin: 
   long double __builtin_powil(long double  , int  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_sub_fetch_8(...) ;  */
/* compiler builtin: 
   long double __builtin_expl(long double  ) ;  */
/* compiler builtin: 
   int __builtin_constant_p(int  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_sub_16(...) ;  */
/* 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: 
   long double __builtin_atan2l(long double  , long double  ) ;  */
/* compiler builtin: 
   void *__builtin_apply_args(void) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_exchange_2(...) ;  */
/* compiler builtin: 
   float __builtin_logf(float  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_sub_fetch_2(...) ;  */
/* compiler builtin: 
   unsigned long __builtin_strlen(char const   * ) ;  */
/* compiler builtin: 
   int __builtin_ffs(unsigned int  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_xor_16(...) ;  */
/* compiler builtin: 
   double __builtin_inf(void) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_or_16(...) ;  */
/* compiler builtin: 
   void *__builtin___memcpy_chk(void * , void const   * , unsigned long  , unsigned long  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_load_4(...) ;  */
/* compiler builtin: 
   void __atomic_store_n(...) ;  */
/* compiler builtin: 
   void __builtin_trap(void) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_add_4(...) ;  */
/* compiler builtin: 
   int __builtin_parityl(unsigned long  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_nand_fetch_2(...) ;  */
/* 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: 
   void __attribute__((__overloaded__))  __atomic_sub_fetch(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_and_16(...) ;  */
/* compiler builtin: 
   _Bool __atomic_compare_exchange_8(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_nand_fetch(...) ;  */
/* compiler builtin: 
   double __builtin_nan(char const   * ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_load_8(...) ;  */
/* compiler builtin: 
   int __builtin___snprintf_chk(char * , unsigned long  , int  , unsigned long  ,
                                char const   *  , ...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_xor_fetch_4(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_sub_2(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_add_fetch(...) ;  */
/* compiler builtin: 
   long double __builtin_atanl(long 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 __atomic_store_8(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_xor_fetch(...) ;  */
/* 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: 
   void __attribute__((__overloaded__))  __atomic_or_fetch_2(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_add_fetch_1(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_xor(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_add_fetch_8(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_xor_4(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_sub_8(...) ;  */
/* compiler builtin: 
   _Bool __sync_bool_compare_and_swap(...) ;  */
/* compiler builtin: 
   double __builtin_atan2(double  , double  ) ;  */
/* compiler builtin: 
   int __builtin_popcountl(unsigned long  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_and_fetch_1(...) ;  */
/* compiler builtin: 
   long double __builtin_ceill(long double  ) ;  */
/* compiler builtin: 
   void __atomic_store_1(...) ;  */
/* compiler builtin: 
   char *__builtin___strcpy_chk(char * , char const   * , unsigned long  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_xor_fetch_1(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_or_2(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_sub_fetch_16(...) ;  */
/* compiler builtin: 
   double __builtin_floor(double  ) ;  */
/* compiler builtin: 
   double __builtin_cos(double  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __sync_fetch_and_sub(...) ;  */
/* compiler builtin: 
   void *__builtin_memset(void * , int  , int  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_add_2(...) ;  */
/* compiler builtin: 
   long double __builtin_nanl(char const   * ) ;  */
/* compiler builtin: 
   float __builtin_atan2f(float  , float  ) ;  */
/* compiler builtin: 
   _Bool __atomic_is_lock_free(unsigned long  , void * ) ;  */
/* compiler builtin: 
   int __builtin_popcount(unsigned int  ) ;  */
/* compiler builtin: 
   double __builtin_sinh(double  ) ;  */
/* compiler builtin: 
   void __builtin_bcopy(void const   * , void * , unsigned long  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_and_fetch_8(...) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_fetch_sub(...) ;  */
/* compiler builtin: 
   void *__builtin_extract_return_addr(void * ) ;  */
/* compiler builtin: 
   int __builtin_bswap32(int  ) ;  */
/* compiler builtin: 
   double __builtin_ldexp(double  , int  ) ;  */
/* compiler builtin: 
   long double __builtin_infl(void) ;  */
/* compiler builtin: 
   float __builtin_fmodf(float  ) ;  */
/* compiler builtin: 
   void __attribute__((__overloaded__))  __atomic_add_fetch_4(...) ;  */
/* compiler builtin: 
   void *__builtin_frame_address(unsigned int  ) ;  */
int buggyQ(int x , int y , int z ) 
{ 


  {
  if (x > y) {
    if (y > z) {
      return (x);
    } else
    if (x > z) {
      return (x);
    } else {
      return (z);
    }
  } else
  if (x > z) {
    return (y);
  } else
  if (y > z) {
    return (y);
  } else {
    return (y);
  }
}
}
int correctQ(int x , int y , int z ) 
{ 


  {
  if (x > y) {
    if (y > z) {
      return (x);
    } else
    if (x > z) {
      return (x);
    } else {
      return (z);
    }
  } else
  if (x > z) {
    return (y);
  } else
  if (y > z) {
    return (y);
  } else {
    return (z);
  }
}
}
extern int ( /* missing proto */  printf)() ;
int mainQ(int x , int y , int z ) 
{ 
  int rb ;
  int tmp ;
  int rc ;
  int tmp___0 ;
  int x_new ;
  int y_new ;
  int z_new ;

  {
  rb = buggyQ(x, y, z);
  rc = correctQ(x, y, z);
  if (rb != rc) {
    x_new = (0 * x + 0 * y) + (1 * z + 0);
    y_new = (0 * x + 0 * y) + (0 * z + -131);
    z_new = (0 * x + 3 * y) + (-4 * z + -10);
    if (rb != rc) {
      printf("FAIL with inputs: x %d y %d z %d \n", x, y, z);
    }
  }
  return(0);
}
}
extern int ( /* missing proto */  klee_make_symbolic)() ;
extern int ( /* missing proto */  klee_assume)() ;
int main(void) 
{ 
  int uk_0 ;
  int uk_1 ;
  int uk_2 ;
  int rv ;
  int tmp ;

  {
  klee_make_symbolic(& uk_0, sizeof(uk_0), "uk_0");
  klee_assume(-100 <= uk_0);
  klee_assume(uk_0 <= 100);
  klee_make_symbolic(& uk_1, sizeof(uk_1), "uk_1");
  klee_assume(-100 <= uk_1);
  klee_assume(uk_1 <= 100);
  klee_make_symbolic(& uk_2, sizeof(uk_2), "uk_2");
  klee_assume(-100 <= uk_2);
  klee_assume(uk_2 <= 100);
  tmp = mainQ(uk_0, uk_1, uk_2);
  rv = tmp;
  return (0);
}
}