Herbie run

Date:Sunday, January 26th, 2025
Commit:c73a45c1 on main
Seed:2025026
Parameters:256 points for 4 iterations
Flags:
localize:costslocalize:errorsreduce:regimesreduce:binary-searchreduce:branch-expressionssetup:simplifysetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:simplifygenerate:proofs
default
Memory:246 847.6 MB

Time bar (total: 3.9min)

sample1.2min (30.6%)

Memory
861.2MiB live, 79 252.9MiB allocated; 23.7s collecting garbage
Samples
30.9s284 608×0valid
14.6s44 143×1valid
7.8s17 585×2valid
501.0ms4 088×0invalid
224.0ms416×3valid
218.0ms202×5exit
164.0ms962×0exit
Precisions
Click to see histograms. Total time spent on operations: 39.6s
ival-mult: 9.9s (25% of total)
ival-add: 5.1s (12.8% of total)
ival-pow: 5.0s (12.5% of total)
adjust: 4.8s (12% of total)
ival-div: 3.8s (9.5% of total)
ival-sub: 2.8s (7.2% of total)
ival-sin: 1.8s (4.6% of total)
ival-cos: 1.6s (4.1% of total)
const: 1.4s (3.5% of total)
ival-pow2: 1.3s (3.2% of total)
ival-exp: 514.0ms (1.3% of total)
ival-sqrt: 494.0ms (1.2% of total)
ival-neg: 411.0ms (1% of total)
exact: 269.0ms (0.7% of total)
ival-assert: 119.0ms (0.3% of total)
ival-atan: 94.0ms (0.2% of total)
ival-expm1: 84.0ms (0.2% of total)
ival-log1p: 79.0ms (0.2% of total)
ival-tan: 61.0ms (0.2% of total)
ival-pi: 41.0ms (0.1% of total)
ival-hypot: 25.0ms (0.1% of total)
ival-fabs: 17.0ms (0% of total)
ival-<=: 11.0ms (0% of total)
ival-true: 9.0ms (0% of total)
ival-and: 9.0ms (0% of total)
ival-if: 6.0ms (0% of total)
ival-==: 3.0ms (0% of total)
ival-<: 1.0ms (0% of total)
Bogosity

simplify57.1s (24.4%)

Memory
238.1MiB live, 53 602.4MiB allocated; 13.5s collecting garbage
Stop Event
427×iter limit
303×node limit
42×saturated
Counts
13 570 → 13 570

localize24.4s (10.4%)

Memory
166.3MiB live, 24 743.4MiB allocated; 7.1s collecting garbage
Samples
8.2s3 430×2valid
6.9s28 000×0valid
3.9s5 319×1valid
240.0ms164×3valid
98.0ms289×0invalid
55.0ms159×0exit
46.0ms13×5exit
8.0ms2×4valid
Compiler

Compiled 34 155 to 3 931 computations (88.5% saved)

Precisions
Click to see histograms. Total time spent on operations: 14.5s
ival-mult: 3.0s (20.6% of total)
adjust: 2.9s (19.8% of total)
ival-sin: 2.2s (15% of total)
ival-add: 2.0s (13.5% of total)
ival-div: 1.4s (9.6% of total)
ival-pow: 737.0ms (5.1% of total)
ival-sub: 701.0ms (4.8% of total)
const: 543.0ms (3.7% of total)
ival-cos: 382.0ms (2.6% of total)
ival-tan: 253.0ms (1.7% of total)
ival-exp: 102.0ms (0.7% of total)
ival-neg: 98.0ms (0.7% of total)
ival-sqrt: 75.0ms (0.5% of total)
exact: 55.0ms (0.4% of total)
ival-pow2: 49.0ms (0.3% of total)
ival-true: 30.0ms (0.2% of total)
ival-expm1: 26.0ms (0.2% of total)
ival-pi: 17.0ms (0.1% of total)
ival-assert: 15.0ms (0.1% of total)
ival-log1p: 12.0ms (0.1% of total)
ival-log: 11.0ms (0.1% of total)
ival-atan: 4.0ms (0% of total)

rewrite15.6s (6.7%)

Memory
-63.1MiB live, 16 378.5MiB allocated; 2.7s collecting garbage
Stop Event
428×iter limit
117×node limit
26×unsound
12×saturated
Counts
1 949 → 31 076

derivations13.4s (5.7%)

Memory
-218.1MiB live, 9 514.8MiB allocated; 1.6s collecting garbage
Stop Event
22×fuel
20×done
Compiler

Compiled 30 645 to 2 748 computations (91% saved)

explain11.0s (4.7%)

Memory
-146.1MiB live, 13 268.9MiB allocated; 2.7s collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
-.f64#fcancellation12962
+.f64#fcancellation37082
sqrt.f64#foflow-rescue2340
-.f64(-.f64 (*.f64 #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64) t) #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64))oflow-left2170
log.f64(log.f64 (+.f64 #s(literal 1 binary64) x))sensitivity1681
/.f64#fn/o1530
/.f64#fo/o1530
-.f64#fnan-rescue1160
pow.f64(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)sensitivity1141
/.f64#fu/n1100
/.f64#fn/u580
/.f64#fu/u580
+.f64#fnan-rescue440
/.f64#fo/n440
*.f64#fn*u440
*.f64#fn*o290
pow.f64(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)oflow-rescue200
↳(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)overflow25
↳(/.f64 i n)overflow20
↳(+.f64 #s(literal 1 binary64) (/.f64 i n))overflow20
sqrt.f64#fuflow-rescue120
exp.f64#fsensitivity20
Confusion
Predicted +Predicted -
+3873234
-1406505
Precision
0.9651133815100922
Recall
0.9430241051862673
Confusion?
Predicted +Predicted MaybePredicted -
+387316272
-1401796326
Precision?
0.9267340376665135
Recall?
0.9824689554419284
Freqs
test
numberfreq
06739
13560
2402
351
Total Confusion?
Predicted +Predicted MaybePredicted -
+3110
-208
Precision?
0.9411764705882353
Recall?
1.0
Samples
1.9s3 700×1valid
1.8s16 274×0valid
602.0ms1 484×2valid
48.0ms46×3valid
Compiler

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

Precisions
Click to see histograms. Total time spent on operations: 3.1s
ival-mult: 664.0ms (21.7% of total)
adjust: 520.0ms (17% of total)
ival-exp: 414.0ms (13.5% of total)
ival-div: 280.0ms (9.2% of total)
ival-sub: 273.0ms (8.9% of total)
ival-add: 268.0ms (8.8% of total)
ival-pow: 245.0ms (8% of total)
ival-sin: 129.0ms (4.2% of total)
ival-cos: 69.0ms (2.3% of total)
const: 40.0ms (1.3% of total)
ival-sqrt: 27.0ms (0.9% of total)
ival-expm1: 27.0ms (0.9% of total)
ival-neg: 20.0ms (0.7% of total)
ival-pow2: 19.0ms (0.6% of total)
ival-true: 19.0ms (0.6% of total)
exact: 18.0ms (0.6% of total)
ival-assert: 9.0ms (0.3% of total)
ival-atan: 6.0ms (0.2% of total)
ival-log1p: 6.0ms (0.2% of total)
ival-tan: 4.0ms (0.1% of total)
ival-pi: 2.0ms (0.1% of total)

preprocess10.6s (4.5%)

Memory
459.3MiB live, 10 639.2MiB allocated; 1.9s collecting garbage
Stop Event
84×iter limit
64×node limit
20×saturated
Compiler

Compiled 68 909 to 9 782 computations (85.8% saved)

eval8.4s (3.6%)

Memory
187.8MiB live, 11 439.6MiB allocated; 2.0s collecting garbage
Compiler

Compiled 2 108 356 to 185 761 computations (91.2% saved)

regimes6.1s (2.6%)

Memory
-25.6MiB live, 8 140.4MiB allocated; 1.0s collecting garbage
Counts
4 902 → 620
Calls

96 calls:

787.0ms
x
268.0ms
b
268.0ms
(*.f64 (cos.f64 x) (exp.f64 (*.f64 #s(literal 10 binary64) (*.f64 x x))))
263.0ms
d
219.0ms
(/.f64 (/.f64 #s(literal 2 binary64) t) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) t)))
Compiler

Compiled 9 300 to 5 975 computations (35.8% saved)

series4.4s (1.9%)

Memory
-105.7MiB live, 5 179.5MiB allocated; 1.2s collecting garbage
Counts
1 949 → 13 570
Calls

867 calls:

TimeVariablePointExpression
113.0ms
x
@0
((+ (* x x) (pow x 3)) (pow x 3) (+ (* x (* x x)) (* x x)) (* x x) (* (+ (* x x) x) x) (+ (* x x) x) (* (+ 1 x) (* x x)) (+ 1 x) (+ (* (* x x) x) (* x x)))
96.0ms
i
@-inf
((* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (* (* (/ (- (exp i) 1) i) 100) n) (* (/ (- (exp i) 1) i) 100) (/ (- (exp i) 1) i) (* 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) (pow (+ 1 (/ i n)) n) (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (- (pow (+ 1 (/ i n)) n) 1) (+ (* (* i i) (+ (* (- (+ (/ 1/3 (* n n)) 1/6) (/ 1/2 n)) i) (- 1/2 (/ 1/2 n)))) i) (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (* (* n n) (/ (- (log i) (log n)) i)) (* n n) (/ 1/3 (* n n)) (- (log i) (log n)) (/ (- (log i) (log n)) i))
76.0ms
x
@inf
((/ x (+ (* x x) 1)) (+ (* x x) 1) (/ x (+ (* x x) 1)) (/ x (+ (* x x) 1)) (/ 1 x) (/ x (+ (* x x) 1)) (- x (pow x 3)) (pow x 3) (exp (* (log x) 2)) (+ (exp (* (log x) 2)) 1) (/ x (+ (exp (* (log x) 2)) 1)) (* (log x) 2) (log x))
75.0ms
i
@-inf
((/ (* (- (exp (* (log (+ 1 (/ i n))) n)) 1) 100) (/ i n)) (* (- (exp (* (log (+ 1 (/ i n))) n)) 1) 100) (- (exp (* (log (+ 1 (/ i n))) n)) 1) (* (log (+ 1 (/ i n))) n) (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (* (* (/ (- (exp i) 1) i) 100) n) (* (/ (- (exp i) 1) i) 100) (+ (* 50 i) 100) (* 100 (/ (* (- (pow (+ 1 (/ i n)) n) 1) n) i)) (/ (* (- (pow (+ 1 (/ i n)) n) 1) n) i) (* (- (pow (+ 1 (/ i n)) n) 1) n) (- (pow (+ 1 (/ i n)) n) 1) (/ (* (* (neg n) (- (pow (+ 1 (/ i n)) n) 1)) 100) (neg i)) (* (* (neg n) (- (pow (+ 1 (/ i n)) n) 1)) 100) (* (neg n) (- (pow (+ 1 (/ i n)) n) 1)) (neg n) (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (* (* (/ (log (/ i n)) i) n) n) (* (/ (log (/ i n)) i) n) (log (+ 1 (/ i n))) (pow (+ 1 (/ i n)) n) (- (pow (+ 1 (/ i n)) n) 1) (pow (+ 1 (/ i n)) n) (log (/ i n)) (/ (log (/ i n)) i))
63.0ms
w
@inf
((- (- (+ 3 (/ 2 (* r r))) (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (- 1 v))) 9/2) (* 1/8 (- 3 (* 2 v))) (- (+ 3 (/ 2 (* r r))) (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (- 1 v))) (- 3 (* 2 v)) (* (* w w) r) (* (* (* w w) r) r) (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (- 1 v)) (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)))

analyze4.3s (1.8%)

Memory
27.4MiB live, 4 943.0MiB allocated; 937ms 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)

prune4.1s (1.8%)

Memory
97.4MiB live, 6 160.2MiB allocated; 887ms collecting garbage
Counts
46 723 → 1 855
Compiler

Compiled 142 174 to 60 561 computations (57.4% saved)

bsearch3.1s (1.3%)

Memory
44.3MiB live, 3 578.8MiB allocated; 510ms collecting garbage
Algorithm
226×binary-search
88×left-value
Stop Event
221×narrow-enough
4×predicate-same
1×predicate-failed
Samples
1.2s12 858×0valid
213.0ms634×1valid
154.0ms294×2valid
77.0ms668×0invalid
22.0ms194×0exit
14.0ms22×3valid
Compiler

Compiled 139 485 to 79 110 computations (43.3% saved)

Precisions
Click to see histograms. Total time spent on operations: 1.1s
ival-mult: 384.0ms (34.2% of total)
ival-sub: 147.0ms (13.1% of total)
ival-div: 133.0ms (11.8% of total)
ival-pow: 127.0ms (11.3% of total)
ival-add: 103.0ms (9.2% of total)
ival-exp: 77.0ms (6.9% of total)
adjust: 60.0ms (5.3% of total)
ival-neg: 36.0ms (3.2% of total)
ival-sqrt: 21.0ms (1.9% of total)
ival-true: 11.0ms (1% of total)
exact: 9.0ms (0.8% of total)
ival-assert: 6.0ms (0.5% of total)
ival-expm1: 5.0ms (0.4% of total)
const: 3.0ms (0.3% of total)
ival-pi: 1.0ms (0.1% of total)

start19.0ms (0%)

Memory
-50.3MiB live, 5.3MiB allocated; 23ms collecting garbage

end0.0ms (0%)

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

Profiling

Loading profile data...