Herbie run

Date:Monday, May 12th, 2025
Commit:2ad78556 on artem-rules-updates
Seed:2025132
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:207 910.7 MB

Time bar (total: 3.4min)

sample1.3min (39.2%)

Memory
997.0MiB live, 81 622.5MiB allocated; 32.2s collecting garbage
Samples
42.0s433 948×0valid
8.4s26 114×1valid
4.8s9 617×2valid
1.7s4 512×0invalid
759.0ms8 366×0exit
312.0ms926×3valid
Precisions
Click to see histograms. Total time spent on operations: 41.0s
ival-mult!: 11.8s (28.7% of total)
ival-hypot: 4.5s (10.9% of total)
ival-exp: 4.2s (10.2% of total)
ival-div!: 3.7s (9% of total)
ival-add!: 3.2s (7.7% of total)
adjust: 2.3s (5.7% of total)
ival-log: 1.8s (4.5% of total)
ival-sin: 1.6s (3.9% of total)
ival-asin: 1.6s (3.8% of total)
ival-sub!: 1.1s (2.8% of total)
ival-cos: 1.1s (2.6% of total)
ival-atan2: 951.0ms (2.3% of total)
ival-sqrt: 858.0ms (2.1% of total)
ival-sinu: 492.0ms (1.2% of total)
ival-pow: 350.0ms (0.9% of total)
ival-acosh: 349.0ms (0.9% of total)
ival-asinh: 337.0ms (0.8% of total)
ival-fabs: 332.0ms (0.8% of total)
ival-neg: 253.0ms (0.6% of total)
ival-atanh: 180.0ms (0.4% of total)
ival-cosu: 84.0ms (0.2% of total)
const: 0.0ms (0% of total)
ival-pi: 0.0ms (0% of total)
Bogosity

rewrite52.2s (25.5%)

Memory
986.8MiB live, 43 223.1MiB allocated; 14.4s collecting garbage
Stop Event
412×iter-limit
162×node-limit
38×unsound
18×saturated
Counts
22 923 → 52 143

derivations16.3s (8%)

Memory
-188.2MiB live, 13 932.8MiB allocated; 4.2s collecting garbage
Stop Event
33×fuel
24×done
Compiler

Compiled 6 979 to 3 631 computations (48% saved)

series13.3s (6.5%)

Memory
886.3MiB live, 16 718.1MiB allocated; 3.7s collecting garbage
Counts
5 002 → 17 921
Calls

1170 calls:

TimeVariablePointExpression
430.0ms
im
@-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) (atan2 im re) 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 im) (log base)) (log im) (/ (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (+ (* (log base) (log base)) (* 0 0))) (/ (neg (log (/ -1 re))) (log base)) (neg (log (/ -1 re))) (log (/ -1 re)) (/ -1 re) -1 (/ (+ (* (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 re) (log base)) (log re) (* (+ (* (log base) (log (sqrt (+ (* im im) (* re re))))) 0) (/ 1 (* (log base) (log base)))) (+ (* (log base) (log (sqrt (+ (* im im) (* re re))))) 0) (log (sqrt (+ (* im im) (* re re)))) (sqrt (+ (* im im) (* re re))) (+ (* im im) (* re re)) (* re re) (/ 1 (* (log base) (log base))) 1)
218.0ms
base
@0
((/ (+ (* (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 re) (log base)) (log re) (/ (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (+ (* (log base) (log base)) (* 0 0))) (/ 1 (/ (log base) (neg (log (/ -1 re))))) 1 (/ (log base) (neg (log (/ -1 re)))) (neg (log (/ -1 re))) (log (/ -1 re)) (/ -1 re) -1 (/ (+ (* (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 im) (log base)) (log im) (/ 1 (/ (* (log base) (log base)) (* (log base) (log (sqrt (+ (* im im) (* re re))))))) (/ (* (log base) (log base)) (* (log base) (log (sqrt (+ (* im im) (* re re)))))) (* (log base) (log (sqrt (+ (* im im) (* re re))))) (log (sqrt (+ (* im im) (* re re)))) (sqrt (+ (* im im) (* re re))) (+ (* im im) (* re re)) (* re re))
196.0ms
x.re
@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 (- (* y.re (log (fabs x.re))) (* y.im (atan2 x.im x.re)))) (sin (+ (* y.im (log (fabs x.re))) (* y.re (atan2 x.im x.re))))) (exp (- (* y.re (log (fabs x.re))) (* y.im (atan2 x.im x.re)))) (- (* y.re (log (fabs x.re))) (* y.im (atan2 x.im x.re))) (* y.re (log (fabs x.re))) y.re (log (fabs x.re)) (fabs x.re) x.re (* y.im (atan2 x.im x.re)) y.im (atan2 x.im x.re) x.im (sin (+ (* y.im (log (fabs x.re))) (* y.re (atan2 x.im x.re)))) (+ (* y.im (log (fabs x.re))) (* 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 (+ (* (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)) (sin (* y.re (atan2 x.im x.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.re))))) (* -1 (* y.re (log (/ -1 x.re)))) -1 (* y.re (log (/ -1 x.re))) (log (/ -1 x.re)) (/ -1 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/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))) (* x.im x.im) (* y.re (pow x.re y.re)) (pow x.re y.re) (* 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)))) (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 (* 1/2 (/ (* x.im x.im) (* x.re x.re)))))) (* x.re (+ 1 (* 1/2 (/ (* x.im x.im) (* x.re x.re))))) (+ 1 (* 1/2 (/ (* x.im x.im) (* x.re x.re)))) (* 1/2 (/ (* x.im x.im) (* x.re x.re))) (/ (* x.im x.im) (* x.re x.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))) (+ (* (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))
178.0ms
beta
@inf
((/ (/ (* (* i (+ (+ alpha beta) i)) (+ (* beta alpha) (* i (+ (+ alpha beta) i)))) (* (+ (+ alpha beta) (* 2 i)) (+ (+ alpha beta) (* 2 i)))) (- (* (+ (+ alpha beta) (* 2 i)) (+ (+ alpha beta) (* 2 i))) 1)) (/ (* (* i (+ (+ alpha beta) i)) (+ (* beta alpha) (* i (+ (+ alpha beta) i)))) (* (+ (+ alpha beta) (* 2 i)) (+ (+ alpha beta) (* 2 i)))) (* (* i (+ (+ alpha beta) i)) (+ (* beta alpha) (* i (+ (+ alpha beta) i)))) (* i (+ (+ alpha beta) i)) i (+ (+ alpha beta) i) (+ alpha beta) alpha beta (+ (* beta alpha) (* i (+ (+ alpha beta) i))) (* beta alpha) (* (+ (+ alpha beta) (* 2 i)) (+ (+ alpha beta) (* 2 i))) (+ (+ alpha beta) (* 2 i)) (* 2 i) 2 (- (* (+ (+ alpha beta) (* 2 i)) (+ (+ alpha beta) (* 2 i))) 1) 1)
145.0ms
x.re
@inf
((* (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 (- (* y.re (log (fabs x.re))) (* y.im (atan2 x.im x.re)))) (sin (+ (* y.im (log (fabs x.re))) (* y.re (atan2 x.im x.re))))) (exp (- (* y.re (log (fabs x.re))) (* y.im (atan2 x.im x.re)))) (- (* y.re (log (fabs x.re))) (* y.im (atan2 x.im x.re))) (* y.re (log (fabs x.re))) y.re (log (fabs x.re)) (fabs x.re) x.re (* y.im (atan2 x.im x.re)) y.im (atan2 x.im x.re) x.im (sin (+ (* y.im (log (fabs x.re))) (* y.re (atan2 x.im x.re)))) (+ (* y.im (log (fabs x.re))) (* 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 (+ (* (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)) (sin (* y.re (atan2 x.im x.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.re))))) (* -1 (* y.re (log (/ -1 x.re)))) -1 (* y.re (log (/ -1 x.re))) (log (/ -1 x.re)) (/ -1 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/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))) (* x.im x.im) (* y.re (pow x.re y.re)) (pow x.re y.re) (* 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)))) (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 (* 1/2 (/ (* x.im x.im) (* x.re x.re)))))) (* x.re (+ 1 (* 1/2 (/ (* x.im x.im) (* x.re x.re))))) (+ 1 (* 1/2 (/ (* x.im x.im) (* x.re x.re)))) (* 1/2 (/ (* x.im x.im) (* x.re x.re))) (/ (* x.im x.im) (* x.re x.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))) (+ (* (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))

eval11.0s (5.4%)

Memory
-143.1MiB live, 13 660.5MiB allocated; 3.8s collecting garbage
Compiler

Compiled 1 010 338 to 274 947 computations (72.8% saved)

preprocess10.5s (5.1%)

Memory
-280.1MiB live, 12 112.1MiB allocated; 2.7s collecting garbage
Stop Event
48×node-limit
9×saturated
Compiler

Compiled 40 776 to 29 212 computations (28.4% saved)

regimes9.7s (4.8%)

Memory
-100.1MiB live, 13 017.1MiB allocated; 3.5s collecting garbage
Counts
5 555 → 644
Calls

123 calls:

598.0ms
x
549.0ms
re
518.0ms
im
409.0ms
y.im
366.0ms
x.im
Compiler

Compiled 9 043 to 7 707 computations (14.8% saved)

prune4.8s (2.3%)

Memory
111.8MiB live, 6 859.0MiB allocated; 1.1s collecting garbage
Counts
52 047 → 2 590
Compiler

Compiled 160 606 to 113 067 computations (29.6% saved)

bsearch4.3s (2.1%)

Memory
38.8MiB live, 3 577.3MiB allocated; 2.3s collecting garbage
Algorithm
156×binary-search
150×left-value
Stop Event
147×narrow-enough
9×predicate-same
Samples
1.2s10 460×0valid
826.0ms1 573×1valid
24.0ms32×3valid
23.0ms79×2valid
Compiler

Compiled 82 550 to 64 287 computations (22.1% saved)

Precisions
Click to see histograms. Total time spent on operations: 1.7s
ival-mult!: 450.0ms (26.6% of total)
ival-log: 331.0ms (19.6% of total)
ival-hypot: 209.0ms (12.4% of total)
ival-atan2: 143.0ms (8.5% of total)
ival-div!: 106.0ms (6.3% of total)
adjust: 91.0ms (5.4% of total)
ival-sub!: 78.0ms (4.6% of total)
ival-cos: 72.0ms (4.3% of total)
ival-sin: 71.0ms (4.2% of total)
ival-add!: 57.0ms (3.4% of total)
ival-exp: 54.0ms (3.2% of total)
ival-sqrt: 29.0ms (1.7% of total)

analyze2.3s (1.1%)

Memory
-67.3MiB live, 3 181.3MiB allocated; 708ms 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)

start3.0ms (0%)

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

end0.0ms (0%)

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

Profiling

Loading profile data...