#include <tgmath.h>
#include <gmp.h>
#include <mpfr.h>
#include <stdio.h>
#include <stdbool.h>

char *name = "Examples.Basics.ProofTests:f4 from sbv-4.4";

double f_if(float x, float y) {
        float r51777 = x;
        float r51778 = r51777 * r51777;
        float r51779 = 2.0;
        float r51780 = r51777 * r51779;
        float r51781 = y;
        float r51782 = r51780 * r51781;
        float r51783 = r51778 + r51782;
        float r51784 = r51781 * r51781;
        float r51785 = r51783 + r51784;
        return r51785;
}

double f_id(double x, double y) {
        double r51786 = x;
        double r51787 = r51786 * r51786;
        double r51788 = 2.0;
        double r51789 = r51786 * r51788;
        double r51790 = y;
        double r51791 = r51789 * r51790;
        double r51792 = r51787 + r51791;
        double r51793 = r51790 * r51790;
        double r51794 = r51792 + r51793;
        return r51794;
}


double f_of(float x, float y) {
        float r51795 = x;
        float r51796 = r51795 * r51795;
        float r51797 = 2.0;
        float r51798 = r51795 * r51797;
        float r51799 = y;
        float r51800 = r51798 * r51799;
        float r51801 = r51796 + r51800;
        float r51802 = r51799 * r51799;
        float r51803 = r51801 + r51802;
        return r51803;
}

double f_od(double x, double y) {
        double r51804 = x;
        double r51805 = r51804 * r51804;
        double r51806 = 2.0;
        double r51807 = r51804 * r51806;
        double r51808 = y;
        double r51809 = r51807 * r51808;
        double r51810 = r51805 + r51809;
        double r51811 = r51808 * r51808;
        double r51812 = r51810 + r51811;
        return r51812;
}

void mpfr_fmod2(mpfr_t r, mpfr_t n, mpfr_t d, mpfr_rnd_t rmd) {
        mpfr_fmod(r, n, d, rmd);
        if (mpfr_cmp_ui(r, 0) < 0) mpfr_add(r, r, d, rmd);
}


static mpfr_t r51813, r51814, r51815, r51816, r51817, r51818, r51819, r51820, r51821;

void setup_mpfr_f_im() {
        mpfr_set_default_prec(400);
        mpfr_init(r51813);
        mpfr_init(r51814);
        mpfr_init_set_str(r51815, "2.0", 10, MPFR_RNDN);
        mpfr_init(r51816);
        mpfr_init(r51817);
        mpfr_init(r51818);
        mpfr_init(r51819);
        mpfr_init(r51820);
        mpfr_init(r51821);
}

double f_im(double x, double y) {
        mpfr_set_d(r51813, x, MPFR_RNDN);
        mpfr_mul(r51814, r51813, r51813, MPFR_RNDN);
        ;
        mpfr_mul(r51816, r51813, r51815, MPFR_RNDN);
        mpfr_set_d(r51817, y, MPFR_RNDN);
        mpfr_mul(r51818, r51816, r51817, MPFR_RNDN);
        mpfr_add(r51819, r51814, r51818, MPFR_RNDN);
        mpfr_mul(r51820, r51817, r51817, MPFR_RNDN);
        mpfr_add(r51821, r51819, r51820, MPFR_RNDN);
        return mpfr_get_d(r51821, MPFR_RNDN);
}

static mpfr_t r51822, r51823, r51824, r51825, r51826, r51827, r51828, r51829, r51830;

void setup_mpfr_f_fm() {
        mpfr_set_default_prec(400);
        mpfr_init(r51822);
        mpfr_init(r51823);
        mpfr_init_set_str(r51824, "2.0", 10, MPFR_RNDN);
        mpfr_init(r51825);
        mpfr_init(r51826);
        mpfr_init(r51827);
        mpfr_init(r51828);
        mpfr_init(r51829);
        mpfr_init(r51830);
}

double f_fm(double x, double y) {
        mpfr_set_d(r51822, x, MPFR_RNDN);
        mpfr_mul(r51823, r51822, r51822, MPFR_RNDN);
        ;
        mpfr_mul(r51825, r51822, r51824, MPFR_RNDN);
        mpfr_set_d(r51826, y, MPFR_RNDN);
        mpfr_mul(r51827, r51825, r51826, MPFR_RNDN);
        mpfr_add(r51828, r51823, r51827, MPFR_RNDN);
        mpfr_mul(r51829, r51826, r51826, MPFR_RNDN);
        mpfr_add(r51830, r51828, r51829, MPFR_RNDN);
        return mpfr_get_d(r51830, MPFR_RNDN);
}

static mpfr_t r51831, r51832, r51833, r51834, r51835, r51836, r51837, r51838, r51839;

void setup_mpfr_f_dm() {
        mpfr_set_default_prec(400);
        mpfr_init(r51831);
        mpfr_init(r51832);
        mpfr_init_set_str(r51833, "2.0", 10, MPFR_RNDN);
        mpfr_init(r51834);
        mpfr_init(r51835);
        mpfr_init(r51836);
        mpfr_init(r51837);
        mpfr_init(r51838);
        mpfr_init(r51839);
}

double f_dm(double x, double y) {
        mpfr_set_d(r51831, x, MPFR_RNDN);
        mpfr_mul(r51832, r51831, r51831, MPFR_RNDN);
        ;
        mpfr_mul(r51834, r51831, r51833, MPFR_RNDN);
        mpfr_set_d(r51835, y, MPFR_RNDN);
        mpfr_mul(r51836, r51834, r51835, MPFR_RNDN);
        mpfr_add(r51837, r51832, r51836, MPFR_RNDN);
        mpfr_mul(r51838, r51835, r51835, MPFR_RNDN);
        mpfr_add(r51839, r51837, r51838, MPFR_RNDN);
        return mpfr_get_d(r51839, MPFR_RNDN);
}