Herbie run

Date:Sunday, April 27th, 2025
Commit:1a213e3e on autofix-26-1
Seed:2025117
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 229.5 MB

Time bar (total: 2.1min)

sample50.5s (40.2%)

Memory
839.4MiB live, 54 790.3MiB allocated; 23.8s collecting garbage
Samples
20.6s293 039×0valid
8.2s35 604×1valid
7.1s17 646×2valid
456.0ms4 356×0invalid
381.0ms952×0exit
302.0ms463×3valid
160.0ms101×4exit
48.0ms101×3exit
5.0ms42×1exit
Precisions
Click to see histograms. Total time spent on operations: 24.7s
ival-mult!: 5.6s (22.7% of total)
ival-pow: 3.5s (14% of total)
ival-div!: 2.7s (11% of total)
ival-sin: 2.4s (9.8% of total)
adjust: 2.3s (9.4% of total)
ival-sub!: 1.8s (7.3% of total)
ival-add!: 1.6s (6.4% of total)
ival-cos: 1.5s (6.1% of total)
ival-sqrt: 1.1s (4.3% of total)
ival-exp: 929.0ms (3.8% of total)
ival-neg: 435.0ms (1.8% of total)
ival-pow2: 274.0ms (1.1% of total)
ival-log1p: 236.0ms (1% of total)
ival-expm1: 128.0ms (0.5% of total)
ival-tan: 115.0ms (0.5% of total)
ival-atan: 83.0ms (0.3% of total)
ival-hypot: 15.0ms (0.1% of total)
ival-<=: 11.0ms (0% of total)
ival-and: 7.0ms (0% of total)
ival-if: 4.0ms (0% of total)
ival-fabs: 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

rewrite32.1s (25.5%)

Memory
677.2MiB live, 29 458.5MiB allocated; 9.7s collecting garbage
Stop Event
368×iter-limit
146×node-limit
10×saturated
unsound
Counts
19 441 → 39 984

derivations8.8s (7%)

Memory
-183.4MiB live, 7 729.7MiB allocated; 2.9s collecting garbage
Stop Event
23×fuel
19×done
Compiler

Compiled 5 067 to 2 659 computations (47.5% saved)

eval6.8s (5.4%)

Memory
89.1MiB live, 9 289.7MiB allocated; 2.1s collecting garbage
Compiler

Compiled 561 383 to 176 563 computations (68.5% saved)

regimes6.0s (4.8%)

Memory
-42.5MiB live, 8 099.7MiB allocated; 1.9s collecting garbage
Counts
4 644 → 566
Calls

96 calls:

678.0ms
x
324.0ms
b
281.0ms
(*.f64 (cos.f64 x) (exp.f64 (*.f64 #s(literal 10 binary64) (*.f64 x x))))
268.0ms
(-.f64 (-.f64 (+.f64 #s(literal 3 binary64) (/.f64 #s(literal 2 binary64) (*.f64 r r))) (/.f64 (*.f64 (*.f64 #s(literal 1/8 binary64) (-.f64 #s(literal 3 binary64) (*.f64 #s(literal 2 binary64) v))) (*.f64 (*.f64 (*.f64 w w) r) r)) (-.f64 #s(literal 1 binary64) v))) #s(literal 9/2 binary64))
265.0ms
c
Compiler

Compiled 6 910 to 5 662 computations (18.1% saved)

series6.0s (4.7%)

Memory
-101.7MiB live, 5 987.8MiB allocated; 3.1s collecting garbage
Counts
3 245 → 16 196
Calls

897 calls:

TimeVariablePointExpression
227.0ms
n
@-inf
((* (* (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) n) 100) (* (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) n) (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) (- (exp (* (log (+ (/ i n) 1)) n)) 1) (* (log (+ (/ i n) 1)) n) i n 100 (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (/ (* (- (exp i) 1) n) i) (* (- (exp i) 1) n) (- (exp 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) (- (exp i) 1) (/ i n) (* (* (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) n) 100) (* (/ (* (log (* (/ 1 n) i)) (* n n)) i) 100) (/ (* (log (* (/ 1 n) i)) (* n n)) i) (* (log (* (/ 1 n) i)) (* n n)) (log (* (/ 1 n) i)) (* (/ 1 n) i) (/ 1 n) 1 (* n n) (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (* (* (- (exp (* (log (* (/ 1 n) i)) n)) 1) n) 100) i) (* (* (- (exp (* (log (* (/ 1 n) i)) n)) 1) n) 100) (* (- (exp (* (log (* (/ 1 n) i)) n)) 1) n) (- (exp (* (log (* (/ 1 n) i)) n)) 1) (* (log (* (/ 1 n) i)) n))
113.0ms
c
@inf
((/ (- (* b c) (* a d)) (+ (* c c) (* d d))) (* (neg b) (/ (+ (* a (/ d b)) (neg c)) (+ (* d d) (* c c)))) (neg b) b (/ (+ (* a (/ d b)) (neg c)) (+ (* d d) (* c c))) (+ (* a (/ d b)) (neg c)) a (/ d b) d (neg c) c (+ (* d d) (* c c)) (* c c) (/ (- (* b c) (* a d)) (+ (* c c) (* d d))) (/ (neg a) d) (neg a) (/ (- (* b c) (* a d)) (+ (* c c) (* d d))) (neg (/ (+ (neg (/ (* c b) d)) a) d)) (/ (+ (neg (/ (* c b) d)) a) d) (/ (* (neg b) c) (* d d)) (* (neg b) c) (* d d) (/ (- (* b c) (* a d)) (+ (* c c) (* d d))) (neg (/ (+ (* (/ d c) a) (neg b)) c)) (/ (+ (* (/ d c) a) (neg b)) c) (+ (* (/ d c) a) (neg b)) (/ d c) (/ (- (* b c) (* a d)) (+ (* c c) (* d d))) (+ (* (/ (neg a) c) (/ d c)) (/ b c)) (/ (neg a) c) (/ b c))
107.0ms
i
@-inf
((* (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) (* 100 n)) (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) (- (exp (* (log (+ (/ i n) 1)) n)) 1) (* (log (+ (/ i n) 1)) n) i (* 100 n) 100 n (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (* (- (exp i) 1) (/ n i)) (- (exp i) 1) (/ n i) (/ (* 100 (- (exp (* (log (+ (/ i n) 1)) n)) 1)) (/ i n)) (* 100 (- (exp (* (log (+ (/ i n) 1)) n)) 1)) (- (exp (* (log (+ (/ i n) 1)) n)) 1) (- (exp i) 1) (/ i n) (* (* (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) n) 100) (/ (* (* (* (log (* (/ 1 n) i)) n) n) 100) i) (* (* (* (log (* (/ 1 n) i)) n) n) 100) (* (* (log (* (/ 1 n) i)) n) n) (* (log (* (/ 1 n) i)) n) (log (* (/ 1 n) i)) (* (/ 1 n) i) (/ 1 n) 1 (* (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) (* n 100)) (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) (- (exp (* (log (+ (/ i n) 1)) n)) 1) (* (log (+ (/ i n) 1)) n) (log (+ (/ i n) 1)) (+ (/ i n) 1) (* n 100))
106.0ms
b
@inf
((+ (/ (sqrt (+ (* b b) (* (* a -4) c))) (+ a a)) (/ (neg b) (+ a a))) (/ (sqrt (+ (* b b) (* (* a -4) c))) (+ a a)) (sqrt (+ (* b b) (* (* a -4) c))) (+ (* b b) (* (* a -4) c)) b (* (* a -4) c) (* a -4) a -4 c (+ a a) (/ (neg b) (+ a a)) (neg b) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (* (neg b) (+ (/ (neg c) (* b b)) (/ 1 a))) (/ c b) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (* (sqrt (* (/ c a) -4)) 1/2) (sqrt (* (/ c a) -1)) (* (/ c a) -1) (/ c a) -1 (/ (+ (sqrt (+ (* (* -4 a) c) (* b b))) (neg b)) (+ a a)) (+ (sqrt (+ (* (* -4 a) c) (* b b))) (neg b)) (sqrt (* (* a -4) c)) (/ (+ (sqrt (+ (* (* -4 a) c) (* b b))) (neg b)) (+ a a)) (+ (sqrt (+ (* (* -4 a) c) (* b b))) (neg b)) (sqrt (+ (* (* -4 a) c) (* b b))) (+ (* (* -4 a) c) (* b b)))
98.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 (* 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))) (+ (* 1335/4 (pow y 6)) (* (* x x) (- (- (- (* (* (* (* 11 x) x) y) y) (pow y 6)) (* 121 (pow y 4))) 2))) (* 1335/4 (pow y 6)) 1335/4 (pow y 6) y 6 (* (* x x) (- (- (- (* (* (* (* 11 x) x) y) y) (pow y 6)) (* 121 (pow y 4))) 2)) (* x x) x (- (- (- (* (* (* (* 11 x) x) y) y) (pow y 6)) (* 121 (pow y 4))) 2) (- (- (* (* (* (* 11 x) x) y) y) (pow y 6)) (* 121 (pow y 4))) (- (* (* (* (* 11 x) x) y) y) (pow y 6)) (* (* (* (* 11 x) x) y) y) (* (* (* 11 x) x) y) (* (* 11 x) x) (* 11 x) 11 (* 121 (pow y 4)) 121 (pow y 4) 4 2 (* 11/2 (pow y 8)) 11/2 (pow y 8) 8 (/ x (* 2 y)) (* 2 y))

preprocess5.8s (4.6%)

Memory
-339.6MiB live, 6 828.1MiB allocated; 1.5s collecting garbage
Stop Event
32×node-limit
10×saturated
Compiler

Compiled 19 641 to 14 409 computations (26.6% saved)

analyze3.4s (2.7%)

Memory
-20.4MiB live, 3 711.7MiB allocated; 1.6s 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)

prune3.2s (2.5%)

Memory
347.3MiB live, 4 733.5MiB allocated; 875ms collecting garbage
Counts
36 310 → 1 985
Compiler

Compiled 90 773 to 67 721 computations (25.4% saved)

bsearch3.1s (2.5%)

Memory
-41.1MiB live, 3 594.3MiB allocated; 998ms collecting garbage
Algorithm
193×binary-search
87×left-value
Stop Event
180×narrow-enough
12×predicate-same
predicate-failed
Samples
1.2s10 177×0valid
311.0ms485×2valid
237.0ms1 027×1valid
104.0ms1 190×0invalid
19.0ms23×3valid
1.0ms0exit
Compiler

Compiled 96 041 to 75 795 computations (21.1% saved)

Precisions
Click to see histograms. Total time spent on operations: 1.1s
ival-mult!: 367.0ms (32.6% of total)
ival-pow: 260.0ms (23.1% of total)
ival-div!: 197.0ms (17.5% of total)
ival-add!: 92.0ms (8.2% of total)
adjust: 63.0ms (5.6% of total)
ival-sub!: 61.0ms (5.4% of total)
ival-neg: 32.0ms (2.8% of total)
ival-exp: 25.0ms (2.2% of total)
ival-sqrt: 23.0ms (2% of total)
ival-log1p: 4.0ms (0.4% of total)
ival-expm1: 3.0ms (0.3% of total)

start2.0ms (0%)

Memory
5.3MiB live, 5.4MiB allocated; 0ms collecting garbage

end0.0ms (0%)

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

Profiling

Loading profile data...