Herbie run

Date:Friday, May 16th, 2025
Commit:7acd8706 on new-rules
Seed:2025136
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:229 480.4 MB

Time bar (total: 3.0min)

sample1.2min (38.8%)

Memory
1 430.8MiB live, 88 114.1MiB allocated; 27.2s collecting garbage
Samples
28.2s224 593×0valid
7.9s64 969×0invalid
6.3s23 491×1valid
3.9s14 658×1invalid
2.8s9 604×2valid
2.2s6 495×3valid
134.0ms582×2invalid
21.0ms232×0exit
3.0ms9×4valid
0.0ms1×5exit
Precisions
Click to see histograms. Total time spent on operations: 36.3s
ival-mult!: 8.8s (24.3% of total)
ival-div!: 4.5s (12.3% of total)
ival-pow2: 2.9s (7.9% of total)
adjust: 2.8s (7.7% of total)
ival-sqrt: 2.6s (7.3% of total)
ival-sin: 2.4s (6.5% of total)
ival-exp: 2.3s (6.4% of total)
ival-pow: 2.0s (5.6% of total)
ival-sub!: 1.6s (4.5% of total)
ival-add!: 1.5s (4.2% of total)
ival-tan: 1.2s (3.3% of total)
ival-cos: 1.1s (3% of total)
ival-neg: 648.0ms (1.8% of total)
ival-acos: 594.0ms (1.6% of total)
ival-log: 407.0ms (1.1% of total)
ival-hypot: 377.0ms (1% of total)
ival-asin: 196.0ms (0.5% of total)
ival-tanu: 190.0ms (0.5% of total)
ival-atan: 100.0ms (0.3% of total)
ival-fabs: 55.0ms (0.2% of total)
ival-<: 1.0ms (0% of total)
ival-and: 1.0ms (0% of total)
exact: 0.0ms (0% of total)
ival-pi: 0.0ms (0% of total)
ival-assert: 0.0ms (0% of total)
Bogosity

rewrite29.9s (16.7%)

Memory
783.2MiB live, 35 533.0MiB allocated; 8.9s collecting garbage
Stop Event
273×iter-limit
128×node-limit
Counts
24 445 → 56 047

regimes16.9s (9.4%)

Memory
-262.4MiB live, 23 464.5MiB allocated; 6.5s collecting garbage
Counts
9 896 → 701
Calls

156 calls:

1.6s
l
601.0ms
Vef
493.0ms
t
453.0ms
k
440.0ms
x
Compiler

Compiled 10 851 to 12 231 computations (-12.7% saved)

series15.9s (8.9%)

Memory
429.6MiB live, 22 433.6MiB allocated; 6.5s collecting garbage
Counts
4 664 → 19 781
Calls

1200 calls:

TimeVariablePointExpression
317.0ms
U
@-inf
((sqrt (* (- (+ (* -2 (* l (/ l Om))) t) (* n (* (* (/ l Om) (/ l Om)) (- U U*)))) (* (+ n n) U))) (* (- (+ (* -2 (* l (/ l Om))) t) (* n (* (* (/ l Om) (/ l Om)) (- U U*)))) (* (+ n n) U)) (- (+ (* -2 (* l (/ l Om))) t) (* n (* (* (/ l Om) (/ l Om)) (- U U*)))) (+ (* -2 (* l (/ l Om))) t) -2 (* l (/ l Om)) l (/ l Om) Om t (* n (* (* (/ l Om) (/ l Om)) (- U U*))) n (* (* (/ l Om) (/ l Om)) (- U U*)) (* (/ l Om) (/ l Om)) (- U U*) U U* (* (+ n n) U) (+ n n) (sqrt (* (* (* 2 n) U) (- (- t (* 2 (/ (* l l) Om))) (* (* n (pow (/ l Om) 2)) (- U U*))))) (* (* (* 2 n) U) (- (- t (* 2 (/ (* l l) Om))) (* (* n (pow (/ l Om) 2)) (- U U*)))) (* (* (* t n) U) 2) (* (* t n) U) (* t n) 2 (sqrt (* (* (* 2 n) U) (- (- t (* 2 (/ (* l l) Om))) (* (* n (pow (/ l Om) 2)) (- U U*))))) (* (sqrt (* (/ (* (* U (* l l)) (- U U*)) (* Om Om)) -2)) n) (sqrt (* (/ (* (* U (* l l)) (- U U*)) (* Om Om)) -2)) (* (/ (* (* U (* l l)) (- U U*)) (* Om Om)) -2) (/ (* (* U (* l l)) (- U U*)) (* Om Om)) (* (* U (* l l)) (- U U*)) (* U (* l l)) (* l l) (* Om Om) (sqrt (* (* (* 2 n) U) (- (- t (* 2 (/ (* l l) Om))) (* (* n (pow (/ l Om) 2)) (- U U*))))) (* (sqrt (* (* (* (+ (* n (/ (- U U*) (* Om Om))) (/ 2 Om)) n) U) -2)) l) (sqrt (* (* (* (+ (* n (/ (- U U*) (* Om Om))) (/ 2 Om)) n) U) -2)) (* (* (* (+ (* n (/ (- U U*) (* Om Om))) (/ 2 Om)) n) U) -2) (* (* (+ (* n (/ (- U U*) (* Om Om))) (/ 2 Om)) n) U) (* (+ (* n (/ (- U U*) (* Om Om))) (/ 2 Om)) n) (+ (* n (/ (- U U*) (* Om Om))) (/ 2 Om)) (/ (- U U*) (* Om Om)) (/ 2 Om) (sqrt (* (+ n n) (* U (- (+ (* -2 (* l (/ l Om))) t) (* n (* (* (/ l Om) (/ l Om)) (- U U*))))))) (* (+ n n) (* U (- (+ (* -2 (* l (/ l Om))) t) (* n (* (* (/ l Om) (/ l Om)) (- U U*)))))) (* U (- (+ (* -2 (* l (/ l Om))) t) (* n (* (* (/ l Om) (/ l Om)) (- U U*))))))
211.0ms
f
@-inf
((neg (* 4 (/ (log (* 1 (/ (cosh (* (* 1/4 (PI)) f)) (sinh (* (* 1/4 (PI)) f))))) (PI)))) (* 4 (/ (log (* 1 (/ (cosh (* (* 1/4 (PI)) f)) (sinh (* (* 1/4 (PI)) f))))) (PI))) 4 (/ (log (* 1 (/ (cosh (* (* 1/4 (PI)) f)) (sinh (* (* 1/4 (PI)) f))))) (PI)) (log (* 1 (/ (cosh (* (* 1/4 (PI)) f)) (sinh (* (* 1/4 (PI)) f))))) (* 1 (/ (cosh (* (* 1/4 (PI)) f)) (sinh (* (* 1/4 (PI)) f)))) 1 (/ (cosh (* (* 1/4 (PI)) f)) (sinh (* (* 1/4 (PI)) f))) (cosh (* (* 1/4 (PI)) f)) (* (* 1/4 (PI)) f) (* 1/4 (PI)) 1/4 (PI) f (sinh (* (* 1/4 (PI)) f)) (neg (* (/ 1 (/ (PI) 4)) (log (/ (+ (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))) (- (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))))))) (* (/ (log (/ 2 (* (* (PI) 1/2) f))) (PI)) -4) (/ (log (/ 2 (* (* (PI) 1/2) f))) (PI)) (log (/ 2 (* (* (PI) 1/2) f))) (/ 2 (* (* (PI) 1/2) f)) 2 (* (* (PI) 1/2) f) (* (PI) 1/2) 1/2 -4 (neg (* (/ 1 (/ (PI) 4)) (log (/ (+ (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))) (- (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))))))) (* (/ 1 (/ (PI) 4)) (log (/ (+ (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))) (- (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f))))))) (/ 1 (/ (PI) 4)) (/ (PI) 4) (log (/ (+ (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))) (- (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))))) (/ (+ (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))) (- (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f))))) (/ (+ (* (* (/ (PI) (* (PI) 1/2)) 0) f) (/ 2 (* (PI) 1/2))) f) (+ (* (* (/ (PI) (* (PI) 1/2)) 0) f) (/ 2 (* (PI) 1/2))) (* (/ (PI) (* (PI) 1/2)) 0) (/ (PI) (* (PI) 1/2)) 0 (/ 2 (* (PI) 1/2)) (neg (* (/ 1 (/ (PI) 4)) (log (/ (+ (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))) (- (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))))))) (* (/ 1 (/ (PI) 4)) (log (/ (+ (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))) (- (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f))))))) (log (/ (+ (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))) (- (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))))) (/ (+ (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))) (- (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f))))) (+ (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))) (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f))) (neg (* (/ (PI) 4) f)) (* (/ (PI) 4) f) (- (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))) (neg (* (/ 1 (/ (PI) 4)) (- (log (* 2 (cosh (* (* 1/4 (PI)) f)))) (log (* 2 (sinh (* (* 1/4 (PI)) f))))))) (* (/ 1 (/ (PI) 4)) (- (log (* 2 (cosh (* (* 1/4 (PI)) f)))) (log (* 2 (sinh (* (* 1/4 (PI)) f)))))) (- (log (* 2 (cosh (* (* 1/4 (PI)) f)))) (log (* 2 (sinh (* (* 1/4 (PI)) f))))) (log (* 2 (cosh (* (* 1/4 (PI)) f)))) (* 2 (cosh (* (* 1/4 (PI)) f))) (log (* 2 (sinh (* (* 1/4 (PI)) f)))) (* 2 (sinh (* (* 1/4 (PI)) f))))
206.0ms
x
@inf
((+ (neg (* x (/ 1 (tan B)))) (/ 1 (sin B))) (neg (* x (/ 1 (tan B)))) (* x (/ 1 (tan B))) x (/ 1 (tan B)) 1 (tan B) B (/ 1 (sin B)) (sin B))
186.0ms
t
@0
((/ 2 (* (* (* (exp (- (* (log t) 3) (* (log l) 2))) (sin k)) (tan k)) (+ (+ 1 (pow (/ k t) 2)) 1))) 2 (* (* (* (exp (- (* (log t) 3) (* (log l) 2))) (sin k)) (tan k)) (+ (+ 1 (pow (/ k t) 2)) 1)) (* (* (exp (- (* (log t) 3) (* (log l) 2))) (sin k)) (tan k)) (* (exp (- (* (log t) 3) (* (log l) 2))) (sin k)) (exp (- (* (log t) 3) (* (log l) 2))) (- (* (log t) 3) (* (log l) 2)) (* (log t) 3) (log t) t 3 (* (log l) 2) (log l) l (sin k) k (tan k) (+ (+ 1 (pow (/ k t) 2)) 1) (+ 1 (pow (/ k t) 2)) 1 (pow (/ k t) 2) (/ k t) (/ 2 (* (* (* (/ (pow t 3) (* l l)) (sin k)) (tan k)) (+ (+ 1 (pow (/ k t) 2)) 1))) (/ (* l l) (* (* k k) (* (* t t) t))) (* l l) (* (* k k) (* (* t t) t)) (* k k) (* (* t t) t) (* t t) (/ 2 (* (* (* (/ (pow t 3) (* l l)) (sin k)) (tan k)) (+ (+ 1 (pow (/ k t) 2)) 1))) (/ (+ (* (/ (* (* (+ (/ 1 (* t t)) 1/3) (* l l)) (* k k)) (* (* t t) t)) -1/2) (/ (* l l) (* (* t t) t))) (* k k)) (+ (* (/ (* (* (+ (/ 1 (* t t)) 1/3) (* l l)) (* k k)) (* (* t t) t)) -1/2) (/ (* l l) (* (* t t) t))) (/ (* (* (+ (/ 1 (* t t)) 1/3) (* l l)) (* k k)) (* (* t t) t)) (* (* (+ (/ 1 (* t t)) 1/3) (* l l)) (* k k)) (* (+ (/ 1 (* t t)) 1/3) (* l l)) (+ (/ 1 (* t t)) 1/3) (/ 1 (* t t)) 1/3 -1/2 (/ (* l l) (* (* t t) t)) (/ 2 (* (* (* (/ (pow t 3) (* l l)) (sin k)) (tan k)) (+ (+ 1 (pow (/ k t) 2)) 1))) (* (* (* (/ (pow t 3) (* l l)) (sin k)) (tan k)) (+ (+ 1 (pow (/ k t) 2)) 1)) (* (* k k) (* t (/ (- 1/2 (* 1/2 (cos (* 2 k)))) (* (cos k) (* l l))))) (* t (/ (- 1/2 (* 1/2 (cos (* 2 k)))) (* (cos k) (* l l)))) (/ (- 1/2 (* 1/2 (cos (* 2 k)))) (* (cos k) (* l l))) (- 1/2 (* 1/2 (cos (* 2 k)))) 1/2 (* 1/2 (cos (* 2 k))) (cos (* 2 k)) (* 2 k) (* (cos k) (* l l)) (cos k) (/ 2 (* (* (* (/ (pow (pow t 3/2) 2) (* l l)) (sin k)) (tan k)) (+ (+ 1 (pow (/ k t) 2)) 1))) (* (* (* (/ (pow (pow t 3/2) 2) (* l l)) (sin k)) (tan k)) (+ (+ 1 (pow (/ k t) 2)) 1)) (* (* (/ (pow (pow t 3/2) 2) (* l l)) (sin k)) (tan k)) (* (/ (pow (pow t 3/2) 2) (* l l)) (sin k)) (/ (pow (pow t 3/2) 2) (* l l)) (pow (pow t 3/2) 2) (pow t 3/2) 3/2)
147.0ms
f
@inf
((neg (* 4 (/ (log (* 1 (/ (cosh (* (* 1/4 (PI)) f)) (sinh (* (* 1/4 (PI)) f))))) (PI)))) (* 4 (/ (log (* 1 (/ (cosh (* (* 1/4 (PI)) f)) (sinh (* (* 1/4 (PI)) f))))) (PI))) 4 (/ (log (* 1 (/ (cosh (* (* 1/4 (PI)) f)) (sinh (* (* 1/4 (PI)) f))))) (PI)) (log (* 1 (/ (cosh (* (* 1/4 (PI)) f)) (sinh (* (* 1/4 (PI)) f))))) (* 1 (/ (cosh (* (* 1/4 (PI)) f)) (sinh (* (* 1/4 (PI)) f)))) 1 (/ (cosh (* (* 1/4 (PI)) f)) (sinh (* (* 1/4 (PI)) f))) (cosh (* (* 1/4 (PI)) f)) (* (* 1/4 (PI)) f) (* 1/4 (PI)) 1/4 (PI) f (sinh (* (* 1/4 (PI)) f)) (neg (* (/ 1 (/ (PI) 4)) (log (/ (+ (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))) (- (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))))))) (* (/ (log (/ 2 (* (* (PI) 1/2) f))) (PI)) -4) (/ (log (/ 2 (* (* (PI) 1/2) f))) (PI)) (log (/ 2 (* (* (PI) 1/2) f))) (/ 2 (* (* (PI) 1/2) f)) 2 (* (* (PI) 1/2) f) (* (PI) 1/2) 1/2 -4 (neg (* (/ 1 (/ (PI) 4)) (log (/ (+ (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))) (- (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))))))) (* (/ 1 (/ (PI) 4)) (log (/ (+ (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))) (- (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f))))))) (/ 1 (/ (PI) 4)) (/ (PI) 4) (log (/ (+ (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))) (- (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))))) (/ (+ (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))) (- (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f))))) (/ (+ (* (* (/ (PI) (* (PI) 1/2)) 0) f) (/ 2 (* (PI) 1/2))) f) (+ (* (* (/ (PI) (* (PI) 1/2)) 0) f) (/ 2 (* (PI) 1/2))) (* (/ (PI) (* (PI) 1/2)) 0) (/ (PI) (* (PI) 1/2)) 0 (/ 2 (* (PI) 1/2)) (neg (* (/ 1 (/ (PI) 4)) (log (/ (+ (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))) (- (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))))))) (* (/ 1 (/ (PI) 4)) (log (/ (+ (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))) (- (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f))))))) (log (/ (+ (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))) (- (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))))) (/ (+ (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))) (- (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f))))) (+ (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))) (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f))) (neg (* (/ (PI) 4) f)) (* (/ (PI) 4) f) (- (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))) (neg (* (/ 1 (/ (PI) 4)) (- (log (* 2 (cosh (* (* 1/4 (PI)) f)))) (log (* 2 (sinh (* (* 1/4 (PI)) f))))))) (* (/ 1 (/ (PI) 4)) (- (log (* 2 (cosh (* (* 1/4 (PI)) f)))) (log (* 2 (sinh (* (* 1/4 (PI)) f)))))) (- (log (* 2 (cosh (* (* 1/4 (PI)) f)))) (log (* 2 (sinh (* (* 1/4 (PI)) f))))) (log (* 2 (cosh (* (* 1/4 (PI)) f)))) (* 2 (cosh (* (* 1/4 (PI)) f))) (log (* 2 (sinh (* (* 1/4 (PI)) f)))) (* 2 (sinh (* (* 1/4 (PI)) f))))

derivations11.1s (6.2%)

Memory
89.6MiB live, 10 645.8MiB allocated; 1.7s collecting garbage
Stop Event
32×fuel
Compiler

Compiled 6 689 to 3 917 computations (41.4% saved)

preprocess9.8s (5.5%)

Memory
-531.1MiB live, 12 318.5MiB allocated; 3.7s collecting garbage
Stop Event
32×node-limit
Compiler

Compiled 108 355 to 83 336 computations (23.1% saved)

analyze8.5s (4.7%)

Memory
166.7MiB live, 10 344.3MiB allocated; 3.2s collecting garbage
Algorithm
32×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%98.2%1.8%0%0%0%0
22.2%21.8%76.4%1.8%0%0%0%1
22.6%21.8%74.8%1.8%0%1.6%0%2
28.6%26.5%66.3%1.8%0%5.5%0%3
32.6%29.6%61.2%1.8%0%7.4%0%4
35.8%32.3%58%1.8%0%8%0%5
40.1%36.1%54%1.8%0%8.1%0%6
45.5%40.6%48.7%1.8%0%8.9%0%7
47.9%42.1%45.8%1.8%0%10.3%0%8
51%44.6%43%1.8%0%10.6%0%9
52.1%45.5%41.8%1.8%0%11%0%10
53.9%46.7%40%1.8%0%11.5%0%11
55.6%47.9%38.2%1.8%0%12.1%0%12
Compiler

Compiled 798 to 574 computations (28.1% saved)

eval8.3s (4.6%)

Memory
371.9MiB live, 13 605.2MiB allocated; 3.1s collecting garbage
Compiler

Compiled 1 136 452 to 289 410 computations (74.5% saved)

prune4.8s (2.7%)

Memory
-249.3MiB live, 7 758.1MiB allocated; 1.9s collecting garbage
Counts
53 323 → 2 988
Compiler

Compiled 172 796 to 140 936 computations (18.4% saved)

bsearch4.5s (2.5%)

Memory
36.8MiB live, 5 259.4MiB allocated; 2.3s collecting garbage
Algorithm
197×left-value
172×binary-search
Stop Event
166×narrow-enough
4×predicate-same
2×predicate-failed
Samples
1.8s13 480×0valid
210.0ms1 602×0invalid
114.0ms531×1valid
10.0ms31×3valid
9.0ms38×2valid
3.0ms18×1invalid
Compiler

Compiled 77 864 to 75 812 computations (2.6% saved)

Precisions
Click to see histograms. Total time spent on operations: 1.5s
ival-pow: 268.0ms (17.4% of total)
ival-mult!: 243.0ms (15.8% of total)
ival-sin: 218.0ms (14.2% of total)
ival-div!: 167.0ms (10.8% of total)
ival-tan: 132.0ms (8.6% of total)
ival-pow2: 109.0ms (7.1% of total)
ival-add!: 91.0ms (5.9% of total)
ival-sub!: 65.0ms (4.2% of total)
ival-exp: 57.0ms (3.7% of total)
ival-cos: 55.0ms (3.6% of total)
ival-neg: 37.0ms (2.4% of total)
ival-tanu: 26.0ms (1.7% of total)
adjust: 25.0ms (1.6% of total)
ival-sqrt: 24.0ms (1.6% of total)
ival-hypot: 17.0ms (1.1% of total)
ival-fabs: 6.0ms (0.4% of total)
ival-atan: 0.0ms (0% of total)

start1.0ms (0%)

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

end0.0ms (0%)

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

Profiling

Loading profile data...