Incorrect benchmark: ell/ellpi/Eq

[FrNecas]

The benchmark ell/ellpi/Eq is marked as semantically equal, however, it clearly isn't. The gist of the change is simplification of an arithmetic expression using mathematical laws -- simplifying (A + B) * (A - B) to A^2 - B^2, however it's changed to A^2 + B^2 instead. Try adding the following main to the programs:

int main(void) {
    printf("%f\n", snippet(30.0, 1, 2.0));
    return 0;
}

The old version produces:

invalid arguments in rf
invalid arguments in rj
-nan

The new version produces:

-0.729108

which clearly showcases inequality. I believe that the change in newV.c should be to q=1.0-((s*ak)*(s*ak)) instead of q=1.0+((s*ak)*(s*ak)). One thing that I am not completely sure about is whether this makes it really semantically equal. Due to the change of order of operations, it is possible that there the floating points are rounded differently (floating point arithmetic is not distributive). On the other hand, there are checks for invalid arguments which exclude large and small numbers so perhaps this prevents rounding differences from occurring but I am not sure how to effectively verify this. I am going to open a PR with the change for now but feel free to suggest a different fix and/or continue the discussion regarding rounding of floating points.

[shrBadihi]

That is correct and it should be q=1.0-((sak)(s*ak)). Regarding being equivalent, I've checked with SMT solver and the two programs are equivalent. As you said for proving the equivalent with the tools we might need to bound the accepted values.