Herbie run

Date:Thursday, April 3rd, 2025
Commit:753370c2 on random-cleanup
Seed:2025093
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:134 982.6 MB

Time bar (total: 2.0min)

sample46.1s (39.3%)

Memory
869.5MiB live, 52 500.0MiB allocated; 17.3s collecting garbage
Samples
19.9s276 791×0valid
6.8s35 440×1valid
6.0s17 557×2valid
354.0ms4 229×0invalid
205.0ms452×3valid
139.0ms951×0exit
56.0ms101×4exit
49.0ms101×3exit
4.0ms32×1exit
Precisions
Click to see histograms. Total time spent on operations: 22.5s
ival-mult!: 5.9s (26.3% of total)
ival-pow: 3.8s (16.7% of total)
adjust: 2.4s (10.8% of total)
ival-div!: 2.0s (8.8% of total)
ival-sin: 1.8s (8% of total)
ival-sub!: 1.5s (6.5% of total)
ival-add!: 1.4s (6.2% of total)
ival-cos: 1.2s (5.3% of total)
ival-sqrt: 913.0ms (4.1% of total)
ival-exp: 544.0ms (2.4% of total)
ival-neg: 417.0ms (1.9% of total)
ival-pow2: 256.0ms (1.1% of total)
ival-log1p: 121.0ms (0.5% of total)
ival-atan: 79.0ms (0.4% of total)
ival-expm1: 74.0ms (0.3% of total)
ival-tan: 68.0ms (0.3% of total)
ival-<=: 21.0ms (0.1% of total)
ival-hypot: 17.0ms (0.1% of total)
ival-and: 9.0ms (0% of total)
ival-fabs: 4.0ms (0% of total)
ival-if: 4.0ms (0% of total)
ival-==: 2.0ms (0% of total)
ival-assert: 1.0ms (0% of total)
const: 0.0ms (0% of total)
ival-<: 0.0ms (0% of total)
Bogosity

rewrite28.2s (24%)

Memory
499.0MiB live, 30 084.8MiB allocated; 5.8s collecting garbage
Stop Event
356×iter-limit
146×node-limit
1×saturated
1×unsound
Counts
21 015 → 42 899

eval9.4s (8%)

Memory
328.6MiB live, 11 693.0MiB allocated; 3.4s collecting garbage
Compiler

Compiled 2 709 501 to 212 006 computations (92.2% saved)

explain8.2s (7%)

Memory
-146.0MiB live, 10 585.1MiB allocated; 1.6s collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
-.f64#fcancellation12891
+.f64#fcancellation35384
-.f64(-.f64 (*.f64 #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64) t) #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64))oflow-left2210
sqrt.f64#foflow-rescue1840
/.f64#fo/o1780
log.f64(log.f64 (+.f64 #s(literal 1 binary64) x))sensitivity1630
/.f64#fn/o1420
pow.f64(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)sensitivity1290
-.f64#fnan-rescue1030
/.f64#fu/n970
/.f64#fn/u670
+.f64#fnan-rescue530
/.f64#fo/n500
/.f64(/.f64 (*.f64 (-.f64 x y) (+.f64 x y)) (+.f64 (*.f64 x x) (*.f64 y y)))u/u340
↳(*.f64 (-.f64 x y) (+.f64 x y))underflow34
↳(*.f64 y y)underflow85
↳(*.f64 x x)underflow123
↳(+.f64 (*.f64 x x) (*.f64 y y))underflow34
*.f64#fn*u280
*.f64#fn*o240
pow.f64(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)oflow-rescue160
↳(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)overflow22
↳(/.f64 i n)overflow16
↳(+.f64 #s(literal 1 binary64) (/.f64 i n))overflow16
sqrt.f64#fuflow-rescue100
Confusion
Predicted +Predicted -
+3549224
-1126355
Precision
0.9694072657743786
Recall
0.9406307977736549
Confusion?
Predicted +Predicted MaybePredicted -
+354915965
-1121826173
Precision?
0.9265367316341829
Recall?
0.9827723297111052
Freqs
test
numberfreq
06579
13214
2394
353
Total Confusion?
Predicted +Predicted MaybePredicted -
+2910
-208
Precision?
0.9375
Recall?
1.0
Samples
1.3s15 798×0valid
957.0ms3 170×1valid
570.0ms1 472×2valid
24.0ms40×3valid
Compiler

Compiled 6 784 to 1 355 computations (80% saved)

Precisions
Click to see histograms. Total time spent on operations: 1.7s
ival-mult!: 417.0ms (23.9% of total)
ival-pow: 372.0ms (21.3% of total)
ival-div!: 194.0ms (11.1% of total)
adjust: 189.0ms (10.8% of total)
ival-sub!: 155.0ms (8.9% of total)
ival-add!: 132.0ms (7.6% of total)
ival-sin: 86.0ms (4.9% of total)
ival-cos: 70.0ms (4% of total)
ival-pow2: 43.0ms (2.5% of total)
ival-exp: 32.0ms (1.8% of total)
ival-sqrt: 23.0ms (1.3% of total)
ival-neg: 14.0ms (0.8% of total)
ival-log1p: 5.0ms (0.3% of total)
ival-tan: 4.0ms (0.2% of total)
ival-atan: 4.0ms (0.2% of total)
ival-expm1: 3.0ms (0.2% of total)
const: 0.0ms (0% of total)

regimes6.1s (5.1%)

Memory
245.5MiB live, 8 182.7MiB allocated; 1.3s collecting garbage
Counts
4 244 → 543
Calls

96 calls:

942.0ms
x
271.0ms
d
265.0ms
a
239.0ms
(*.f64 (cos.f64 x) (exp.f64 (*.f64 #s(literal 10 binary64) (*.f64 x x))))
234.0ms
c
Compiler

Compiled 8 140 to 5 554 computations (31.8% saved)

series5.3s (4.5%)

Memory
601.8MiB live, 6 947.4MiB allocated; 1.3s collecting garbage
Counts
3 425 → 17 590
Calls

897 calls:

TimeVariablePointExpression
143.0ms
a
@-inf
((* (+ a (+ b (+ c d))) 2) (* 2 (+ c (+ (+ d b) a))) 2 (+ c (+ (+ d b) a)) c (+ (+ d b) a) (+ d b) d b a (* (+ a (+ b (+ c d))) 2) (+ a (+ b (+ c d))) (* (+ a (+ b (+ c d))) 2) (* 2 (+ b (+ (+ d c) a))) (+ b (+ (+ d c) a)) (+ (+ d c) a) (+ d c) (* (+ a (+ b (+ c d))) 2) (* (+ (* (/ (+ (+ d c) a) b) 2) 2) b) (+ (* (/ (+ (+ d c) a) b) 2) 2) (/ (+ (+ d c) a) b) (* (- (/ (* a a) (- a (+ (+ d c) b))) (/ (pow (+ (+ d c) b) 2) (- a (+ (+ d c) b)))) 2) (- (/ (* a a) (- a (+ (+ d c) b))) (/ (pow (+ (+ d c) b) 2) (- a (+ (+ d c) b)))) (/ (* a a) (- a (+ (+ d c) b))) (* a a) (- a (+ (+ d c) b)) (+ (+ d c) b) (/ (pow (+ (+ d c) b) 2) (- a (+ (+ d c) b))) (pow (+ (+ d c) b) 2))
119.0ms
eps
@inf
((- (pow (+ x eps) 5) (pow x 5)) (neg (* (- (neg (/ (+ (+ (* 4 x) (neg (/ (+ (* -4 (* x x)) (* -1 (+ (* (* x x) 6) (/ (+ (* (* (* x x) 6) x) (* (pow x 3) 4)) eps)))) eps))) x) eps)) 1) (pow eps 5))) (* (- (neg (/ (+ (+ (* 4 x) (neg (/ (+ (* -4 (* x x)) (* -1 (+ (* (* x x) 6) (/ (+ (* (* (* x x) 6) x) (* (pow x 3) 4)) eps)))) eps))) x) eps)) 1) (pow eps 5)) (* (+ (* (+ (* (* x x) -10) (* (* -1 (+ (* 5 x) eps)) eps)) eps) (neg (* (* (* x x) x) 10))) (* eps eps)) (+ (* (+ (* (* x x) -10) (* (* -1 (+ (* 5 x) eps)) eps)) eps) (neg (* (* (* x x) x) 10))) (+ (* (* x x) -10) (* (* -1 (+ (* 5 x) eps)) eps)) (* x x) x -10 (* (* -1 (+ (* 5 x) eps)) eps) (* -1 (+ (* 5 x) eps)) -1 (+ (* 5 x) eps) 5 eps (neg (* (* (* x x) x) 10)) (* (* (* x x) x) 10) (* (* x x) x) 10 (* eps eps) (- (pow (+ x eps) 5) (pow x 5)) (* (* (* 5 (* x x)) (* x x)) eps) (* (* 5 (* x x)) (* x x)) (* 5 (* x x)) (- (pow (+ x eps) 5) (pow x 5)) (* (* (pow x 4) eps) 5) (* (pow x 4) eps) (pow x 4) 4 (- (pow (+ x eps) 5) (pow x 5)) (* (* 5 (* (pow x 3) x)) eps) (* 5 (* (pow x 3) x)) (* (pow x 3) x) (pow x 3) 3 (- (pow (+ x eps) 5) (pow x 5)) (+ (* (pow x 4) eps) (* (pow x 4) (* 4 eps))) (* (pow x 4) (* 4 eps)) (* 4 eps))
91.0ms
i
@-inf
((* 100 (* (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i) n)) 100 (* (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i) n) (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i) (- (exp (* (log (+ 1 (/ i n))) n)) 1) (* (log (+ 1 (/ i n))) n) i n (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (/ (* (- (exp i) 1) n) i) (+ (* (* n i) 1/2) n) (* n i) 1/2 (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (- (pow (+ 1 (/ i n)) n) 1) (pow (+ 1 (/ i n)) n) 1 (/ i n) (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (/ (* (log (/ i n)) (* n n)) i) (* (log (/ i n)) (* n n)) (log (/ i n)) (* n n) (* 100 (* (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i) n)) (* (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i) n) (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i) (* n (/ (+ (* -1 (log n)) (log i)) i)) (/ (+ (* -1 (log n)) (log i)) i) (+ (* -1 (log n)) (log i)) -1 (log n) (log i))
90.0ms
i
@inf
((* 100 (* (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i) n)) 100 (* (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i) n) (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i) (- (exp (* (log (+ 1 (/ i n))) n)) 1) (* (log (+ 1 (/ i n))) n) i n (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (/ (* (- (exp i) 1) n) i) (+ (* (* n i) 1/2) n) (* n i) 1/2 (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (- (pow (+ 1 (/ i n)) n) 1) (pow (+ 1 (/ i n)) n) 1 (/ i n) (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (/ (* (log (/ i n)) (* n n)) i) (* (log (/ i n)) (* n n)) (log (/ i n)) (* n n) (* 100 (* (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i) n)) (* (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i) n) (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i) (* n (/ (+ (* -1 (log n)) (log i)) i)) (/ (+ (* -1 (log n)) (log i)) i) (+ (* -1 (log n)) (log i)) -1 (log n) (log i))
81.0ms
i
@-inf
((* (* 100 (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i)) n) (* 100 (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i)) 100 (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i) (- (exp (* (log (+ 1 (/ i n))) n)) 1) (* (log (+ 1 (/ i n))) n) i n (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (/ (* (- (exp i) 1) n) i) (+ (* (* n i) 1/2) n) (* (* n i) 1/2) (* n i) 1/2 (* 100 (* (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i) n)) (* (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i) n) (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i) (+ (* (- 1/2 (/ 1/2 n)) i) 1) (- 1/2 (/ 1/2 n)) (/ 1/2 n) 1 (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (/ (* (* (log (/ i n)) n) n) i) (* (* (log (/ i n)) n) n) (* (log (/ i n)) n) (log (/ i n)) (/ i n) (* 100 (* (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i) n)) (* (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i) n) (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i) (* n (/ (+ (neg (log n)) (log i)) i)) (/ (+ (neg (log n)) (log i)) i) (+ (neg (log n)) (log i)) (neg (log n)) (log n) (log i))

prune4.2s (3.6%)

Memory
-626.0MiB live, 5 348.9MiB allocated; 1.7s collecting garbage
Counts
50 125 → 1 891
Compiler

Compiled 150 279 to 62 614 computations (58.3% saved)

analyze3.6s (3.1%)

Memory
202.1MiB live, 3 959.8MiB allocated; 1.5s collecting garbage
Algorithm
43×search
2×random
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%54.5%45.5%0%0%0%0
21.4%11.7%42.9%45.5%0%0%0%1
37.4%20.4%34.1%45.5%0%0%0%2
48.7%26.2%27.7%45.5%0%0.6%0%3
57.7%30.7%22.6%45.5%0%1.2%0%4
71.2%37.7%15.3%45.5%0%1.6%0%5
72.9%38.4%14.3%45.5%0%1.8%0%6
77.9%40.7%11.6%45.5%0%2.2%0%7
81.5%42.6%9.7%45.5%0%2.3%0%8
84.1%43.8%8.3%45.5%0%2.5%0%9
86.2%44.6%7.2%45.5%0%2.7%0%10
88.2%45.6%6.1%45.5%0%2.8%0%11
89.1%45.9%5.6%45.5%0%2.9%0%12
Compiler

Compiled 1 402 to 721 computations (48.6% saved)

derivations3.3s (2.8%)

Memory
-199.3MiB live, 2 795.1MiB allocated; 1.1s collecting garbage
Stop Event
12×done
11×fuel
Compiler

Compiled 3 597 to 878 computations (75.6% saved)

preprocess3.1s (2.6%)

Memory
-523.7MiB live, 2 813.8MiB allocated; 519ms collecting garbage
Stop Event
30×node-limit
10×saturated
Compiler

Compiled 13 108 to 5 752 computations (56.1% saved)

bsearch33.0ms (0%)

Memory
66.1MiB live, 66.1MiB allocated; 0ms collecting garbage
Algorithm
66×left-value
Compiler

Compiled 2 075 to 1 086 computations (47.7% saved)

start2.0ms (0%)

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

end0.0ms (0%)

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

Profiling

Loading profile data...