Herbie run

Date:Sunday, May 11th, 2025
Commit:32d50127 on autofix-28-1
Seed:2025131
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:224 434.7 MB

Time bar (total: 3.2min)

sample1.2min (38.6%)

Memory
1 610.0MiB live, 87 805.8MiB allocated; 28.8s collecting garbage
Samples
38.0s433 955×0valid
8.4s26 390×1valid
4.4s9 393×2valid
1.1s10 289×0exit
1.0s4 264×0invalid
529.0ms921×3valid
Precisions
Click to see histograms. Total time spent on operations: 37.7s
ival-mult!: 12.0s (31.9% of total)
ival-exp: 3.7s (9.7% of total)
ival-hypot: 3.2s (8.6% of total)
ival-add!: 2.9s (7.6% of total)
ival-asin: 2.3s (6.1% of total)
ival-div!: 2.1s (5.5% of total)
adjust: 1.9s (5% of total)
ival-log: 1.7s (4.6% of total)
ival-sin: 1.4s (3.6% of total)
ival-cos: 1.4s (3.6% of total)
ival-sub!: 1.3s (3.6% of total)
ival-atan2: 795.0ms (2.1% of total)
ival-sqrt: 786.0ms (2.1% of total)
ival-pow: 433.0ms (1.1% of total)
ival-acosh: 359.0ms (1% of total)
ival-neg: 331.0ms (0.9% of total)
ival-sinu: 289.0ms (0.8% of total)
ival-asinh: 255.0ms (0.7% of total)
ival-fabs: 245.0ms (0.6% of total)
ival-atanh: 241.0ms (0.6% of total)
ival-cosu: 124.0ms (0.3% of total)
const: 0.0ms (0% of total)
ival-pi: 0.0ms (0% of total)
Bogosity

rewrite42.0s (22.2%)

Memory
894.7MiB live, 44 678.9MiB allocated; 13.6s collecting garbage
Stop Event
466×iter-limit
181×node-limit
14×unsound
4×saturated
Counts
23 146 → 57 652

derivations15.1s (8%)

Memory
-567.6MiB live, 13 328.1MiB allocated; 4.7s collecting garbage
Stop Event
34×fuel
23×done
Compiler

Compiled 8 382 to 4 137 computations (50.6% saved)

series12.9s (6.8%)

Memory
759.3MiB live, 19 145.5MiB allocated; 3.2s collecting garbage
Counts
5 275 → 17 871
Calls

1230 calls:

TimeVariablePointExpression
162.0ms
u1
@0
((+ (* (* (* (sqrt 2) (cos (* u2 (+ (PI) (PI))))) 1/6) (sqrt (neg (log u1)))) 1/2) (* (* (* (sqrt 2) (cos (* u2 (+ (PI) (PI))))) 1/6) (sqrt (neg (log u1)))) (* (* (sqrt 2) (cos (* u2 (+ (PI) (PI))))) 1/6) (* (sqrt 2) (cos (* u2 (+ (PI) (PI))))) (sqrt 2) 2 (cos (* u2 (+ (PI) (PI)))) (* u2 (+ (PI) (PI))) u2 (+ (PI) (PI)) (PI) 1/6 (sqrt (neg (log u1))) (neg (log u1)) (log u1) u1 1/2 (+ (* (* (/ 1 6) (pow (* -2 (log u1)) 1/2)) (cos (* (* 2 (PI)) u2))) 1/2) (+ (* (sqrt (* (log u1) -2)) 1/6) 1/2) (sqrt (* (log u1) -2)) (* (log u1) -2) -2 (+ (* (* (cos (* u2 (+ (PI) (PI)))) 1/6) (sqrt (* (log u1) -2))) 1/2) (* (cos (* u2 (+ (PI) (PI)))) 1/6) (+ (* (* (sqrt (neg (log u1))) 1/6) (* (sqrt 2) (cos (* u2 (+ (PI) (PI)))))) 1/2) (* (sqrt (neg (log u1))) 1/6) (+ (* (* (/ 1 6) (pow (pow (* (log u1) -2) 1/4) 2)) (cos (* (* 2 (PI)) u2))) 1/2) (* (* (/ 1 6) (pow (pow (* (log u1) -2) 1/4) 2)) (cos (* (* 2 (PI)) u2))) (* (/ 1 6) (pow (pow (* (log u1) -2) 1/4) 2)) (/ 1 6) 1 6 (pow (pow (* (log u1) -2) 1/4) 2) (pow (* (log u1) -2) 1/4) 1/4 (cos (* (* 2 (PI)) u2)) (* (* 2 (PI)) u2) (* 2 (PI)))
143.0ms
u1
@-inf
((+ (* (* (* (sqrt 2) (cos (* u2 (+ (PI) (PI))))) 1/6) (sqrt (neg (log u1)))) 1/2) (* (* (sqrt 2) (cos (* u2 (+ (PI) (PI))))) 1/6) (* (sqrt 2) (cos (* u2 (+ (PI) (PI))))) (sqrt 2) 2 (cos (* u2 (+ (PI) (PI)))) (* u2 (+ (PI) (PI))) u2 (+ (PI) (PI)) (PI) 1/6 (sqrt (neg (log u1))) (neg (log u1)) (log u1) u1 1/2 (+ (* (* (/ 1 6) (pow (* -2 (log u1)) 1/2)) (cos (* (* 2 (PI)) u2))) 1/2) (+ (* (* (sqrt (neg (log u1))) (sqrt 2)) 1/6) 1/2) (* (sqrt (neg (log u1))) (sqrt 2)) (+ (* (* (sqrt (neg (log u1))) 1/6) (* (sqrt 2) (cos (* u2 (+ (PI) (PI)))))) 1/2) (* (sqrt (neg (log u1))) 1/6) (* (sqrt 2) (cos (* u2 (+ (PI) (PI))))) (cos (* u2 (+ (PI) (PI)))) (+ (* (* -2 (* u2 u2)) (* (PI) (PI))) 1) (* -2 (* u2 u2)) -2 (* u2 u2) (* (PI) (PI)) 1 (+ (* (* (/ 1 6) (pow (* -2 (log u1)) 1/2)) (cos (* (* 2 (PI)) u2))) 1/2) (+ (* (exp (* (log (pow (* (log u1) -2) 1/4)) 2)) 1/6) 1/2) (exp (* (log (pow (* (log u1) -2) 1/4)) 2)) (* (log (pow (* (log u1) -2) 1/4)) 2) (log (pow (* (log u1) -2) 1/4)) (pow (* (log u1) -2) 1/4) (* (log u1) -2) 1/4 (+ (* (* (sqrt (* (log u1) -2)) 1/6) (cos (* (+ (PI) (PI)) u2))) 1/2) (* (sqrt (* (log u1) -2)) 1/6) (sqrt (* (log u1) -2)) (cos (* (+ (PI) (PI)) u2)) (* (+ (PI) (PI)) u2))
135.0ms
x.im
@0
((* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (sin (+ (* (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.re (* x.im x.im) x.im y.re (* (atan2 x.im x.re) y.im) (atan2 x.im x.re) y.im (sin (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re))) (+ (sin (* y.re (atan2 x.im x.re))) (* y.im (* (cos (* y.re (atan2 x.im x.re))) (log (sqrt (+ (* x.im x.im) (* x.re x.re))))))) (sin (* y.re (atan2 x.im x.re))) (* y.re (atan2 x.im x.re)) (* y.im (* (cos (* y.re (atan2 x.im x.re))) (log (sqrt (+ (* x.im x.im) (* x.re x.re)))))) (* (cos (* y.re (atan2 x.im x.re))) (log (sqrt (+ (* x.im x.im) (* x.re x.re))))) (cos (* y.re (atan2 x.im x.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)) (* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (sin (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)))) (* (sin (* y.re (atan2 x.im x.re))) (pow (sqrt (+ (* x.im x.im) (* x.re x.re))) y.re)) (pow (sqrt (+ (* x.im x.im) (* x.re x.re))) y.re) 1 (* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (sin (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)))) (* (sin (* y.re (atan2 x.im x.re))) (pow (sqrt (+ (* x.im x.im) (* x.re x.re))) y.re)) (pow (sqrt (+ (* x.im x.im) (* x.re x.re))) y.re) (exp (* -1 (* y.re (log (/ -1 x.im))))) (* -1 (* y.re (log (/ -1 x.im)))) -1 (* y.re (log (/ -1 x.im))) (log (/ -1 x.im)) (/ -1 x.im) (* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (sin (+ (* (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))) (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 (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re))) (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)) (+ (* y.im (log x.im)) (* y.re (atan2 x.im x.re))) (log x.im) (* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (sin (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)))) (* (sin (* y.re (atan2 x.im x.re))) (pow (sqrt (+ (* x.im x.im) (* x.re x.re))) y.re)) (pow (sqrt (+ (* x.im x.im) (* x.re x.re))) y.re) (+ (* 1/2 (/ (* (* x.im x.im) (* y.re (pow x.re y.re))) (* x.re x.re))) (pow x.re y.re)) 1/2 (/ (* (* x.im x.im) (* y.re (pow x.re y.re))) (* x.re x.re)) (* (* x.im x.im) (* y.re (pow x.re y.re))) (* y.re (pow x.re y.re)) (pow x.re y.re))
130.0ms
y.re
@0
((* (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.re (* x.im x.im) x.im y.re (* (atan2 x.im x.re) y.im) (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))) (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))) (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))) (pow (sqrt (+ (* x.im x.im) (* x.re x.re))) y.re)) (pow (sqrt (+ (* x.im x.im) (* x.re x.re))) y.re) (sqrt (+ (* x.im x.im) (* x.re x.re))) (+ (* x.im x.im) (* x.re x.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)))) (* (cos (+ (* y.im (log x.im)) (* y.re (atan2 x.im x.re)))) (exp (- (* y.re (log x.im)) (* y.im (atan2 x.im x.re))))) (cos (+ (* y.im (log x.im)) (* y.re (atan2 x.im x.re)))) (+ (* y.im (log x.im)) (* y.re (atan2 x.im x.re))) (log x.im) (exp (- (* y.re (log x.im)) (* y.im (atan2 x.im x.re)))) (- (* y.re (log x.im)) (* y.im (atan2 x.im x.re))) (* y.re (log x.im)) (* y.im (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))) (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))) (* -1 x.re) -1 (cos (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re))) (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)) (* (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))) (cos (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)))) (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 (* y.im (* (log (sqrt (+ (* x.im x.im) (* x.re x.re)))) (sin (* y.re (atan2 x.im x.re))))))) (* 1 (* y.im (* (log (sqrt (+ (* x.im x.im) (* x.re x.re)))) (sin (* y.re (atan2 x.im x.re)))))) 1 (* y.im (* (log (sqrt (+ (* x.im x.im) (* x.re x.re)))) (sin (* y.re (atan2 x.im x.re))))) (* (log (sqrt (+ (* x.im x.im) (* x.re x.re)))) (sin (* y.re (atan2 x.im x.re)))) (log (sqrt (+ (* x.im x.im) (* x.re x.re)))) (sin (* y.re (atan2 x.im x.re))))
125.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))) (neg (/ (neg (log (neg im))) (log base))) (/ (neg (log (neg im))) (log base)) (neg (log (neg im))) (log (neg im)) (neg im) (/ (+ (* (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)) (* (neg (log (neg re))) (neg (log base))) (neg (log (neg re))) (log (neg re)) (neg re) (neg (log base)) (/ (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (pow (exp 2) (log (neg (log base))))) (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (* (log re) (log base)) (log re) (pow (exp 2) (log (neg (log base)))) (exp 2) 2 (log (neg (log base))) (/ (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (+ (* (log base) (log base)) (* 0 0))) (neg (* (log base) (/ (neg (log im)) (* 1/2 (+ (* 2 (cosh (* (log (log base)) 2))) (* 2 (sinh (* (log (log base)) 2)))))))) (* (log base) (/ (neg (log im)) (* 1/2 (+ (* 2 (cosh (* (log (log base)) 2))) (* 2 (sinh (* (log (log base)) 2))))))) (/ (neg (log im)) (* 1/2 (+ (* 2 (cosh (* (log (log base)) 2))) (* 2 (sinh (* (log (log base)) 2)))))) (neg (log im)) (log im) (* 1/2 (+ (* 2 (cosh (* (log (log base)) 2))) (* 2 (sinh (* (log (log base)) 2))))) 1/2 (+ (* 2 (cosh (* (log (log base)) 2))) (* 2 (sinh (* (log (log base)) 2)))) (cosh (* (log (log base)) 2)) (* (log (log base)) 2) (log (log base)) (* 2 (sinh (* (log (log base)) 2))) (sinh (* (log (log base)) 2)))

regimes12.5s (6.6%)

Memory
-278.5MiB live, 16 442.3MiB allocated; 5.5s collecting garbage
Counts
6 613 → 761
Calls

132 calls:

1.2s
(log.f64 u1)
1.0s
(fabs.f64 x)
749.0ms
im
592.0ms
x
530.0ms
re
Compiler

Compiled 13 381 to 10 491 computations (21.6% saved)

preprocess11.5s (6.1%)

Memory
72.9MiB live, 13 182.3MiB allocated; 2.8s collecting garbage
Stop Event
49×node-limit
8×saturated
Compiler

Compiled 49 777 to 34 470 computations (30.8% saved)

eval10.7s (5.7%)

Memory
170.6MiB live, 15 189.2MiB allocated; 5.7s collecting garbage
Compiler

Compiled 1 101 766 to 296 051 computations (73.1% saved)

prune5.2s (2.7%)

Memory
-318.4MiB live, 7 556.3MiB allocated; 1.5s collecting garbage
Counts
58 394 → 2 611
Compiler

Compiled 163 582 to 114 167 computations (30.2% saved)

bsearch3.5s (1.8%)

Memory
167.3MiB live, 3 952.8MiB allocated; 734ms collecting garbage
Algorithm
200×binary-search
167×left-value
Stop Event
194×narrow-enough
6×predicate-same
Samples
1.4s13 156×0valid
633.0ms1 658×1valid
140.0ms236×2valid
28.0ms38×3valid
Compiler

Compiled 90 685 to 74 175 computations (18.2% saved)

Precisions
Click to see histograms. Total time spent on operations: 1.7s
ival-mult!: 541.0ms (31.9% of total)
ival-div!: 223.0ms (13.2% of total)
ival-hypot: 203.0ms (12% of total)
ival-log: 124.0ms (7.3% of total)
ival-exp: 121.0ms (7.1% of total)
ival-sin: 95.0ms (5.6% of total)
ival-cos: 76.0ms (4.5% of total)
adjust: 73.0ms (4.3% of total)
ival-atan2: 70.0ms (4.1% of total)
ival-add!: 64.0ms (3.8% of total)
ival-asin: 44.0ms (2.6% of total)
ival-sub!: 38.0ms (2.2% of total)
ival-sqrt: 19.0ms (1.1% of total)
ival-fabs: 3.0ms (0.2% of total)
ival-copysign: 1.0ms (0.1% of total)
ival-neg: 1.0ms (0.1% of total)
ival-pi: 0.0ms (0% of total)

analyze2.6s (1.4%)

Memory
38.9MiB live, 3 146.1MiB allocated; 1.3s collecting garbage
Algorithm
58×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
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
Compiler

Compiled 1 498 to 816 computations (45.5% saved)

start19.0ms (0%)

Memory
-37.6MiB live, 6.3MiB allocated; 17ms collecting garbage

end0.0ms (0%)

Memory
1.0MiB live, 1.0MiB allocated; 0ms collecting garbage

Profiling

Loading profile data...