// This file is part of the SV-Benchmarks collection of verification tasks:
// https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks
//
// SPDX-FileCopyrightText: 2001-2016 Daniel Kroening, Computer Science Department, University of Oxford
// SPDX-FileCopyrightText: 2001-2016 Edmund Clarke, Computer Science Department, Carnegie Mellon University
// SPDX-FileCopyrightText: 2012 FBK-ES <https://es.fbk.eu/>
// SPDX-FileCopyrightText: 2012-2021 The SV-Benchmarks Community
//
// SPDX-License-Identifier: Apache-2.0
// SPDX-License-Identifier: LicenseRef-BSD-4-Clause-Attribution-Kroening-Clarke

extern unsigned int __VERIFIER_nondet_uint();
extern char __VERIFIER_nondet_char();
extern int __VERIFIER_nondet_int();
extern long __VERIFIER_nondet_long();
extern unsigned long __VERIFIER_nondet_ulong();
extern float __VERIFIER_nondet_float();
extern void exit(int);

extern void abort(void);

extern void __assert_fail (const char *__assertion, const char *__file,
      unsigned int __line, const char *__function)
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
extern void __assert_perror_fail (int __errnum, const char *__file,
      unsigned int __line, const char *__function)
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
extern void __assert (const char *__assertion, const char *__file, int __line)
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));

void reach_error() { ((void) sizeof ((0) ? 1 : 0), __extension__ ({ if (0) ; else __assert_fail ("0", "square_3.c", 7, __extension__ __PRETTY_FUNCTION__); })); }
extern void abort(void);
void assume_abort_if_not(int cond) {
  if(!cond) {abort();}
}
extern float __VERIFIER_nondet_float(void);
int main1()
{
  float IN = __VERIFIER_nondet_float();
  assume_abort_if_not(IN >= 0.0f && IN < 1.0f);

  float x = IN;

  float result =
    1.0f + 0.5f*x - 0.125f*x*x + 0.0625f*x*x*x - 0.0390625f*x*x*x*x;

  if(!(result >= 0.0f && result < 1.39843f))
    {reach_error();}

  return 0;
}

extern void abort(void);
extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));

extern char __VERIFIER_nondet_char(void);
extern unsigned int __VERIFIER_nondet_uint(void);
void __VERIFIER_assert(int cond) {
  if (!(cond)) {
    ERROR: {reach_error();abort();}
  }
  return;
}
/* Generated by CIL v. 1.3.7 */
/* print_CIL_Input is true */

unsigned int base2flt(unsigned int m , int e ) 
{ unsigned int res ;
  unsigned int __retres4 ;

  {
  if (! m) {
    __retres4 = 0U;
    goto return_label;
  } else {

  }
  if (m < 1U << 24U) {
    {
    while (1) {
      while_0_continue: /* CIL Label */ ;
      if (e <= -128) {
        __retres4 = 0U;
        goto return_label;
      } else {

      }
      e = e - 1;
      m = m << 1U;
      if (m < 1U << 24U) {

      } else {
        goto while_0_break;
      }
    }
    while_0_break: /* CIL Label */ ;
    }
  } else {
    {
    while (1) {
      while_1_continue: /* CIL Label */ ;
      if (m >= 1U << 25U) {

      } else {
        goto while_1_break;
      }
      if (e >= 127) {
        __retres4 = 4294967295U;
        goto return_label;
      } else {

      }
      e = e + 1;
      m = m >> 1U;
    }
    while_1_break: /* CIL Label */ ;
    }
  }
  m = m & ~ (1U << 24U);
  res = m | ((unsigned int )(e + 128) << 24U);
  __retres4 = res;
  return_label: /* CIL Label */ 
  return (__retres4);
}
}
unsigned int addflt(unsigned int a , unsigned int b ) 
{ unsigned int res ;
  unsigned int ma ;
  unsigned int mb ;
  unsigned int delta ;
  int ea ;
  int eb ;
  unsigned int tmp ;
  unsigned int __retres10 ;

  {
  if (a < b) {
    tmp = a;
    a = b;
    b = tmp;
  } else {

  }
  if (! b) {
    __retres10 = a;
    goto return_label;
  } else {

  }
  {
  ma = a & ((1U << 24U) - 1U);
  ea = (int )(a >> 24U) - 128;
  ma = ma | (1U << 24U);
  mb = b & ((1U << 24U) - 1U);
  eb = (int )(b >> 24U) - 128;
  mb = mb | (1U << 24U);
  __VERIFIER_assert(ea >= eb);
  delta = ea - eb;
  mb = mb >> delta;
  }
  if (! mb) {
    __retres10 = a;
    goto return_label;
  } else {

  }
  ma = ma + mb;
  if (ma & (1U << 25U)) {
    if (ea == 127) {
      __retres10 = 4294967295U;
      goto return_label;
    } else {

    }
    ea = ea + 1;
    ma = ma >> 1U;
  } else {

  }
  {
  __VERIFIER_assert(ma < 1U << 25U);
  ma = ma & ((1U << 24U) - 1U);
  res = ma | (unsigned int )((ea + 128) << 24U);
  }
  __retres10 = res;
  return_label: /* CIL Label */ 
  return (__retres10);
}
}
unsigned int mulflt(unsigned int a , unsigned int b ) 
{ unsigned int res ;
  unsigned int ma ;
  unsigned int mb ;
  unsigned long long accu ;
  int ea ;
  int eb ;
  unsigned int tmp ;
  unsigned int __retres10 ;

  {
  if (a < b) {
    tmp = a;
    a = b;
    b = tmp;
  } else {

  }
  if (! b) {
    __retres10 = 0U;
    goto return_label;
  } else {

  }
  ma = a & ((1U << 24U) - 1U);
  ea = (int )(a >> 24U) - 128;
  ma = ma | (1U << 24U);
  mb = b & ((1U << 24U) - 1U);
  eb = (int )(b >> 24U) - 128;
  mb = mb | (1U << 24U);
  ea = ea + eb;
  ea = ea + 24;
  if (ea > 127) {
    __retres10 = 4294967295U;
    goto return_label;
  } else {

  }
  if (ea < -128) {
    __retres10 = 0U;
    goto return_label;
  } else {

  }
  accu = ma;
  accu = accu * (unsigned long long )mb;
  accu = accu >> 24U;
  if (accu >= (unsigned long long )(1U << 25U)) {
    if (ea == 127) {
      __retres10 = 4294967295U;
      goto return_label;
    } else {

    }
    ea = ea + 1;
    accu = accu >> 1U;
    if (accu >= (unsigned long long )(1U << 25U)) {
      __retres10 = 4294967295U;
      goto return_label;
    } else {

    }
  } else {

  }
  ma = accu;
  ma = ma & ~ (1U << 24U);
  res = ma | ((unsigned int )(ea + 128) << 24U);
  __retres10 = res;
  return_label: /* CIL Label */ 
  return (__retres10);
}
}
int main2(void) 
{ unsigned int a ;
  unsigned int ma  = __VERIFIER_nondet_uint();
  signed char ea  = __VERIFIER_nondet_char();
  unsigned int b ;
  unsigned int mb  = __VERIFIER_nondet_uint();
  signed char eb  = __VERIFIER_nondet_char();
  unsigned int r_mul ;
  unsigned int zero ;
  unsigned int one ;
  int sb ;
  int tmp ;
  int tmp___0 ;
  int tmp___1 ;
  int __retres16 ;

  {
  {
  zero = base2flt(0, 0);
  one = base2flt(1, 0);
  a = base2flt(ma, ea);
  b = base2flt(mb, eb);
  r_mul = mulflt(a, b);
  }
  if (b < one) {
    sb = -1;
  } else {
    if (b > one) {
      tmp = 1;
    } else {
      tmp = 0;
    }
    sb = tmp;
  }
  if (sb == 0) {
    if (r_mul < a) {
      tmp___1 = -1;
    } else {
      if (r_mul > a) {
        tmp___0 = 1;
      } else {
        tmp___0 = 0;
      }
      tmp___1 = tmp___0;
    }
    {
    __VERIFIER_assert(tmp___1 == 0);
    }
  } else {

  }
  __retres16 = 0;
  return (__retres16);
}
}
int main()
{
  if(__VERIFIER_nondet_int())
    main1();
  else
    main2();
}