Herbie run

Date:Wednesday, April 9th, 2025
Commit:5cea69ef on main
Seed:2025099
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:159 620.0 MB

Time bar (total: 2.1min)

sample48.1s (37.4%)

Memory
508.2MiB live, 59 584.5MiB allocated; 17.6s collecting garbage
Samples
19.9s293 006×0valid
7.6s17 746×2valid
6.5s35 563×1valid
459.0ms4 456×0invalid
193.0ms437×3valid
148.0ms961×0exit
52.0ms101×4exit
45.0ms101×3exit
6.0ms52×1exit
Precisions
Click to see histograms. Total time spent on operations: 22.9s
ival-mult!: 5.1s (22.3% of total)
ival-pow: 3.3s (14.2% of total)
adjust: 3.0s (13% of total)
ival-div!: 2.4s (10.6% of total)
ival-add!: 2.1s (9% of total)
ival-cos: 1.9s (8.2% of total)
ival-sin: 1.7s (7.6% of total)
ival-sub!: 1.3s (5.7% of total)
ival-sqrt: 517.0ms (2.3% of total)
ival-exp: 480.0ms (2.1% of total)
ival-pow2: 358.0ms (1.6% of total)
ival-neg: 356.0ms (1.6% of total)
ival-log1p: 141.0ms (0.6% of total)
ival-atan: 97.0ms (0.4% of total)
ival-expm1: 75.0ms (0.3% of total)
ival-tan: 69.0ms (0.3% of total)
ival-<=: 30.0ms (0.1% of total)
ival-hypot: 16.0ms (0.1% of total)
ival-and: 8.0ms (0% of total)
ival-fabs: 6.0ms (0% of total)
ival-if: 4.0ms (0% of total)
ival-==: 2.0ms (0% of total)
ival-assert: 1.0ms (0% of total)
ival-pi: 0.0ms (0% of total)
const: 0.0ms (0% of total)
ival-<: 0.0ms (0% of total)
Bogosity

rewrite30.1s (23.4%)

Memory
583.9MiB live, 32 214.5MiB allocated; 8.6s collecting garbage
Stop Event
365×iter-limit
141×node-limit
9×saturated
6×unsound
Counts
20 332 → 41 198

explain8.3s (6.4%)

Memory
69.5MiB live, 13 051.2MiB allocated; 2.0s collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
-.f64#fcancellation12714
+.f64#fcancellation36582
-.f64(-.f64 (*.f64 #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64) t) #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64))oflow-left2280
sqrt.f64#foflow-rescue1820
/.f64#fo/o1800
log.f64(log.f64 (+.f64 #s(literal 1 binary64) x))sensitivity1651
/.f64#fn/o1580
-.f64#fnan-rescue1170
pow.f64(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)sensitivity1050
/.f64#fu/n760
/.f64#fo/n500
/.f64#fn/u490
*.f64#fn*u490
+.f64#fnan-rescue480
/.f64#fu/u450
pow.f64(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)oflow-rescue230
↳(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)overflow34
↳(/.f64 i n)overflow23
↳(+.f64 #s(literal 1 binary64) (/.f64 i n))overflow23
*.f64#fn*o200
sqrt.f64#fuflow-rescue140
Confusion
Predicted +Predicted -
+3841234
-1246553
Precision
0.9687263556116015
Recall
0.9425766871165644
Confusion?
Predicted +Predicted MaybePredicted -
+384115975
-1241846369
Precision?
0.9285051067780873
Recall?
0.9815950920245399
Freqs
test
numberfreq
06787
13549
2377
339
Total Confusion?
Predicted +Predicted MaybePredicted -
+3010
-209
Precision?
0.9393939393939394
Recall?
1.0
Samples
1.3s16 854×0valid
695.0ms3 176×1valid
544.0ms1 416×2valid
54.0ms56×3valid
2.0ms2×4valid
Compiler

Compiled 7 535 to 1 486 computations (80.3% saved)

Precisions
Click to see histograms. Total time spent on operations: 1.6s
ival-mult!: 396.0ms (24.6% of total)
adjust: 296.0ms (18.4% of total)
ival-pow: 228.0ms (14.2% of total)
ival-add!: 171.0ms (10.6% of total)
ival-div!: 139.0ms (8.7% of total)
ival-sub!: 105.0ms (6.5% of total)
ival-sin: 96.0ms (6% of total)
ival-cos: 65.0ms (4% of total)
ival-pow2: 27.0ms (1.7% of total)
ival-exp: 26.0ms (1.6% of total)
ival-sqrt: 23.0ms (1.4% of total)
ival-neg: 18.0ms (1.1% 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)

eval8.1s (6.3%)

Memory
44.7MiB live, 12 282.1MiB allocated; 3.0s collecting garbage
Compiler

Compiled 2 365 215 to 202 429 computations (91.4% saved)

derivations7.5s (5.8%)

Memory
-252.5MiB live, 7 789.1MiB allocated; 1.4s collecting garbage
Stop Event
26×fuel
16×done
Compiler

Compiled 23 716 to 2 600 computations (89% saved)

regimes6.8s (5.3%)

Memory
228.2MiB live, 9 233.9MiB allocated; 2.4s collecting garbage
Counts
4 840 → 543
Calls

96 calls:

741.0ms
(*.f64 (cos.f64 x) (exp.f64 (*.f64 #s(literal 10 binary64) (*.f64 x x))))
587.0ms
x
396.0ms
b
279.0ms
(-.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) (+.f64 #s(literal 2 binary64) (*.f64 (-.f64 #s(literal 2 binary64) (/.f64 (/.f64 #s(literal 2 binary64) t) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) t)))) (-.f64 #s(literal 2 binary64) (/.f64 (/.f64 #s(literal 2 binary64) t) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) t))))))))
222.0ms
a
Compiler

Compiled 9 134 to 5 798 computations (36.5% saved)

series4.6s (3.6%)

Memory
754.1MiB live, 6 422.5MiB allocated; 1.8s collecting garbage
Counts
3 359 → 16 973
Calls

888 calls:

TimeVariablePointExpression
506.0ms
c
@-inf
((* (+ a (+ b (+ c d))) 2) (* 2 (+ b (+ (+ d c) a))) 2 (+ b (+ (+ d c) a)) b (+ (+ d c) a) (* c (+ 1 (/ (+ a d) c))) c (+ 1 (/ (+ a d) c)) 1 (/ (+ a d) c) (+ a d) a d (* (- (/ (* 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 (+ (+ c b) d)) 2) (+ a (+ (+ c b) d)) (+ (+ c b) d) (+ c b) (* (+ a (+ b (+ c d))) 2) (* (+ (* (/ (+ (+ d c) b) a) 2) 2) a) (+ (* (/ (+ (+ d c) b) a) 2) 2) (/ (+ (+ d c) b) a) (+ (+ d c) b) (+ d c) (* (+ a (+ b (+ c d))) 2) (* (+ (* (/ (+ (+ d c) a) b) 2) 2) b) (+ (* (/ (+ (+ d c) a) b) 2) 2) (+ 2 (+ (* 2 (/ c b)) (* 2 (/ (+ a d) b)))) (+ (* 2 (/ c b)) (* 2 (/ (+ a d) b))) (/ c b) (* 2 (/ (+ a d) b)) (/ (+ a d) b))
114.0ms
a
@inf
((* (/ (PI) (* 2 (+ a b))) (* (pow (- b a) -1) (- (pow a -1) (pow b -1)))) (/ (PI) (* 2 (+ a b))) (PI) (* 2 (+ a b)) 2 (+ a b) a b (* (pow (- b a) -1) (- (pow a -1) (pow b -1))) (pow (* b a) -1) (* b a) -1 (* (* (/ (/ (PI) 2) (+ b a)) (/ 1 (- b a))) (- (/ 1 a) (/ 1 b))) (* (/ (PI) (* (* b b) a)) 1/2) (/ (PI) (* (* b b) a)) (* (* b b) a) (* b b) 1/2 (* (* (/ (PI) 2) (/ 1 (- (* b b) (* a a)))) (- (/ 1 a) (/ 1 b))) (/ (/ (+ (* (/ (PI) b) 1/2) (* (/ (PI) a) -1/2)) a) a) (/ (+ (* (/ (PI) b) 1/2) (* (/ (PI) a) -1/2)) a) (+ (* (/ (PI) b) 1/2) (* (/ (PI) a) -1/2)) (* (/ (PI) b) 1/2) (/ (PI) b) (* (/ (* (PI) 1) (* 2 (- (* b b) (* a a)))) (- (/ 1 a) (/ 1 b))) (/ (* (PI) 1) (* 2 (- (* b b) (* a a)))) (* (PI) 1) 1 (* 2 (- (* b b) (* a a))) (- (* b b) (* a a)) (- (/ 1 a) (/ 1 b)) (/ (- (/ b a) 1) b) (- (/ b a) 1) (/ b a) (* (/ (* (PI) 1) (* 2 (* (+ b a) (- b a)))) (- (/ 1 a) (/ 1 b))) (/ (* (PI) 1) (* 2 (* (+ b a) (- b a)))) (* 2 (* (+ b a) (- b a))) (* (+ b a) (- b a)) (+ b a) (- b a) (- (/ 1 a) (/ 1 b)) (/ 1 a) (/ 1 b))
112.0ms
eps
@-inf
((- (pow (+ x eps) 5) (pow x 5)) (* (+ (* 5 (/ x eps)) 1) (pow eps 5)) (+ (* 5 (/ x eps)) 1) 5 (/ x eps) x eps 1 (pow eps 5) (- (pow (+ x eps) 5) (pow x 5)) (- (pow (+ x eps) 5) (pow x 5)) (* (* 5 eps) (pow x 4)) (* 5 eps) (pow x 4) 4 (- (pow (+ x eps) 5) (pow x 5)) (* (* 5 (pow x 4)) eps) (* 5 (pow x 4)) (- (pow (+ x eps) 5) (pow x 5)) (* (+ (+ (* 4 eps) (neg (/ (+ (* -4 (* eps eps)) (neg (* (* eps eps) 6))) x))) eps) (pow x 4)) (+ (+ (* 4 eps) (neg (/ (+ (* -4 (* eps eps)) (neg (* (* eps eps) 6))) x))) eps) (+ (* 4 eps) (neg (/ (+ (* -4 (* eps eps)) (neg (* (* eps eps) 6))) x))) (neg (/ (+ (* -4 (* eps eps)) (neg (* (* eps eps) 6))) x)) (/ (+ (* -4 (* eps eps)) (neg (* (* eps eps) 6))) x) (+ (* -4 (* eps eps)) (neg (* (* eps eps) 6))) -4 (* eps eps) (neg (* (* eps eps) 6)) (* (* eps eps) 6) 6)
110.0ms
y
@0
((/ (+ (* x x) (* (neg y) y)) (+ (* y y) (* x x))) (+ (* x x) (* (neg y) y)) x (* (neg y) y) (neg y) y (+ (* y y) (* x x)) (* x x) (/ (* (- x y) (+ x y)) (+ (* y y) (* x x))) (+ (* (/ (* y y) (* x x)) -2) 1) (/ (* y y) (* x x)) (* y y) -2 1 (/ (* (- x y) (+ x y)) (+ (* y y) (* x x))) (- (/ (* 2 (* x x)) (* y y)) 1) (/ (* 2 (* x x)) (* y y)) (* 2 (* x x)) 2 (/ (* (+ y x) (* (+ y x) (- x y))) (* (+ y x) (+ (* y y) (* x x)))) (* (+ y x) (* (+ y x) (- x y))) (+ y x) (* (+ y x) (- x y)) (- x y) (* (+ y x) (+ (* y y) (* x x))) (/ (* (- (* x x) (* y y)) (+ y x)) (* (+ y x) (+ (* y y) (* x x)))) (* (- (* x x) (* y y)) (+ y x)) (- (* x x) (* y y)) (* (- (/ (* x x) (* y y)) 1) (* y y)) (- (/ (* x x) (* y y)) 1) (/ (* x x) (* y y)))
94.0ms
x
@inf
((* (sin (+ x (/ (PI) 2))) (pow (pow (exp 10) (neg x)) (neg x))) (sin (+ x (/ (PI) 2))) (+ x (/ (PI) 2)) x (/ (PI) 2) (PI) 2 (pow (pow (exp 10) (neg x)) (neg x)) (pow (exp 10) (neg x)) (exp 10) 10 (neg x) (* (cos x) (pow (pow (exp 10) x) x)) (cos x) (pow (pow (exp 10) x) x) 1 (* (cos x) (exp (* 10 (* x x)))) (cos x) (+ (* (- (* (* (+ (* -1/720 (* x x)) 1/24) x) x) 1/2) (* x x)) 1) (- (* (* (+ (* -1/720 (* x x)) 1/24) x) x) 1/2) (* (* (+ (* -1/720 (* x x)) 1/24) x) x) (* (+ (* -1/720 (* x x)) 1/24) x) (+ (* -1/720 (* x x)) 1/24) -1/720 (* x x) 1/24 1/2 (exp (* 10 (* x x))) (* 10 (* x x)) (* (cos x) (/ 1 (pow (exp 10) (* (neg x) x)))) (/ 1 (pow (exp 10) (* (neg x) x))) (pow (exp 10) (* (neg x) x)) (* (neg x) x) (* (cos x) (pow (pow (pow (exp 10) (neg x)) -1) x)) (pow (pow (pow (exp 10) (neg x)) -1) x) (pow (pow (exp 10) (neg x)) -1) -1)

prune4.6s (3.6%)

Memory
-475.5MiB live, 5 952.9MiB allocated; 2.3s collecting garbage
Counts
49 720 → 1 936
Compiler

Compiled 149 995 to 64 915 computations (56.7% saved)

preprocess4.6s (3.6%)

Memory
-506.7MiB live, 5 056.7MiB allocated; 871ms collecting garbage
Stop Event
32×node-limit
10×saturated
Compiler

Compiled 66 794 to 15 274 computations (77.1% saved)

analyze3.5s (2.7%)

Memory
-30.0MiB live, 4 286.4MiB allocated; 1.2s 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)

bsearch2.6s (2%)

Memory
116.2MiB live, 3 739.6MiB allocated; 582ms collecting garbage
Algorithm
163×binary-search
96×left-value
Stop Event
153×narrow-enough
9×predicate-same
1×predicate-failed
Samples
875.0ms10 671×0valid
261.0ms1 242×1valid
192.0ms442×2valid
71.0ms1 330×0invalid
12.0ms13×3valid
3.0ms39×0exit
0.0ms2×1exit
Compiler

Compiled 114 461 to 65 295 computations (43% saved)

Precisions
Click to see histograms. Total time spent on operations: 906.0ms
ival-mult!: 266.0ms (29.4% of total)
ival-pow: 229.0ms (25.3% of total)
ival-div!: 109.0ms (12% of total)
ival-sub!: 75.0ms (8.3% of total)
adjust: 57.0ms (6.3% of total)
ival-add!: 57.0ms (6.3% of total)
ival-neg: 46.0ms (5.1% of total)
ival-exp: 38.0ms (4.2% of total)
ival-sqrt: 24.0ms (2.6% of total)
ival-expm1: 3.0ms (0.3% of total)

start2.0ms (0%)

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

end0.0ms (0%)

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

Profiling

Loading profile data...