Herbie run
| Date: | Thursday, April 24th, 2025 |
|---|---|
| Commit: | d5acc5eb on main |
| Seed: | 2025114 |
| 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: | 140 494.8 MB |
Time bar (total: 2.3min)
| 23.9s | 44 610× | 2 | valid |
| 17.0s | 96 920× | 1 | valid |
| 15.4s | 146 423× | 0 | invalid |
| 10.5s | 5 838× | 5 | exit |
| 6.3s | 86 075× | 0 | valid |
| 2.5s | 3 558× | 3 | valid |
| 280.0ms | 4 085× | 0 | exit |
| 229.0ms | 1 083× | 1 | exit |
| 120.0ms | 134× | 4 | exit |
| 8.0ms | 2× | 3 | exit |
| 8.0ms | 5× | 4 | valid |
ival-tan: 11.9s (18.9% of total)ival-pow: 10.1s (16.1% of total)adjust: 6.6s (10.5% of total)ival-mult!: 3.9s (6.2% of total)ival-cos: 3.8s (6.1% of total)ival-log: 3.6s (5.8% of total)ival-div!: 3.2s (5.1% of total)ival-sin: 3.2s (5.1% of total)ival-add!: 2.7s (4.4% of total)ival-expm1: 2.2s (3.5% of total)ival-sub!: 2.0s (3.2% of total)ival-exp: 1.9s (3.1% of total)ival-sqrt: 1.7s (2.8% of total)ival-fabs: 1.7s (2.7% of total)ival-log1p: 1.5s (2.4% of total)ival-<: 833.0ms (1.3% of total)ival-<=: 375.0ms (0.6% of total)ival-atan: 374.0ms (0.6% of total)ival-and: 333.0ms (0.5% of total)ival-cbrt: 273.0ms (0.4% of total)ival-neg: 255.0ms (0.4% of total)ival-fmin: 74.0ms (0.1% of total)ival-assert: 62.0ms (0.1% of total)ival->: 1.0ms (0% of total)exact: 0.0ms (0% of total)| 265× | iter-limit |
| 107× | node-limit |
Compiled 480 505 to 170 934 computations (64.4% saved)
| 23× | fuel |
| 5× | done |
Compiled 3 106 to 1 849 computations (40.5% saved)
501 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 172.0ms | n | @ | 0 | ((- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (neg (/ (+ (+ (neg (/ (+ (neg (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n)) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))))) n)) (neg (log (+ 1 x)))) (log x)) n)) (/ (+ (+ (neg (/ (+ (neg (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n)) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))))) n)) (neg (log (+ 1 x)))) (log x)) n) (+ (+ (neg (/ (+ (neg (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n)) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))))) n)) (neg (log (+ 1 x)))) (log x)) (+ (neg (/ (+ (neg (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n)) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))))) n)) (neg (log (+ 1 x)))) (neg (/ (+ (neg (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n)) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))))) n)) (/ (+ (neg (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n)) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))))) n) (+ (neg (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n)) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))))) (neg (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n)) (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n) (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3)) (pow (log (+ 1 x)) 3) (log (+ 1 x)) (+ 1 x) 1 x 3 (pow (log x) 3) (log x) n (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))) (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)) (neg (log (+ 1 x))) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (log (/ (+ 1 x) x)) n) (log (/ (+ 1 x) x)) (/ (+ 1 x) x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (+ x 1) (/ 1 n) (pow x (/ 1 n)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (+ (/ x n) 1) (/ x n) (pow x (/ 1 n)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (neg (/ (+ (+ (neg (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n)) (neg (log (+ 1 x)))) (log x)) n)) (/ (+ (+ (neg (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n)) (neg (log (+ 1 x)))) (log x)) n) (+ (+ (neg (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n)) (neg (log (+ 1 x)))) (log x)) (+ (neg (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n)) (neg (log (+ 1 x)))) (neg (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n)) (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n)) |
| 84.0ms | n | @ | 0 | ((- (- (* (+ n 1) (log (+ n 1))) (* n (log n))) 1) (- (* (+ n 1) (log (+ n 1))) (* n (log n))) (* (+ n 1) (log (+ n 1))) (+ n 1) n 1 (log (+ n 1)) (* n (log n)) (log n)) |
| 80.0ms | n | @ | 0 | ((- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (neg (/ (+ (+ (neg (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n)) (neg (log (+ 1 x)))) (log x)) n)) (/ (+ (+ (neg (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n)) (neg (log (+ 1 x)))) (log x)) n) (+ (+ (neg (/ (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) n)) (neg (log (+ 1 x)))) (log x)) (/ (- (* n (log (/ x (+ 1 x)))) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))))) n) (- (* n (log (/ x (+ 1 x)))) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))))) (* n (log (/ x (+ 1 x)))) n (log (/ x (+ 1 x))) (/ x (+ 1 x)) x (+ 1 x) 1 (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x)))) 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))) (* (log (+ 1 x)) (log (+ 1 x))) (log (+ 1 x)) (* (log x) (log x)) (log x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (log (/ (+ 1 x) x)) n) (log (/ (+ 1 x) x)) (+ x (neg (log x))) (neg (log x)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (log (/ (+ 1 x) x)) n) (log (/ (+ 1 x) x)) (/ (- (+ 1 (/ 1/3 (* x x))) (* 1/2 (/ 1 x))) x) (- (+ 1 (/ 1/3 (* x x))) (* 1/2 (/ 1 x))) (+ 1 (/ 1/3 (* x x))) (/ 1/3 (* x x)) 1/3 (* x x) (* 1/2 (/ 1 x)) (/ 1 x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (neg (/ (+ (+ (neg (/ (+ (neg (/ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) n)) (* 1/2 (- (* (log (+ 1 x)) (log (+ 1 x))) (* (log x) (log x))))) n)) (neg (log (+ 1 x)))) (log x)) n)) (- (* -1/2 (/ (* (log x) (log x)) (* n n))) (+ (* 1/6 (pow (/ (log x) n) 3)) (/ (log x) n))) (* -1/2 (/ (* (log x) (log x)) (* n n))) -1/2 (/ (* (log x) (log x)) (* n n)) (* n n) (+ (* 1/6 (pow (/ (log x) n) 3)) (/ (log x) n)) 1/6 (pow (/ (log x) n) 3) (/ (log x) n) 3) |
| 78.0ms | x | @ | inf | ((- (sin (+ (neg (+ eps x)) (/ (PI) 2))) (cos x)) (* (- (* (* (cos x) eps) -1/2) (sin x)) eps) (- (* (* (cos x) eps) -1/2) (sin x)) (* (* (cos x) eps) -1/2) (* (cos x) eps) (cos x) x eps -1/2 (sin x) (- (cos (+ x eps)) (cos x)) (- (cos eps) 1) (cos eps) 1 (- (cos (+ x eps)) (cos x)) (* (- (* (+ (* (* (sin x) eps) 1/6) (* -1/2 (cos x))) eps) (sin x)) eps) (- (* (+ (* (* (sin x) eps) 1/6) (* -1/2 (cos x))) eps) (sin x)) (+ (* (- (+ (* (* eps x) 1/4) (* (* eps eps) 1/6)) 1) x) (* -1/2 eps)) (- (+ (* (* eps x) 1/4) (* (* eps eps) 1/6)) 1) (+ (* (* eps x) 1/4) (* (* eps eps) 1/6)) (* eps x) 1/4 (* (* eps eps) 1/6) (* eps eps) 1/6 (* -1/2 eps) (- (cos (+ x eps)) (cos x)) (* (- (* (+ (* (* (sin x) eps) 1/6) (* -1/2 (cos x))) eps) (sin x)) eps) (+ (* (+ (* (+ (* (* (+ (* -1/36 (* eps eps)) 1/6) x) eps) (* 1/4 (* eps eps))) x) (* (- (* (* eps eps) 1/6) 1) eps)) x) (* (* eps eps) -1/2)) (+ (* (+ (* (* (+ (* -1/36 (* eps eps)) 1/6) x) eps) (* 1/4 (* eps eps))) x) (* (- (* (* eps eps) 1/6) 1) eps)) (+ (* (* (+ (* -1/36 (* eps eps)) 1/6) x) eps) (* 1/4 (* eps eps))) (* (+ (* -1/36 (* eps eps)) 1/6) x) (+ (* -1/36 (* eps eps)) 1/6) -1/36 (* 1/4 (* eps eps)) (* (- (* (* eps eps) 1/6) 1) eps) (- (* (* eps eps) 1/6) 1) (* (* eps eps) -1/2) (- (sin (+ (neg (+ eps x)) (/ (PI) 2))) (sin (+ (/ (PI) 2) x))) (sin (+ (neg (+ eps x)) (/ (PI) 2))) (+ (neg (+ eps x)) (/ (PI) 2)) (neg (+ eps x)) (+ eps x) (/ (PI) 2) (PI) 2 (sin (+ (/ (PI) 2) x)) (+ (/ (PI) 2) x)) |
| 63.0ms | N | @ | 0 | ((log (+ 1 (/ N (* N N)))) (/ N (* N N)) N (* N N) (- (log (+ N 1)) (log N)) (- (log (+ N 1)) (log N)) (/ (/ (- N 1/2) N) N) (/ (- N 1/2) N) (- N 1/2) 1/2 (- (log (+ N 1)) (log N)) (/ (- (/ (- (/ 1/3 N) 1/2) N) -1) N) (- (/ (- (/ 1/3 N) 1/2) N) -1) (/ (- (/ 1/3 N) 1/2) N) (- (/ 1/3 N) 1/2) (/ 1/3 N) 1/3 -1 (- (log (+ N 1)) (log N)) (/ (- (/ (- (/ (- (/ 1/4 N) 1/3) (neg N)) 1/2) (neg N)) 1) (neg N)) (- (/ (- (/ (- (/ 1/4 N) 1/3) (neg N)) 1/2) (neg N)) 1) (/ (- (/ (- (/ 1/4 N) 1/3) (neg N)) 1/2) (neg N)) (- (/ (- (/ 1/4 N) 1/3) (neg N)) 1/2) (/ (- (/ 1/4 N) 1/3) (neg N)) (- (/ 1/4 N) 1/3) (/ 1/4 N) 1/4 (neg N) 1) |
43 calls:
| 1.4s | x |
| 428.0ms | eps |
| 196.0ms | (/.f64 #s(literal 1 binary64) n) |
| 146.0ms | (-.f64 (tan.f64 (+.f64 x eps)) (tan.f64 x)) |
| 118.0ms | (-.f64 (sin.f64 (+.f64 x eps)) (sin.f64 x)) |
Compiled 1 723 to 1 866 computations (-8.3% saved)
| 26× | node-limit |
| 2× | saturated |
Compiled 5 084 to 3 506 computations (31% saved)
Compiled 64 046 to 51 513 computations (19.6% saved)
| 28× | search |
| Probability | Valid | Unknown | Precondition | Infinite | Domain | Can't | Iter |
|---|---|---|---|---|---|---|---|
| 0% | 0% | 61.1% | 38.9% | 0% | 0% | 0% | 0 |
| 7.4% | 4.5% | 56.6% | 38.9% | 0% | 0% | 0% | 1 |
| 22.3% | 13.6% | 47.5% | 38.9% | 0% | 0% | 0% | 2 |
| 40.2% | 23.5% | 34.9% | 38.9% | 0% | 2.7% | 0% | 3 |
| 53.4% | 31.1% | 27.2% | 38.9% | 0% | 2.8% | 0% | 4 |
| 63% | 36.3% | 21.3% | 38.9% | 0% | 3.6% | 0% | 5 |
| 65.9% | 37.5% | 19.4% | 38.9% | 0% | 4.2% | 0% | 6 |
| 70.4% | 38.8% | 16.3% | 38.9% | 0% | 6% | 0% | 7 |
| 73.6% | 40.2% | 14.4% | 38.9% | 0% | 6.5% | 0% | 8 |
| 76.3% | 40.9% | 12.7% | 38.9% | 0% | 7.5% | 0% | 9 |
| 78.4% | 41.4% | 11.4% | 38.9% | 0% | 8.3% | 0% | 10 |
| 81.1% | 42.4% | 9.9% | 38.9% | 0% | 8.8% | 0% | 11 |
| 82.3% | 42.7% | 9.2% | 38.9% | 0% | 9.3% | 0% | 12 |
Compiled 483 to 337 computations (30.2% saved)
| 90× | binary-search |
| 20× | left-value |
| 87× | narrow-enough |
| 3× | predicate-same |
| 357.0ms | 5 196× | 0 | valid |
| 134.0ms | 1 115× | 1 | valid |
| 93.0ms | 352× | 2 | valid |
| 91.0ms | 1 214× | 0 | invalid |
| 2.0ms | 29× | 0 | exit |
| 2.0ms | 9× | 3 | valid |
Compiled 25 886 to 26 979 computations (-4.2% saved)
ival-mult!: 100.0ms (23.3% of total)ival-pow: 94.0ms (21.9% of total)ival-sqrt: 49.0ms (11.4% of total)ival-div!: 48.0ms (11.2% of total)adjust: 40.0ms (9.3% of total)ival-neg: 37.0ms (8.6% of total)ival-sub!: 30.0ms (7% of total)ival-add!: 13.0ms (3% of total)ival-cbrt: 10.0ms (2.3% of total)ival-cos: 7.0ms (1.6% of total)ival-expm1: 2.0ms (0.5% of total)Loading profile data...