#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 r49397 = x;
        float r49398 = r49397 * r49397;
        float r49399 = 2.0f;
        float r49400 = r49397 * r49399;
        float r49401 = y;
        float r49402 = r49400 * r49401;
        float r49403 = r49398 + r49402;
        float r49404 = r49401 * r49401;
        float r49405 = r49403 + r49404;
        return r49405;
}

double f_id(double x, double y) {
        double r49406 = x;
        double r49407 = r49406 * r49406;
        double r49408 = 2.0;
        double r49409 = r49406 * r49408;
        double r49410 = y;
        double r49411 = r49409 * r49410;
        double r49412 = r49407 + r49411;
        double r49413 = r49410 * r49410;
        double r49414 = r49412 + r49413;
        return r49414;
}


double f_of(float x, float y) {
        float r49415 = x;
        float r49416 = r49415 * r49415;
        float r49417 = 2.0f;
        float r49418 = r49415 * r49417;
        float r49419 = y;
        float r49420 = r49418 * r49419;
        float r49421 = r49416 + r49420;
        float r49422 = r49419 * r49419;
        float r49423 = r49421 + r49422;
        return r49423;
}

double f_od(double x, double y) {
        double r49424 = x;
        double r49425 = r49424 * r49424;
        double r49426 = 2.0;
        double r49427 = r49424 * r49426;
        double r49428 = y;
        double r49429 = r49427 * r49428;
        double r49430 = r49425 + r49429;
        double r49431 = r49428 * r49428;
        double r49432 = r49430 + r49431;
        return r49432;
}

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 r49433, r49434, r49435, r49436, r49437, r49438, r49439, r49440, r49441;

void setup_mpfr_f_im() {
        mpfr_set_default_prec(144);
        mpfr_init(r49433);
        mpfr_init(r49434);
        mpfr_init_set_str(r49435, "2.0", 10, MPFR_RNDN);
        mpfr_init(r49436);
        mpfr_init(r49437);
        mpfr_init(r49438);
        mpfr_init(r49439);
        mpfr_init(r49440);
        mpfr_init(r49441);
}

double f_im(double x, double y) {
        mpfr_set_d(r49433, x, MPFR_RNDN);
        mpfr_mul(r49434, r49433, r49433, MPFR_RNDN);
        ;
        mpfr_mul(r49436, r49433, r49435, MPFR_RNDN);
        mpfr_set_d(r49437, y, MPFR_RNDN);
        mpfr_mul(r49438, r49436, r49437, MPFR_RNDN);
        mpfr_add(r49439, r49434, r49438, MPFR_RNDN);
        mpfr_mul(r49440, r49437, r49437, MPFR_RNDN);
        mpfr_add(r49441, r49439, r49440, MPFR_RNDN);
        return mpfr_get_d(r49441, MPFR_RNDN);
}

static mpfr_t r49442, r49443, r49444, r49445, r49446, r49447, r49448, r49449, r49450;

void setup_mpfr_f_fm() {
        mpfr_set_default_prec(144);
        mpfr_init(r49442);
        mpfr_init(r49443);
        mpfr_init_set_str(r49444, "2.0", 10, MPFR_RNDN);
        mpfr_init(r49445);
        mpfr_init(r49446);
        mpfr_init(r49447);
        mpfr_init(r49448);
        mpfr_init(r49449);
        mpfr_init(r49450);
}

double f_fm(double x, double y) {
        mpfr_set_d(r49442, x, MPFR_RNDN);
        mpfr_mul(r49443, r49442, r49442, MPFR_RNDN);
        ;
        mpfr_mul(r49445, r49442, r49444, MPFR_RNDN);
        mpfr_set_d(r49446, y, MPFR_RNDN);
        mpfr_mul(r49447, r49445, r49446, MPFR_RNDN);
        mpfr_add(r49448, r49443, r49447, MPFR_RNDN);
        mpfr_mul(r49449, r49446, r49446, MPFR_RNDN);
        mpfr_add(r49450, r49448, r49449, MPFR_RNDN);
        return mpfr_get_d(r49450, MPFR_RNDN);
}

static mpfr_t r49451, r49452, r49453, r49454, r49455, r49456, r49457, r49458, r49459;

void setup_mpfr_f_dm() {
        mpfr_set_default_prec(144);
        mpfr_init(r49451);
        mpfr_init(r49452);
        mpfr_init_set_str(r49453, "2.0", 10, MPFR_RNDN);
        mpfr_init(r49454);
        mpfr_init(r49455);
        mpfr_init(r49456);
        mpfr_init(r49457);
        mpfr_init(r49458);
        mpfr_init(r49459);
}

double f_dm(double x, double y) {
        mpfr_set_d(r49451, x, MPFR_RNDN);
        mpfr_mul(r49452, r49451, r49451, MPFR_RNDN);
        ;
        mpfr_mul(r49454, r49451, r49453, MPFR_RNDN);
        mpfr_set_d(r49455, y, MPFR_RNDN);
        mpfr_mul(r49456, r49454, r49455, MPFR_RNDN);
        mpfr_add(r49457, r49452, r49456, MPFR_RNDN);
        mpfr_mul(r49458, r49455, r49455, MPFR_RNDN);
        mpfr_add(r49459, r49457, r49458, MPFR_RNDN);
        return mpfr_get_d(r49459, MPFR_RNDN);
}