Herbie run

Date:Sunday, March 2nd, 2025
Commit:141e80a8 on main
Seed:2025061
Parameters:256 points for 4 iterations
Flags:
reduce:regimesreduce:binary-searchreduce:branch-expressionsreduce:simplifysetup:simplifysetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:simplifygenerate:proofs
default
Memory:171 385.5 MB

Time bar (total: 2.7min)

sample1.1min (41.5%)

Memory
581.2MiB live, 68 443.3MiB allocated; 27.3s collecting garbage
Samples
28.6s284 904×0valid
11.9s44 093×1valid
8.4s17 326×2valid
447.0ms4 305×0invalid
307.0ms429×3valid
197.0ms202×5exit
183.0ms970×0exit
Precisions
Click to see histograms. Total time spent on operations: 36.1s
ival-mult: 8.9s (24.6% of total)
ival-pow: 5.2s (14.3% of total)
adjust: 3.7s (10.3% of total)
ival-add: 3.6s (10.1% of total)
ival-div: 3.4s (9.6% of total)
ival-sub: 3.4s (9.4% of total)
ival-sin: 2.0s (5.6% of total)
ival-cos: 1.6s (4.3% of total)
const: 1.1s (3.2% of total)
ival-sqrt: 786.0ms (2.2% of total)
ival-neg: 536.0ms (1.5% of total)
ival-exp: 483.0ms (1.3% of total)
ival-pow2: 348.0ms (1% of total)
exact: 278.0ms (0.8% of total)
ival-expm1: 167.0ms (0.5% of total)
ival-assert: 114.0ms (0.3% of total)
ival-tan: 110.0ms (0.3% of total)
ival-log1p: 106.0ms (0.3% of total)
ival-atan: 75.0ms (0.2% of total)
ival-pi: 48.0ms (0.1% of total)
ival-hypot: 24.0ms (0.1% of total)
ival-<=: 12.0ms (0% of total)
ival-true: 11.0ms (0% of total)
ival-if: 9.0ms (0% of total)
ival-and: 9.0ms (0% of total)
ival-fabs: 8.0ms (0% of total)
ival-==: 4.0ms (0% of total)
ival-<: 1.0ms (0% of total)
Bogosity

rewrite29.3s (17.9%)

Memory
606.5MiB live, 29 997.1MiB allocated; 6.2s collecting garbage
Stop Event
372×iter limit
144×node limit
saturated
unsound
Counts
21 298 → 43 351

eval11.4s (7%)

Memory
19.9MiB live, 11 828.1MiB allocated; 6.2s collecting garbage
Compiler

Compiled 2 442 628 to 212 299 computations (91.3% saved)

preprocess10.6s (6.5%)

Memory
520.8MiB live, 10 269.1MiB allocated; 1.8s collecting garbage
Stop Event
84×iter limit
64×node limit
20×saturated
Compiler

Compiled 59 723 to 9 202 computations (84.6% saved)

explain9.5s (5.8%)

Memory
-14.8MiB live, 11 960.8MiB allocated; 2.1s collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
-.f64#fcancellation13203
+.f64#fcancellation36582
-.f64(-.f64 (*.f64 #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64) t) #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64))oflow-left2280
sqrt.f64#foflow-rescue2120
log.f64(log.f64 (+.f64 #s(literal 1 binary64) x))sensitivity1750
/.f64#fo/o1700
/.f64#fn/o1460
-.f64#fnan-rescue1160
pow.f64(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)sensitivity1041
/.f64#fu/n780
/.f64#fn/u600
/.f64#fu/u520
+.f64#fnan-rescue430
/.f64#fo/n370
*.f64#fn*u370
*.f64#fn*o260
pow.f64(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)oflow-rescue220
(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)overflow32
(/.f64 i n)overflow22
(+.f64 #s(literal 1 binary64) (/.f64 i n))overflow22
sqrt.f64#fuflow-rescue180
Confusion
Predicted +Predicted -
+3892245
-1266489
Precision
0.9686411149825784
Recall
0.9407783417935702
Confusion?
Predicted +Predicted MaybePredicted -
+389216679
-1261766313
Precision?
0.9307339449541284
Recall?
0.9809040367416002
Freqs
test
numberfreq
06734
13589
2392
337
Total Confusion?
Predicted +Predicted MaybePredicted -
+3110
-208
Precision?
0.9411764705882353
Recall?
1.0
Samples
1.5s16 270×0valid
1.2s3 754×1valid
657.0ms1 448×2valid
22.0ms32×3valid
Compiler

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

Precisions
Click to see histograms. Total time spent on operations: 2.4s
ival-mult: 614.0ms (25.7% of total)
adjust: 400.0ms (16.8% of total)
ival-add: 361.0ms (15.1% of total)
ival-sub: 239.0ms (10% of total)
ival-div: 212.0ms (8.9% of total)
ival-pow: 198.0ms (8.3% of total)
ival-cos: 79.0ms (3.3% of total)
ival-sin: 79.0ms (3.3% of total)
const: 51.0ms (2.1% of total)
ival-exp: 34.0ms (1.4% of total)
ival-sqrt: 21.0ms (0.9% of total)
ival-true: 19.0ms (0.8% of total)
exact: 19.0ms (0.8% of total)
ival-neg: 18.0ms (0.8% of total)
ival-pow2: 14.0ms (0.6% of total)
ival-assert: 9.0ms (0.4% of total)
ival-atan: 5.0ms (0.2% of total)
ival-log1p: 5.0ms (0.2% of total)
ival-tan: 4.0ms (0.2% of total)
ival-expm1: 3.0ms (0.1% of total)
ival-pi: 2.0ms (0.1% of total)

derivations8.6s (5.2%)

Memory
65.7MiB live, 6 990.2MiB allocated; 1.7s collecting garbage
Stop Event
29×fuel
13×done
Compiler

Compiled 26 782 to 2 809 computations (89.5% saved)

regimes6.1s (3.7%)

Memory
141.8MiB live, 7 868.2MiB allocated; 1.4s collecting garbage
Counts
4 769 → 602
Calls

96 calls:

675.0ms
x
388.0ms
a
335.0ms
b
243.0ms
(*.f64 (cos.f64 x) (exp.f64 (*.f64 #s(literal 10 binary64) (*.f64 x x))))
220.0ms
c
Compiler

Compiled 8 493 to 5 687 computations (33% saved)

series5.7s (3.5%)

Memory
-50.0MiB live, 6 836.2MiB allocated; 2.2s collecting garbage
Counts
3 551 → 17 747
Calls

894 calls:

TimeVariablePointExpression
397.0ms
c
@0
((/ (- (* b b) (+ (* (* c -4) a) (* b b))) (* (- (neg b) (sqrt (+ (* (* c -4) a) (* b b)))) (* 2 a))) (* (neg b) (+ (* (/ c (* b b)) -1) (pow a -1))) (neg b) b (+ (* (/ c (* b b)) -1) (pow a -1)) (/ c (* b b)) c (* b b) -1 (pow a -1) a (/ (+ (sqrt (+ (* (* -4 a) c) (* b b))) (neg b)) (+ a a)) (+ (sqrt (+ (* (* -4 a) c) (* b b))) (neg b)) (sqrt (+ (* (* -4 a) c) (* b b))) (+ a a) (/ (+ (sqrt (+ (* (* -4 a) c) (* b b))) (neg b)) (+ a a)) (+ (sqrt (+ (* (* -4 a) c) (* b b))) (neg b)) (sqrt (* (* a -4) c)) (* (* a -4) c) (* a -4) -4 (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (/ (+ (* (/ (* (* c c) a) (* b b)) -1) (neg c)) b) (+ (* (/ (* (* c c) a) (* b b)) -1) (neg c)) (* (- (neg (* a (/ c (* b b)))) 1) c) (- (neg (* a (/ c (* b b)))) 1) (neg (* a (/ c (* b b)))) (* a (/ c (* b b))) 1 (/ (- (* b b) (+ (* (* c -4) a) (* b b))) (* (- (neg b) (sqrt (+ (* (* c -4) a) (* b b)))) (* 2 a))) (- (* b b) (+ (* (* c -4) a) (* b b))) (* (* 4 a) c) (* 4 a) 4 (* (- (neg b) (sqrt (+ (* (* c -4) a) (* b b)))) (* 2 a)) (- (neg b) (sqrt (+ (* (* c -4) a) (* b b)))) (sqrt (+ (* (* c -4) a) (* b b))) (+ (* (* c -4) a) (* b b)) (* c -4) (* 2 a) 2)
125.0ms
a
@inf
((+ (* a (/ c (+ (* d d) (* c c)))) (* b (/ d (+ (* d d) (* c c))))) a (/ c (+ (* d d) (* c c))) c (+ (* d d) (* c c)) d (* c c) (* b (/ d (+ (* d d) (* c c)))) b (/ d (+ (* d d) (* c c))) (/ (+ (* a c) (* b d)) (+ (* c c) (* d d))) (/ a c) (/ (+ (* a c) (* b d)) (+ (* c c) (* d d))) (* a (/ c (+ (* d d) (* c c)))) (/ (+ (* a c) (* b d)) (+ (* c c) (* d d))) (/ (+ (* a (/ c d)) b) d) (+ (* a (/ c d)) b) (/ c d) (/ (+ (* a c) (* b d)) (+ (* c c) (* d d))) (+ (* a c) (* b d)) (* d b) (+ (* c c) (* d d)) (* d d))
105.0ms
n
@-inf
((* (/ (* (- (exp (* (log (+ 1 (/ i n))) n)) 1) 100) i) n) (/ (* (- (exp (* (log (+ 1 (/ i n))) n)) 1) 100) i) (* (- (exp (* (log (+ 1 (/ i n))) n)) 1) 100) (- (exp (* (log (+ 1 (/ i n))) n)) 1) (* (log (+ 1 (/ i n))) n) (log (+ 1 (/ i n))) (/ i n) i n 100 (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (- (pow (+ 1 (/ i n)) n) 1) (* (+ (* (- 1/2 (/ 1/2 n)) i) 1) i) (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (- (pow (+ 1 (/ i n)) n) 1) (* (+ (* (- 1/2 (/ 1/2 n)) i) 1) i) (+ (* (- 1/2 (/ 1/2 n)) i) 1) (* -1/2 (/ i n)) -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) (* (/ (- (* (* (- 1/2 (/ 1/2 n)) i) (* (- 1/2 (/ 1/2 n)) i)) 1) (- (* (- 1/2 (/ 1/2 n)) i) 1)) i) (/ (- (* (* (- 1/2 (/ 1/2 n)) i) (* (- 1/2 (/ 1/2 n)) i)) 1) (- (* (- 1/2 (/ 1/2 n)) i) 1)) (- (* (* (- 1/2 (/ 1/2 n)) i) (* (- 1/2 (/ 1/2 n)) i)) 1) (* (* (- 1/2 (/ 1/2 n)) i) (* (- 1/2 (/ 1/2 n)) i)) (* (- 1/2 (/ 1/2 n)) i) (- 1/2 (/ 1/2 n)) 1/2 (/ 1/2 n) 1 (- (* (- 1/2 (/ 1/2 n)) i) 1) (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (- (pow (+ 1 (/ i n)) n) 1) (* (log (/ i n)) n) (log (/ i n)))
89.0ms
n
@0
((/ (* 100 (- (exp (* (log (+ 1 (/ i n))) n)) 1)) (/ i n)) (* 100 (- (exp (* (log (+ 1 (/ i n))) n)) 1)) 100 (- (exp (* (log (+ 1 (/ i n))) n)) 1) (* (log (+ 1 (/ i n))) n) (log (+ 1 (/ i n))) (/ i n) i n (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (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)) (- (pow (+ 1 (/ i n)) n) 1) (* (+ (* (- 1/2 (/ 1/2 n)) i) 1) i) (+ (* (- 1/2 (/ 1/2 n)) i) 1) (- 1/2 (/ 1/2 n)) 1/2 (/ 1/2 n) 1 (* 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)) (- (pow (+ 1 (/ i n)) n) 1) (* (- (log i) (log n)) n) (- (log i) (log n)) (log i) (log n))
72.0ms
x
@inf
((* (cos x) (exp (* 10 (* x x)))) (cos x) x (exp (* 10 (* x x))) (* 10 (* x x)) 10 (* x x))

analyze5.0s (3%)

Memory
73.1MiB live, 4 406.4MiB allocated; 1.8s collecting garbage
Algorithm
43×search
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)

prune4.3s (2.6%)

Memory
-261.6MiB live, 6 639.9MiB allocated; 1.0s collecting garbage
Counts
51 382 → 2 015
Compiler

Compiled 156 428 to 67 468 computations (56.9% saved)

bsearch3.1s (1.9%)

Memory
-12.6MiB live, 4 026.7MiB allocated; 705ms collecting garbage
Algorithm
193×binary-search
113×left-value
Stop Event
182×narrow-enough
10×predicate-same
predicate-failed
Samples
1.2s11 236×0valid
337.0ms1 000×1valid
225.0ms312×2valid
89.0ms1 193×0invalid
31.0ms189×0exit
11.0ms12×3valid
Compiler

Compiled 122 151 to 71 086 computations (41.8% saved)

Precisions
Click to see histograms. Total time spent on operations: 1.3s
ival-mult: 400.0ms (30.8% of total)
ival-pow: 214.0ms (16.5% of total)
ival-div: 156.0ms (12% of total)
ival-sub: 142.0ms (10.9% of total)
ival-add: 106.0ms (8.2% of total)
adjust: 70.0ms (5.4% of total)
ival-sqrt: 68.0ms (5.2% of total)
ival-exp: 60.0ms (4.6% of total)
ival-neg: 50.0ms (3.9% of total)
ival-true: 10.0ms (0.8% of total)
exact: 9.0ms (0.7% of total)
ival-assert: 6.0ms (0.5% of total)
const: 4.0ms (0.3% of total)
ival-expm1: 3.0ms (0.2% of total)
ival-pi: 1.0ms (0.1% of total)

simplify2.2s (1.4%)

Memory
-192.3MiB live, 2 113.0MiB allocated; 393ms collecting garbage
Stop Event
34×node limit
saturated

start59.0ms (0%)

Memory
-36.2MiB live, 5.8MiB allocated; 16ms collecting garbage

end0.0ms (0%)

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

Profiling

Loading profile data...