Random Jason Timeout Test 003

Average Error: 0.1 → 0.1

Time: 2.5s

Precision: 64

• could not determine a ground truth for program body

  1. a = 5.683788269687683e+223
  2. b = 6.200392985854844e-204

Math

\[\sin \left({\left(\sqrt{\tan^{-1}_* \frac{b}{b}}\right)}^{\left(b - a\right)}\right)\]

↓

\[\sin \left({\left(\tan^{-1}_* \frac{b}{b}\right)}^{\left(\frac{1}{2} \cdot \left(b - a\right)\right)}\right)\]

C

double f(double a, double b) {
        double r13148 = b;
        double r13149 = atan2(r13148, r13148);
        double r13150 = sqrt(r13149);
        double r13151 = a;
        double r13152 = r13148 - r13151;
        double r13153 = pow(r13150, r13152);
        double r13154 = sin(r13153);
        return r13154;
}

↓

double f(double a, double b) {
        double r13155 = b;
        double r13156 = atan2(r13155, r13155);
        double r13157 = 0.5;
        double r13158 = a;
        double r13159 = r13155 - r13158;
        double r13160 = r13157 * r13159;
        double r13161 = pow(r13156, r13160);
        double r13162 = sin(r13161);
        return r13162;
}

Error

Bits error versus a

Bits error versus b

Derivation

1. Initial program 0.1

   \[\sin \left({\left(\sqrt{\tan^{-1}_* \frac{b}{b}}\right)}^{\left(b - a\right)}\right)\]
2. Using strategy rm

3. Applied pow1/2 0.1

   \[\leadsto \sin \left({\color{blue}{\left({\left(\tan^{-1}_* \frac{b}{b}\right)}^{\frac{1}{2}}\right)}}^{\left(b - a\right)}\right)\]

4. Applied pow-pow 0.1

   \[\leadsto \sin \color{blue}{\left({\left(\tan^{-1}_* \frac{b}{b}\right)}^{\left(\frac{1}{2} \cdot \left(b - a\right)\right)}\right)}\]

5. Final simplification 0.1

   \[\leadsto \sin \left({\left(\tan^{-1}_* \frac{b}{b}\right)}^{\left(\frac{1}{2} \cdot \left(b - a\right)\right)}\right)\]

Reproduce

herbie shell --seed 2020065 +o rules:numerics
(FPCore (a b)
  :name "Random Jason Timeout Test 003"
  :precision binary64
  (sin (pow (sqrt (atan2 b b)) (- b a))))