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

char *name = "Examples.Basics.BasicTests:f1 from sbv-4.4";

double f_if(float x, float y) {
        float r51256 = x;
        float r51257 = y;
        float r51258 = r51256 + r51257;
        float r51259 = r51256 - r51257;
        float r51260 = r51258 * r51259;
        return r51260;
}

double f_id(double x, double y) {
        double r51261 = x;
        double r51262 = y;
        double r51263 = r51261 + r51262;
        double r51264 = r51261 - r51262;
        double r51265 = r51263 * r51264;
        return r51265;
}


double f_of(float x, float y) {
        float r51266 = x;
        float r51267 = y;
        float r51268 = r51266 + r51267;
        float r51269 = r51266 - r51267;
        float r51270 = r51268 * r51269;
        return r51270;
}

double f_od(double x, double y) {
        double r51271 = x;
        double r51272 = y;
        double r51273 = r51271 + r51272;
        double r51274 = r51271 - r51272;
        double r51275 = r51273 * r51274;
        return r51275;
}

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 r51276, r51277, r51278, r51279, r51280;

void setup_mpfr_f_im() {
        mpfr_set_default_prec(400);
        mpfr_init(r51276);
        mpfr_init(r51277);
        mpfr_init(r51278);
        mpfr_init(r51279);
        mpfr_init(r51280);
}

double f_im(double x, double y) {
        mpfr_set_d(r51276, x, MPFR_RNDN);
        mpfr_set_d(r51277, y, MPFR_RNDN);
        mpfr_add(r51278, r51276, r51277, MPFR_RNDN);
        mpfr_sub(r51279, r51276, r51277, MPFR_RNDN);
        mpfr_mul(r51280, r51278, r51279, MPFR_RNDN);
        return mpfr_get_d(r51280, MPFR_RNDN);
}

static mpfr_t r51281, r51282, r51283, r51284, r51285;

void setup_mpfr_f_fm() {
        mpfr_set_default_prec(400);
        mpfr_init(r51281);
        mpfr_init(r51282);
        mpfr_init(r51283);
        mpfr_init(r51284);
        mpfr_init(r51285);
}

double f_fm(double x, double y) {
        mpfr_set_d(r51281, x, MPFR_RNDN);
        mpfr_set_d(r51282, y, MPFR_RNDN);
        mpfr_add(r51283, r51281, r51282, MPFR_RNDN);
        mpfr_sub(r51284, r51281, r51282, MPFR_RNDN);
        mpfr_mul(r51285, r51283, r51284, MPFR_RNDN);
        return mpfr_get_d(r51285, MPFR_RNDN);
}

static mpfr_t r51286, r51287, r51288, r51289, r51290;

void setup_mpfr_f_dm() {
        mpfr_set_default_prec(400);
        mpfr_init(r51286);
        mpfr_init(r51287);
        mpfr_init(r51288);
        mpfr_init(r51289);
        mpfr_init(r51290);
}

double f_dm(double x, double y) {
        mpfr_set_d(r51286, x, MPFR_RNDN);
        mpfr_set_d(r51287, y, MPFR_RNDN);
        mpfr_add(r51288, r51286, r51287, MPFR_RNDN);
        mpfr_sub(r51289, r51286, r51287, MPFR_RNDN);
        mpfr_mul(r51290, r51288, r51289, MPFR_RNDN);
        return mpfr_get_d(r51290, MPFR_RNDN);
}