Herbie run

Date:Sunday, December 8th, 2024
Commit:393f01df on no-soundiness
Hostname:nightly with Racket 8.10
Seed:2024343
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:280 224.1 MB

Time bar (total: 4.4min)

sample1.3min (28.6%)

Memory
454.1MiB live, 84 448.2MiB allocated
Samples
34.5s285 545×0valid
13.2s43 980×1valid
7.3s16 845×2valid
655.0ms4 152×0invalid
169.0ms1 000×0exit
142.0ms382×3valid
97.0ms101×3exit
58.0ms101×4exit
6.0ms44×1exit
Precisions
Click to see histograms. Total time spent on operations: 41.5s
ival-mult: 8.9s (21.3% of total)
ival-add: 5.5s (13.3% of total)
ival-div: 4.2s (10.2% of total)
ival-sub: 3.8s (9.1% of total)
const: 3.3s (8% of total)
ival-pow: 3.2s (7.7% of total)
adjust: 2.8s (6.7% of total)
ival-sin: 2.3s (5.4% of total)
ival-<=: 2.0s (4.8% of total)
ival-cos: 1.7s (4.1% of total)
ival-sqrt: 570.0ms (1.4% of total)
ival-exp: 540.0ms (1.3% of total)
ival-neg: 525.0ms (1.3% of total)
exact: 455.0ms (1.1% of total)
ival-and: 397.0ms (1% of total)
ival-==: 316.0ms (0.8% of total)
ival-pow2: 306.0ms (0.7% of total)
ival-true: 146.0ms (0.4% of total)
ival-assert: 144.0ms (0.3% of total)
ival-tan: 90.0ms (0.2% of total)
ival-atan: 79.0ms (0.2% of total)
ival-pi: 78.0ms (0.2% of total)
ival-log1p: 78.0ms (0.2% of total)
ival-expm1: 69.0ms (0.2% of total)
ival-<: 64.0ms (0.2% of total)
ival-hypot: 17.0ms (0% of total)
ival-fabs: 4.0ms (0% of total)
ival-if: 4.0ms (0% of total)
Bogosity

simplify48.6s (18.2%)

Memory
500.6MiB live, 45 957.9MiB allocated
Algorithm
342×egg-herbie
Stop Event
439×iter limit
261×node limit
93×saturated
Counts
9 828 → 9 697

rewrite34.6s (13%)

Memory
179.3MiB live, 34 865.6MiB allocated
Stop Event
301×iter limit
145×node limit
11×saturated
1×unsound
Counts
2 005 → 63 308

derivations30.8s (11.5%)

Memory
-194.7MiB live, 21 157.7MiB allocated
Stop Event
267×iter limit
174×node limit
27×fuel
15×done
6×saturated
Compiler

Compiled 28 118 to 2 646 computations (90.6% saved)

localize18.4s (6.9%)

Memory
-101.4MiB live, 22 178.2MiB allocated
Samples
7.8s29 854×0valid
3.5s5 068×1valid
2.5s2 555×2valid
220.0ms596×0invalid
83.0ms262×0exit
49.0ms51×3valid
18.0ms11×5exit
6.0ms3×4valid
Compiler

Compiled 33 111 to 4 061 computations (87.7% saved)

Precisions
Click to see histograms. Total time spent on operations: 10.4s
ival-mult: 3.2s (30.7% of total)
ival-div: 1.5s (13.9% of total)
ival-add: 1.4s (13.5% of total)
adjust: 896.0ms (8.6% of total)
ival-sub: 791.0ms (7.6% of total)
ival-pow: 637.0ms (6.1% of total)
const: 612.0ms (5.9% of total)
ival-sin: 368.0ms (3.5% of total)
ival-pow2: 211.0ms (2% of total)
ival-neg: 127.0ms (1.2% of total)
ival-exp: 120.0ms (1.2% of total)
ival-cos: 120.0ms (1.2% of total)
ival-sqrt: 116.0ms (1.1% of total)
exact: 95.0ms (0.9% of total)
ival-log: 57.0ms (0.5% of total)
ival-cosh: 56.0ms (0.5% of total)
ival-expm1: 45.0ms (0.4% of total)
ival-log1p: 34.0ms (0.3% of total)
ival-true: 32.0ms (0.3% of total)
ival-sinh: 18.0ms (0.2% of total)
ival-assert: 16.0ms (0.2% of total)
ival-tan: 7.0ms (0.1% of total)
ival-atan: 7.0ms (0.1% of total)
ival-pi: 4.0ms (0% of total)
ival-fabs: 1.0ms (0% of total)

eval15.1s (5.7%)

Memory
114.1MiB live, 20 418.6MiB allocated
Compiler

Compiled 3 526 618 to 288 238 computations (91.8% saved)

explain10.3s (3.9%)

Memory
23.2MiB live, 12 833.2MiB allocated
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
-.f64#fcancellation13013
+.f64#fcancellation37993
sqrt.f64#foflow-rescue2320
-.f64(-.f64 (*.f64 #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64) t) #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64))oflow-left2190
log.f64(log.f64 (+.f64 #s(literal 1 binary64) x))sensitivity1721
/.f64#fn/o1700
/.f64#fo/o1590
-.f64#fnan-rescue1260
pow.f64(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)sensitivity1150
/.f64#fu/n860
/.f64#fu/u630
/.f64#fn/u490
+.f64#fnan-rescue490
*.f64#fn*u380
/.f64#fo/n360
*.f64#fn*o270
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)overflow34
↳(/.f64 i n)overflow20
↳(+.f64 #s(literal 1 binary64) (/.f64 i n))overflow20
sqrt.f64#fuflow-rescue80
Confusion
Predicted +Predicted -
+3897220
-1296506
Precision
0.9679582712369598
Recall
0.9465630313334953
Confusion?
Predicted +Predicted MaybePredicted -
+389714773
-1292066300
Precision?
0.9234985156428408
Recall?
0.9822686422152053
Freqs
test
numberfreq
06726
13577
2400
349
Total Confusion?
Predicted +Predicted MaybePredicted -
+3110
-208
Precision?
0.9411764705882353
Recall?
1.0
Samples
2.1s16 496×0valid
1.2s3 658×1valid
532.0ms1 326×2valid
54.0ms22×3valid
4.0ms2×4valid
Compiler

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

Precisions
Click to see histograms. Total time spent on operations: 2.8s
ival-div: 762.0ms (27.1% of total)
ival-mult: 584.0ms (20.8% of total)
ival-pow: 294.0ms (10.5% of total)
ival-add: 277.0ms (9.9% of total)
adjust: 237.0ms (8.4% of total)
ival-sub: 222.0ms (7.9% of total)
ival-sin: 122.0ms (4.3% of total)
ival-cos: 72.0ms (2.6% of total)
const: 52.0ms (1.9% of total)
ival-pow2: 44.0ms (1.6% of total)
ival-exp: 42.0ms (1.5% of total)
ival-sqrt: 21.0ms (0.7% of total)
ival-true: 20.0ms (0.7% of total)
exact: 18.0ms (0.6% of total)
ival-neg: 15.0ms (0.5% of total)
ival-assert: 10.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.1% of total)
ival-expm1: 3.0ms (0.1% of total)
ival-pi: 2.0ms (0.1% of total)

preprocess8.9s (3.4%)

Memory
504.0MiB live, 8 789.0MiB allocated
Algorithm
42×egg-herbie
Stop Event
82×iter limit
53×saturated
33×node limit
Compiler

Compiled 62 009 to 8 130 computations (86.9% saved)

prune5.9s (2.2%)

Memory
-356.6MiB live, 8 048.3MiB allocated
Counts
74 416 → 1 994
Compiler

Compiled 153 600 to 65 774 computations (57.2% saved)

regimes5.8s (2.2%)

Memory
51.3MiB live, 7 574.1MiB allocated
Counts
4 777 → 539
Calls

96 calls:

855.0ms
x
280.0ms
x1
266.0ms
b
245.0ms
(*.f64 (cos.f64 x) (exp.f64 (*.f64 #s(literal 10 binary64) (*.f64 x x))))
228.0ms
c
Compiler

Compiled 9 243 to 5 805 computations (37.2% saved)

analyze4.9s (1.8%)

Memory
86.2MiB live, 5 405.6MiB allocated
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)

series4.2s (1.6%)

Memory
222.6MiB live, 5 523.2MiB allocated
Counts
2 005 → 9 828
Calls

876 calls:

TimeVariablePointExpression
124.0ms
i
@0
((* (/ (* 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)) (- (exp (* (log (+ 1 (/ i n))) n)) 1) (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (+ (* (+ (* (* n i) (- (+ (/ 1/3 (* n n)) 1/6) (/ 1/2 n))) (* (- 1/2 (/ 1/2 n)) n)) i) n) (* (+ (* (+ (* 1/6 i) 1/2) i) 1) n) (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (- (pow (+ 1 (/ i n)) n) 1) (- (exp i) 1) (* 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) (* (* (- (exp (* (log (+ 1 (/ i n))) n)) 1) (/ 100 i)) n) (* (- (exp (* (log (+ 1 (/ i n))) n)) 1) (/ 100 i)) (* (* n (/ (- (log i) (log n)) i)) 100) (* n (/ (- (log i) (log n)) i)) (* (log (+ 1 (/ i n))) n) (log (+ 1 (/ i n))) (+ (* 1/6 i) 1/2) (- (log i) (log n)) (/ (- (log i) (log n)) i))
104.0ms
v
@0
((* (+ (* -2 v) 3) 1/8) (- (+ (/ 2 (* r r)) 3) (+ (* (* (/ (pow (* w r) 2) (- 1 (* v v))) (+ v 1)) (* (+ (* -2 v) 3) 1/8)) 9/2)) (+ (/ 2 (* r r)) 3) (/ 2 (* r r)) (- (- (+ 3 (/ 2 (* r r))) (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (- 1 v))) 9/2) (- (/ 2 (* r r)) 3/2) (- (- (+ 3 (/ 2 (* r r))) (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (- 1 v))) 9/2) (* (* (* (/ w (- 1 v)) (* (+ (* -2 v) 3) w)) (* -1/8 r)) r) (* (* (/ w (- 1 v)) (* (+ (* -2 v) 3) w)) (* -1/8 r)) (* -1/4 (* (* w w) r)) (+ (* (* (* 3/8 (* r r)) w) w) 3/2) (- (- (+ 3 (/ 2 (* r r))) (/ (* (* (+ (* -2 v) 3) (* (* 1/8 w) (* w r))) r) (- 1 v))) 9/2) (- (/ 2 (* r r)) (+ (* (* (* 3/8 (* r r)) w) w) 3/2)) (* (/ (* (* (* w (+ (* v -2) 3)) w) (* -1/8 r)) (- 1 v)) r) (* (* (* w (+ (* v -2) 3)) w) (* -1/8 r)) (- (- (+ 3 (/ 2 (* r r))) (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (- 1 v))) 9/2) (/ (* (* (* w (+ (* v -2) 3)) w) (* -1/8 r)) (- 1 v)) (/ (pow (* w r) 2) (- 1 (* v v))) (* (/ (pow (* w r) 2) (- 1 (* v v))) (+ v 1)) (pow (* w r) 2) (* (* w w) r) (* (* 3/8 (* r r)) w))
101.0ms
y
@inf
((+ (+ (+ (* 1335/4 (pow y 6)) (* (* x x) (- (- (- (* (* (* (* 11 x) x) y) y) (pow y 6)) (* 121 (pow y 4))) 2))) (* 11/2 (pow y 8))) (/ x (+ y y))) (+ (+ (* 1335/4 (pow y 6)) (* (* x x) (- (- (- (* (* (* (* 11 x) x) y) y) (pow y 6)) (* 121 (pow y 4))) 2))) (* 11/2 (pow y 8))) (* -2 (* x x)) (* x x) (/ (- (* (pow (+ (+ (* 1335/4 (pow y 6)) (* (* x x) (- (- (- (* (* (* (* 11 x) x) y) y) (pow y 6)) (* 121 (pow y 4))) 2))) (* 11/2 (pow y 8))) 2) (- (+ (+ (* 1335/4 (pow y 6)) (* (* x x) (- (- (- (* (* (* (* 11 x) x) y) y) (pow y 6)) (* 121 (pow y 4))) 2))) (* 11/2 (pow y 8))) (/ x (* 2 y)))) (* (- (+ (+ (* 1335/4 (pow y 6)) (* (* x x) (- (- (- (* (* (* (* 11 x) x) y) y) (pow y 6)) (* 121 (pow y 4))) 2))) (* 11/2 (pow y 8))) (/ x (* 2 y))) (pow (/ x (* 2 y)) 2))) (* (- (+ (+ (* 1335/4 (pow y 6)) (* (* x x) (- (- (- (* (* (* (* 11 x) x) y) y) (pow y 6)) (* 121 (pow y 4))) 2))) (* 11/2 (pow y 8))) (/ x (* 2 y))) (- (+ (+ (* 1335/4 (pow y 6)) (* (* x x) (- (- (- (* (* (* (* 11 x) x) y) y) (pow y 6)) (* 121 (pow y 4))) 2))) (* 11/2 (pow y 8))) (/ x (* 2 y))))) (- (* (pow (+ (+ (* 1335/4 (pow y 6)) (* (* x x) (- (- (- (* (* (* (* 11 x) x) y) y) (pow y 6)) (* 121 (pow y 4))) 2))) (* 11/2 (pow y 8))) 2) (- (+ (+ (* 1335/4 (pow y 6)) (* (* x x) (- (- (- (* (* (* (* 11 x) x) y) y) (pow y 6)) (* 121 (pow y 4))) 2))) (* 11/2 (pow y 8))) (/ x (* 2 y)))) (* (- (+ (+ (* 1335/4 (pow y 6)) (* (* x x) (- (- (- (* (* (* (* 11 x) x) y) y) (pow y 6)) (* 121 (pow y 4))) 2))) (* 11/2 (pow y 8))) (/ x (* 2 y))) (pow (/ x (* 2 y)) 2))) (* (pow (+ (+ (* 1335/4 (pow y 6)) (* (* x x) (- (- (- (* (* (* (* 11 x) x) y) y) (pow y 6)) (* 121 (pow y 4))) 2))) (* 11/2 (pow y 8))) 2) (- (+ (+ (* 1335/4 (pow y 6)) (* (* x x) (- (- (- (* (* (* (* 11 x) x) y) y) (pow y 6)) (* 121 (pow y 4))) 2))) (* 11/2 (pow y 8))) (/ x (* 2 y)))) (pow (+ (+ (* 1335/4 (pow y 6)) (* (* x x) (- (- (- (* (* (* (* 11 x) x) y) y) (pow y 6)) (* 121 (pow y 4))) 2))) (* 11/2 (pow y 8))) 2) (+ y y) (+ (+ (* 1335/4 (pow y 6)) (* (* x x) (- (- (- (* (* (* (* 11 x) x) y) y) (pow y 6)) (* 121 (pow y 4))) 2))) (* 11/2 (pow y 8))) (* (- (+ (+ (* 1335/4 (pow y 6)) (* (* x x) (- (- (- (* (* (* (* 11 x) x) y) y) (pow y 6)) (* 121 (pow y 4))) 2))) (* 11/2 (pow y 8))) (/ x (* 2 y))) (pow (/ x (* 2 y)) 2)) (pow (/ x (* 2 y)) 2) (* 2 y))
58.0ms
eps
@0
((- (* x x) (- (* x x) eps)) (/ (- (* x x) (- (* x x) eps)) (+ (sqrt (- (* x x) eps)) x)) (* x x) (- (* x x) eps) (+ (* (pow (- (* x x) eps) 1/4) (neg (pow (- (* x x) eps) 1/4))) x) (- x (/ (- (* x x) eps) (sqrt (- (* x x) eps)))) (/ (- (* x x) eps) (sqrt (- (* x x) eps))) (- (/ (* x x) (+ (sqrt (- (* x x) eps)) x)) (/ (- (* x x) eps) (+ (sqrt (- (* x x) eps)) x))) (/ (* x x) (+ (sqrt (- (* x x) eps)) x)) (+ (sqrt (- (* x x) eps)) x) (/ (- (* (/ (* x x) (+ (sqrt (- (* x x) eps)) x)) (/ (* x x) (+ (sqrt (- (* x x) eps)) x))) (* (/ (- (* x x) eps) (+ (sqrt (- (* x x) eps)) x)) (/ (- (* x x) eps) (+ (sqrt (- (* x x) eps)) x)))) (+ (/ (* x x) (+ (sqrt (- (* x x) eps)) x)) (/ (- (* x x) eps) (+ (sqrt (- (* x x) eps)) x)))) (- (* (/ (* x x) (+ (sqrt (- (* x x) eps)) x)) (/ (* x x) (+ (sqrt (- (* x x) eps)) x))) (* (/ (- (* x x) eps) (+ (sqrt (- (* x x) eps)) x)) (/ (- (* x x) eps) (+ (sqrt (- (* x x) eps)) x)))) (+ (/ (* x x) (+ (sqrt (- (* x x) eps)) x)) (/ (- (* x x) eps) (+ (sqrt (- (* x x) eps)) x))) (* (/ (* x x) (+ (sqrt (- (* x x) eps)) x)) (/ (* x x) (+ (sqrt (- (* x x) eps)) x))) (sqrt (- (* x x) eps)) (- (* x x) eps) (/ (- (* x x) eps) (+ (sqrt (- (* x x) eps)) x)) (* (/ (- (* x x) eps) (+ (sqrt (- (* x x) eps)) x)) (/ (- (* x x) eps) (+ (sqrt (- (* x x) eps)) x))))
58.0ms
y
@0
((* (/ (+ y x) (+ (* y y) (* x x))) (- x y)) (/ (+ y x) (+ (* y y) (* x x))) (/ (+ (- 1 (pow (/ x y) 3)) (/ (+ (* (neg x) (/ x y)) x) y)) y) (+ (- 1 (pow (/ x y) 3)) (/ (+ (* (neg x) (/ x y)) x) y)) (+ (* (* -2 y) (/ y (* x x))) 1) (/ (* (- x y) (+ x y)) (+ (* x x) (* y y))) (* -2 y) (/ y (* x x)) (* (/ (+ y x) (+ (* y y) (* x x))) (- x y)) (/ (+ y x) (+ (* y y) (* x x))) (/ (+ (* (/ x y) (- 1 (/ x y))) 1) y) (+ (* (/ x y) (- 1 (/ x y))) 1) (/ (* (/ y x) (* (/ y x) y)) x) (* (/ y x) (* (/ y x) y)) (+ (- 1 (/ (* (/ y x) (* (/ y x) y)) x)) (* (/ y x) (- 1 (/ y x)))) (* (/ (+ y x) (+ (* y y) (* x x))) (- x y)) (+ (cosh (log (/ y x))) (sinh (log (/ y x)))) (+ (- 1 (pow (/ y x) 3)) (* (+ (cosh (log (/ y x))) (sinh (log (/ y x)))) (- 1 (/ y x)))) (* (/ (+ y x) (+ (* y y) (* x x))) (- x y)) (/ (+ y x) (+ (* y y) (* x x))) (pow (/ x y) 3) (/ (+ (* (neg x) (/ x y)) x) y) (/ (+ y x) (+ (* y y) (* x x))) (log (/ y x)) (sinh (log (/ y x))))

bsearch2.9s (1.1%)

Memory
-65.8MiB live, 3 018.6MiB allocated
Algorithm
171×binary-search
82×left-value
Stop Event
159×narrow-enough
11×predicate-same
1×predicate-failed
Samples
1.1s10 090×0valid
202.0ms964×1valid
122.0ms412×2valid
84.0ms984×0invalid
7.0ms22×3valid
Compiler

Compiled 128 718 to 69 409 computations (46.1% saved)

Precisions
Click to see histograms. Total time spent on operations: 1.1s
ival-mult: 431.0ms (38.7% of total)
ival-div: 166.0ms (14.9% of total)
ival-sub: 165.0ms (14.8% of total)
ival-add: 111.0ms (10% of total)
ival-pow: 76.0ms (6.8% of total)
adjust: 50.0ms (4.5% of total)
ival-exp: 30.0ms (2.7% of total)
ival-neg: 27.0ms (2.4% of total)
ival-sqrt: 25.0ms (2.2% of total)
exact: 10.0ms (0.9% of total)
ival-true: 9.0ms (0.8% of total)
ival-assert: 5.0ms (0.4% of total)
const: 4.0ms (0.4% of total)
ival-expm1: 4.0ms (0.4% of total)
ival-pi: 2.0ms (0.2% of total)

start13.0ms (0%)

Memory
5.5MiB live, 5.5MiB allocated

end0.0ms (0%)

Memory
0.6MiB live, 0.7MiB allocated

Profiling

Loading profile data...