Herbie run
| Date: | Thursday, May 29th, 2025 |
|---|---|
| Commit: | 3faf5b03 on fighting-unsoundness |
| Seed: | 2025149 |
| Parameters: | 256 points for 4 iterations |
| Flags: | reduce:regimesreduce:binary-searchreduce:branch-expressionssetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:proofs default |
| Memory: | 318 121.0 MB |
Time bar (total: 4.2min)
| 40.1s | 433 853× | 0 | valid |
| 7.6s | 26 352× | 1 | valid |
| 4.4s | 9 425× | 2 | valid |
| 1.1s | 4 553× | 0 | invalid |
| 739.0ms | 8 287× | 0 | exit |
| 345.0ms | 971× | 3 | valid |
ival-mult!: 10.6s (29.4% of total)ival-add!: 3.8s (10.5% of total)ival-exp: 3.1s (8.5% of total)ival-hypot: 3.0s (8.2% of total)ival-log: 2.7s (7.5% of total)ival-div!: 2.7s (7.5% of total)adjust: 1.8s (4.9% of total)ival-asin: 1.5s (4% of total)ival-sin: 1.3s (3.5% of total)ival-sub!: 1.2s (3.4% of total)ival-atan2: 1.0s (2.8% of total)ival-cos: 944.0ms (2.6% of total)ival-sqrt: 581.0ms (1.6% of total)ival-pow: 430.0ms (1.2% of total)ival-sinu: 296.0ms (0.8% of total)ival-asinh: 273.0ms (0.8% of total)ival-neg: 252.0ms (0.7% of total)ival-fabs: 225.0ms (0.6% of total)ival-acosh: 199.0ms (0.6% of total)ival-atanh: 163.0ms (0.5% of total)ival-cosu: 148.0ms (0.4% of total)const: 0.0ms (0% of total)ival-pi: 0.0ms (0% of total)| 200× | saturated |
| 200× | iter-limit |
| 194× | node-limit |
Compiled 2 815 062 to 788 238 computations (72% saved)
| 197× | iter-limit |
1203 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 147.0ms | im | @ | inf | ((* (cosh im) (sin re)) (cosh im) im (sin re) (* (+ (* (* re re) -1/6) 1) re) (+ (* (* re re) -1/6) 1) (* re re) re -1/6 1 (* (* 1/2 (sin re)) (+ (exp (- 0 im)) (exp im))) (* 1/2 (* re (+ (exp im) (exp (neg im))))) (+ (* (* (* 1/2 re) im) im) re) (* (* 1/2 re) im) (* 1/2 re) 1/2 (* (* 1/2 (sin re)) (+ (exp (- 0 im)) (exp im))) (* 1/2 (* re (+ (exp im) (exp (neg im))))) (+ (* (* (* im im) re) 1/2) re) (* (* im im) re) (* im im) (* (* 1/2 (sin re)) (+ (exp (- 0 im)) (exp im))) (* 1/2 (* re (+ (exp im) (exp (neg im))))) (* re (+ (exp im) (exp (neg im)))) (+ (exp im) (exp (neg im))) (exp im) (exp (neg im)) (+ 1 (* -1 im)) (* -1 im) -1 (* (* 1/2 (sin re)) (+ (exp (- 0 im)) (exp im))) (* 1/2 (sin re)) (* re (+ 1/2 (* -1/12 (pow re 2)))) (+ 1/2 (* -1/12 (pow re 2))) (* -1/12 (pow re 2)) -1/12 (pow re 2) 2 (+ (exp (- 0 im)) (exp im))) |
| 138.0ms | base | @ | -inf | ((/ (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (+ (* (log base) (log base)) (* 0 0))) (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (log (sqrt (+ (* re re) (* im im)))) (sqrt (+ (* re re) (* im im))) re im (log base) base (* (atan2 im re) 0) 0 (+ (* (log base) (log base)) (* 0 0)) (* (log base) (log base)) (* 0 0) (/ (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (+ (* (log base) (log base)) (* 0 0))) (/ (log (neg im)) (log base)) (log (neg im)) (neg im) (/ (log (sqrt (+ (* im im) (* re re)))) (log base)) (log (sqrt (+ (* im im) (* re re)))) (sqrt (+ (* im im) (* re re))) (+ (* im im) (* re re)) (* re re) (log (pow (sqrt (+ (* im im) (* re re))) (/ 1 (log base)))) (pow (sqrt (+ (* im im) (* re re))) (/ 1 (log base))) (/ 1 (log base)) 1 (* (pow (log base) -2) (* (log base) (log (sqrt (+ (* im im) (* re re)))))) (pow (log base) -2) -2 (* (log base) (log (sqrt (+ (* im im) (* re re)))))) |
| 136.0ms | base | @ | inf | ((/ (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (* (log base) (log base))) (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (log (sqrt (+ (* re re) (* im im)))) (sqrt (+ (* re re) (* im im))) re im (log base) base (* (atan2 im re) 0) 0 (* (log base) (log base)) (/ (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (+ (* (log base) (log base)) (* 0 0))) (* (/ 1 (log base)) (log (neg im))) (/ 1 (log base)) 1 (log (neg im)) (neg im) (- (+ (/ (log (sqrt (+ (* im im) (* re re)))) (log base)) 1) 1) (+ (/ (log (sqrt (+ (* im im) (* re re)))) (log base)) 1) (/ (log (sqrt (+ (* im im) (* re re)))) (log base)) (log (sqrt (+ (* im im) (* re re)))) (sqrt (+ (* im im) (* re re))) (+ (* im im) (* re re)) (* re re) (log (pow (sqrt (+ (* im im) (* re re))) (/ 1 (log base)))) (pow (sqrt (+ (* im im) (* re re))) (/ 1 (log base))) (exp (* -1 (/ (log (/ 1 re)) (log base)))) (* -1 (/ (log (/ 1 re)) (log base))) -1 (/ (log (/ 1 re)) (log base)) (log (/ 1 re)) (/ 1 re) (/ (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (+ (* (log base) (log base)) (* 0 0))) (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (* -1 (* (log base) (log (/ 1 re)))) (* (log base) (log (/ 1 re))) (+ (* (log base) (log base)) (* 0 0)) (* 0 0)) |
| 120.0ms | x.im | @ | inf | ((* (exp (- (* (log (fabs (sqrt (+ (* x.re x.re) (* x.im x.im))))) y.re) (* (atan2 x.im x.re) y.im))) (cos (+ (* (log (fabs (sqrt (+ (* x.re x.re) (* x.im x.im))))) y.im) (* (atan2 x.im x.re) y.re)))) (exp (- (* (log (fabs (sqrt (+ (* x.re x.re) (* x.im x.im))))) y.re) (* (atan2 x.im x.re) y.im))) (- (* (log (fabs (sqrt (+ (* x.re x.re) (* x.im x.im))))) y.re) (* (atan2 x.im x.re) y.im)) (* (log (fabs (sqrt (+ (* x.re x.re) (* x.im x.im))))) y.re) (log (fabs (sqrt (+ (* x.re x.re) (* x.im x.im))))) (fabs (sqrt (+ (* x.re x.re) (* x.im x.im)))) (sqrt (+ (* x.re x.re) (* x.im x.im))) (neg x.re) x.re y.re (* (atan2 x.im x.re) y.im) (atan2 x.im x.re) x.im y.im (cos (+ (* (log (fabs (sqrt (+ (* x.re x.re) (* x.im x.im))))) y.im) (* (atan2 x.im x.re) y.re))) (+ (* (log (fabs (sqrt (+ (* x.re x.re) (* x.im x.im))))) y.im) (* (atan2 x.im x.re) y.re)) (* (log (fabs (sqrt (+ (* x.re x.re) (* x.im x.im))))) y.im) (* (atan2 x.im x.re) y.re) (* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (cos (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)))) (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im)) (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) (sqrt (+ (* x.re x.re) (* x.im x.im))) (+ (* x.re x.re) (* x.im x.im)) (* x.re x.re) (* x.im x.im) (cos (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re))) (cos (* y.re (atan2 x.im x.re))) 1 (* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (cos (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)))) (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im)) (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) (* -1 (log (/ 1 x.im))) -1 (log (/ 1 x.im)) (/ 1 x.im) (cos (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re))) (cos (* y.re (atan2 x.im x.re))) (* y.re (atan2 x.im x.re)) (* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (sin (+ (* y.im (log (sqrt (+ (* x.im x.im) (* x.re x.re))))) (+ (* (PI) 1/2) (* (atan2 x.im x.re) y.re))))) (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (exp (neg (* y.im (atan2 x.im x.re)))) (neg (* y.im (atan2 x.im x.re))) (* y.im (atan2 x.im x.re)) (sin (+ (* y.im (log (sqrt (+ (* x.im x.im) (* x.re x.re))))) (+ (* (PI) 1/2) (* (atan2 x.im x.re) y.re)))) (+ (* y.im (log (sqrt (+ (* x.im x.im) (* x.re x.re))))) (+ (* (PI) 1/2) (* (atan2 x.im x.re) y.re))) (log (sqrt (+ (* x.im x.im) (* x.re x.re)))) (sqrt (+ (* x.im x.im) (* x.re x.re))) (+ (* x.im x.im) (* x.re x.re)) (+ (* (PI) 1/2) (* (atan2 x.im x.re) y.re)) (PI) 1/2 (* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (cos (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)))) (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im)) (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) (sqrt (+ (* x.re x.re) (* x.im x.im))) (+ (* x.re x.re) (* x.im x.im)) (pow x.im 2) 2) |
| 119.0ms | x | @ | inf | ((copysign (asinh (fabs x)) x) (asinh (fabs x)) (fabs x) x (copysign (log (+ (fabs x) (sqrt (+ (* x x) 1)))) x) (log (+ (fabs x) (sqrt (+ (* x x) 1)))) (+ (fabs x) (sqrt (+ (* x x) 1))) (* -1 x) -1 (copysign (log (+ (fabs x) (sqrt (+ (* x x) 1)))) x) (log (+ (fabs x) (sqrt (+ (* x x) 1)))) (+ (fabs x) (sqrt (+ (* x x) 1))) (sqrt (+ (* x x) 1)) 1 (copysign (log (+ (fabs x) (sqrt (+ (* x x) 1)))) x) (log (+ (fabs x) (sqrt (+ (* x x) 1)))) (+ (fabs x) (sqrt (+ (* x x) 1))) (* x (+ 1 (/ (fabs x) x))) (+ 1 (/ (fabs x) x)) (/ (fabs x) x) (copysign (log (+ (sqrt (+ (* x x) 1)) (fabs x))) x) (log (+ (sqrt (+ (* x x) 1)) (fabs x))) (+ (sqrt (+ (* x x) 1)) (fabs x)) (sqrt (+ (* x x) 1)) (+ (* x x) 1)) |
| 48× | node-limit |
| 9× | saturated |
Compiled 28 245 to 20 464 computations (27.5% saved)
| 34× | fuel |
| 23× | done |
Compiled 6 114 to 3 413 computations (44.2% saved)
132 calls:
| 976.0ms | y.re |
| 523.0ms | x |
| 392.0ms | im |
| 387.0ms | (*.f64 x.im y.im) |
| 335.0ms | (fabs.f64 x) |
Compiled 10 710 to 8 356 computations (22% saved)
Compiled 139 554 to 102 750 computations (26.4% saved)
| 58× | search |
| Probability | Valid | Unknown | Precondition | Infinite | Domain | Can't | Iter |
|---|---|---|---|---|---|---|---|
| 0% | 0% | 86.3% | 13.7% | 0% | 0% | 0% | 0 |
| 55.4% | 47.8% | 38.5% | 13.7% | 0% | 0% | 0% | 1 |
| 65.9% | 55.7% | 28.9% | 13.7% | 0% | 1.7% | 0% | 2 |
| 71.2% | 58.4% | 23.6% | 13.7% | 0% | 4.3% | 0% | 3 |
| 77.4% | 62% | 18.1% | 13.7% | 0% | 6.2% | 0% | 4 |
| 83.5% | 66.8% | 13.2% | 13.7% | 0% | 6.3% | 0% | 5 |
| 85.8% | 68.3% | 11.3% | 13.7% | 0% | 6.6% | 0% | 6 |
| 88.3% | 70.3% | 9.4% | 13.7% | 0% | 6.6% | 0% | 7 |
| 89.9% | 71.5% | 8% | 13.7% | 0% | 6.8% | 0% | 8 |
| 91.1% | 72.5% | 7.1% | 13.7% | 0% | 6.8% | 0% | 9 |
| 92.6% | 73.6% | 5.9% | 13.7% | 0% | 6.8% | 0% | 10 |
| 94% | 74.7% | 4.8% | 13.7% | 0% | 6.8% | 0% | 11 |
| 94.5% | 75.1% | 4.4% | 13.7% | 0% | 6.9% | 0% | 12 |
Compiled 1 498 to 816 computations (45.5% saved)
| 164× | binary-search |
| 103× | left-value |
| 159× | narrow-enough |
| 5× | predicate-same |
| 966.0ms | 11 185× | 0 | valid |
| 512.0ms | 1 444× | 1 | valid |
| 96.0ms | 130× | 2 | valid |
| 25.0ms | 105× | 3 | valid |
Compiled 77 033 to 63 365 computations (17.7% saved)
ival-mult!: 346.0ms (31.7% of total)adjust: 154.0ms (14.1% of total)ival-hypot: 154.0ms (14.1% of total)ival-log: 84.0ms (7.7% of total)ival-sin: 78.0ms (7.1% of total)ival-add!: 62.0ms (5.7% of total)ival-exp: 53.0ms (4.9% of total)ival-atan2: 48.0ms (4.4% of total)ival-div!: 35.0ms (3.2% of total)ival-cos: 31.0ms (2.8% of total)ival-sub!: 26.0ms (2.4% of total)ival-sqrt: 13.0ms (1.2% of total)ival-sinu: 4.0ms (0.4% of total)ival-pow: 3.0ms (0.3% of total)ival-fabs: 2.0ms (0.2% of total)ival-neg: 1.0ms (0.1% of total)Loading profile data...