Herbie run
| Date: | Wednesday, April 16th, 2025 |
|---|---|
| Commit: | 5565a39e on main |
| Seed: | 2025106 |
| 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: | 75 150.4 MB |
Time bar (total: 1.1min)
| 11.4s | 15 328× | 5 | exit |
| 6.9s | 39 763× | 1 | valid |
| 6.8s | 108 474× | 0 | valid |
| 5.6s | 16 883× | 2 | valid |
| 456.0ms | 3 944× | 0 | invalid |
| 190.0ms | 1 116× | 1 | exit |
| 160.0ms | 1 283× | 0 | exit |
ival-exp: 3.8s (15.5% of total)ival-pow: 3.4s (13.9% of total)adjust: 3.1s (12.6% of total)ival-cos: 2.4s (10% of total)ival-log: 1.6s (6.6% of total)ival-sinh: 1.5s (6.2% of total)ival-tan: 1.4s (5.9% of total)ival-mult!: 1.2s (5% of total)ival-sqrt: 1.1s (4.4% of total)ival-sin: 996.0ms (4.1% of total)ival-fmod: 840.0ms (3.5% of total)ival-div!: 745.0ms (3.1% of total)ival-acos: 624.0ms (2.6% of total)ival-sub!: 470.0ms (1.9% of total)ival-pow2: 372.0ms (1.5% of total)ival-add!: 334.0ms (1.4% of total)ival-neg: 156.0ms (0.6% of total)ival-hypot: 144.0ms (0.6% of total)ival-<=: 69.0ms (0.3% of total)ival-atan: 49.0ms (0.2% of total)ival-and: 35.0ms (0.1% of total)ival-or: 16.0ms (0.1% of total)ival-assert: 4.0ms (0% of total)ival-<: 2.0ms (0% of total)ival->: 1.0ms (0% of total)| 182× | iter-limit |
| 50× | node-limit |
| 15× | unsound |
| 4× | saturated |
53 calls:
| 608.0ms | x |
| 355.0ms | a |
| 266.0ms | b |
| 220.0ms | z |
| 179.0ms | r |
Compiled 1 524 to 1 754 computations (-15.1% saved)
| 11× | fuel |
| 9× | done |
Compiled 3 733 to 913 computations (75.5% saved)
378 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 398.0ms | x | @ | -inf | ((sqrt (+ (pow x 2) (pow x 2))) (* (sqrt 2) x) (sqrt 2) 2 x (sqrt (+ (pow x 2) (pow x 2))) (+ (pow x 2) (pow x 2)) (sqrt (+ (pow x 2) (pow x 2))) (* (neg x) (sqrt 2)) (neg x) (sqrt (+ (pow x 2) (* x x))) (+ (pow x 2) (* x x)) (pow x 2) (* x x) (/ (sqrt (* 2 (pow x 6))) (sqrt (+ 0 (pow x 4)))) (sqrt (* 2 (pow x 6))) (* 2 (pow x 6)) (pow x 6) 6 (sqrt (+ 0 (pow x 4))) (+ 0 (pow x 4)) 0 (pow x 4) 4) |
| 54.0ms | s | @ | inf | ((/ (cos (* 2 x)) (* (* (* c s) x) (* (* c s) x))) (cos (* 2 x)) (* 2 x) 2 x (* (* (* c s) x) (* (* c s) x)) (* (* c s) x) (* c s) c s (/ (cos (* 2 x)) (* (* c (* c (* x x))) (* s s))) (cos (* 2 x)) 1 (* (* c (* c (* x x))) (* s s)) (* c (* c (* x x))) (* c (* x x)) (* x x) (* s s) (/ (cos (+ x x)) (* (* (* s x) c) (* (* s x) c))) (cos (+ x x)) (+ (* (- (* 2/3 (* x x)) 2) (* x x)) 1) (- (* 2/3 (* x x)) 2) (* 2/3 (* x x)) 2/3 (* (* (* s x) c) (* (* s x) c)) (* (* s x) c) (* s x) (/ (cos (* 2 x)) (pow (* (* s c) x) 2)) (cos (* 2 x)) (+ (* (* x x) -2) 1) -2 (pow (* (* s c) x) 2) (* (* s c) x) (* s c) (/ (cos (* 2 x)) (* (* (* (* s x) (* c x)) c) s)) (* (* (* (* s x) (* c x)) c) s) (* (* (* s x) (* c x)) c) (* (* s x) (* c x)) (* c x)) |
| 45.0ms | l | @ | 0 | ((* (/ 1 (exp w)) (pow l (exp w))) (pow (exp -1) (+ (* (neg (log l)) (exp w)) w)) (exp -1) -1 (+ (* (neg (log l)) (exp w)) w) (neg (log l)) (log l) l (exp w) w (* (exp (neg w)) (pow l (exp w))) (exp (neg w)) (- 1 w) (neg w) (pow l (exp w)) (* (exp (neg w)) (pow l (exp w))) (exp (neg w)) (- 1 w) 1 (pow l (exp w)) (exp w) (+ (* (+ (* 1/2 w) 1) w) 1) (+ (* 1/2 w) 1) 1/2 (* (exp (neg w)) (pow l (exp w))) (exp (neg w)) (+ (* (+ (* (+ (* -1/6 w) 1/2) w) -1) w) 1) (+ (* (+ (* -1/6 w) 1/2) w) -1) (+ (* -1/6 w) 1/2) -1/6 (pow l (exp w)) (exp w) (+ (* (+ (* (+ (* 1/6 w) 1/2) w) 1) w) 1) (+ (* (+ (* 1/6 w) 1/2) w) 1) (+ (* 1/6 w) 1/2) 1/6 (* (exp (neg w)) (pow l (exp w))) (pow l (exp w)) (pow (pow (/ 1 l) (exp w)) -1) (pow (/ 1 l) (exp w)) (/ 1 l)) |
| 40.0ms | l | @ | -inf | ((* (/ 1 (exp w)) (pow l (exp w))) (pow (exp -1) (+ (* (neg (log l)) (exp w)) w)) (exp -1) -1 (+ (* (neg (log l)) (exp w)) w) (neg (log l)) (log l) l (exp w) w (* (exp (neg w)) (pow l (exp w))) (exp (neg w)) (- 1 w) (neg w) (pow l (exp w)) (* (exp (neg w)) (pow l (exp w))) (exp (neg w)) (- 1 w) 1 (pow l (exp w)) (exp w) (+ (* (+ (* 1/2 w) 1) w) 1) (+ (* 1/2 w) 1) 1/2 (* (exp (neg w)) (pow l (exp w))) (exp (neg w)) (+ (* (+ (* (+ (* -1/6 w) 1/2) w) -1) w) 1) (+ (* (+ (* -1/6 w) 1/2) w) -1) (+ (* -1/6 w) 1/2) -1/6 (pow l (exp w)) (exp w) (+ (* (+ (* (+ (* 1/6 w) 1/2) w) 1) w) 1) (+ (* (+ (* 1/6 w) 1/2) w) 1) (+ (* 1/6 w) 1/2) 1/6 (* (exp (neg w)) (pow l (exp w))) (pow l (exp w)) (pow (pow (/ 1 l) (exp w)) -1) (pow (/ 1 l) (exp w)) (/ 1 l)) |
| 40.0ms | w | @ | -inf | ((* (/ 1 (exp w)) (pow l (exp w))) (pow (exp -1) (+ (* (neg (log l)) (exp w)) w)) (exp -1) -1 (+ (* (neg (log l)) (exp w)) w) (neg (log l)) (log l) l (exp w) w (* (exp (neg w)) (pow l (exp w))) (exp (neg w)) (- 1 w) (neg w) (pow l (exp w)) (* (exp (neg w)) (pow l (exp w))) (exp (neg w)) (- 1 w) 1 (pow l (exp w)) (exp w) (+ (* (+ (* 1/2 w) 1) w) 1) (+ (* 1/2 w) 1) 1/2 (* (exp (neg w)) (pow l (exp w))) (exp (neg w)) (+ (* (+ (* (+ (* -1/6 w) 1/2) w) -1) w) 1) (+ (* (+ (* -1/6 w) 1/2) w) -1) (+ (* -1/6 w) 1/2) -1/6 (pow l (exp w)) (exp w) (+ (* (+ (* (+ (* 1/6 w) 1/2) w) 1) w) 1) (+ (* (+ (* 1/6 w) 1/2) w) 1) (+ (* 1/6 w) 1/2) 1/6 (* (exp (neg w)) (pow l (exp w))) (pow l (exp w)) (pow (pow (/ 1 l) (exp w)) -1) (pow (/ 1 l) (exp w)) (/ 1 l)) |
Compiled 639 893 to 85 464 computations (86.6% saved)
| Operator | Subexpression | Explanation | Count | |
|---|---|---|---|---|
sqrt.f64 | #f | oflow-rescue | 537 | 0 |
cos.f64 | #f | sensitivity | 517 | 4 |
-.f64 | #f | cancellation | 347 | 0 |
sqrt.f64 | #f | uflow-rescue | 335 | 0 |
/.f64 | #f | n/o | 260 | 0 |
acos.f64 | (acos.f64 (-.f64 #s(literal 1 binary64) x)) | sensitivity | 255 | 0 |
log.f64 | (log.f64 (/.f64 (sinh.f64 x) x)) | sensitivity | 249 | 0 |
tan.f64 | (tan.f64 (+.f64 y z)) | sensitivity | 180 | 0 |
pow.f64 | (pow.f64 l (exp.f64 w)) | sensitivity | 133 | 14 |
*.f64 | #f | n*u | 38 | 0 |
*.f64 | #f | n*o | 34 | 0 |
*.f64 | (*.f64 (pow.f64 c #s(literal 2 binary64)) (*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x)) | o*u | 17 | 0 |
| ↳ | (pow.f64 c #s(literal 2 binary64)) | overflow | 56 | |
| ↳ | (*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x) | underflow | 82 | |
| ↳ | (*.f64 x (pow.f64 s #s(literal 2 binary64))) | underflow | 79 | |
| ↳ | (pow.f64 s #s(literal 2 binary64)) | underflow | 68 | |
*.f64 | #f | u*o | 16 | 0 |
-.f64 | (-.f64 (*.f64 a a) (*.f64 b b)) | nan-rescue | 10 | 0 |
| ↳ | (*.f64 a a) | overflow | 112 | |
| ↳ | (*.f64 b b) | overflow | 10 | |
log.f64 | (log.f64 (/.f64 (sinh.f64 x) x)) | oflow-rescue | 6 | 0 |
| ↳ | (sinh.f64 x) | overflow | 6 | |
| ↳ | (/.f64 (sinh.f64 x) x) | overflow | 6 |
| Predicted + | Predicted - | |
|---|---|---|
| + | 2151 | 258 |
| - | 718 | 1993 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 2151 | 1 | 257 |
| - | 718 | 16 | 1977 |
| number | freq |
|---|---|
| 0 | 2251 |
| 1 | 2811 |
| 2 | 51 |
| 3 | 7 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 18 | 0 | 0 |
| - | 0 | 0 | 2 |
| 429.0ms | 2 438× | 1 | valid |
| 365.0ms | 6 628× | 0 | valid |
| 314.0ms | 1 088× | 2 | valid |
| 12.0ms | 86× | 1 | exit |
Compiled 1 067 to 440 computations (58.8% saved)
ival-sqrt: 100.0ms (12.4% of total)adjust: 87.0ms (10.8% of total)ival-sin: 79.0ms (9.8% of total)ival-tan: 76.0ms (9.4% of total)ival-cos: 67.0ms (8.3% of total)ival-log: 67.0ms (8.3% of total)ival-mult!: 50.0ms (6.2% of total)ival-exp: 47.0ms (5.8% of total)ival-sinh: 46.0ms (5.7% of total)ival-acos: 35.0ms (4.3% of total)ival-fmod: 27.0ms (3.3% of total)ival-pow: 24.0ms (3% of total)ival-div!: 23.0ms (2.8% of total)ival-sub!: 22.0ms (2.7% of total)ival-pow2: 21.0ms (2.6% of total)ival-add!: 19.0ms (2.4% of total)ival-hypot: 9.0ms (1.1% of total)ival-neg: 5.0ms (0.6% of total)ival-atan: 3.0ms (0.4% of total)| 20× | search |
| Probability | Valid | Unknown | Precondition | Infinite | Domain | Can't | Iter |
|---|---|---|---|---|---|---|---|
| 0% | 0% | 73.7% | 26.3% | 0% | 0% | 0% | 0 |
| 28.8% | 21.3% | 52.5% | 26.3% | 0% | 0% | 0% | 1 |
| 44.1% | 32.5% | 41.2% | 26.3% | 0% | 0% | 0% | 2 |
| 52.6% | 38.7% | 35% | 26.3% | 0% | 0% | 0% | 3 |
| 61.9% | 45.6% | 28.1% | 26.3% | 0% | 0% | 0% | 4 |
| 65.2% | 47.5% | 25.3% | 26.3% | 0% | 0.9% | 0% | 5 |
| 66.8% | 48.4% | 24% | 26.3% | 0% | 1.2% | 0% | 6 |
| 71.1% | 51.1% | 20.8% | 26.3% | 0% | 1.9% | 0% | 7 |
| 72.1% | 51.6% | 20% | 26.3% | 0% | 2.1% | 0% | 8 |
| 74.4% | 53% | 18.2% | 26.3% | 0% | 2.5% | 0% | 9 |
| 75.8% | 53.9% | 17.2% | 26.3% | 0% | 2.6% | 0% | 10 |
| 76.6% | 54.3% | 16.6% | 26.3% | 0% | 2.8% | 0% | 11 |
| 77.3% | 54.8% | 16.1% | 26.3% | 0% | 2.9% | 0% | 12 |
Compiled 279 to 216 computations (22.6% saved)
| 15× | node-limit |
| 5× | saturated |
Compiled 16 186 to 7 210 computations (55.5% saved)
Compiled 81 314 to 41 496 computations (49% saved)
| 44× | binary-search |
| 5× | left-value |
| 29× | narrow-enough |
| 9× | predicate-same |
| 6× | predicate-failed |
| 295.0ms | 1 637× | 1 | valid |
| 167.0ms | 1 291× | 0 | valid |
| 73.0ms | 606× | 0 | invalid |
Compiled 13 753 to 10 886 computations (20.8% saved)
ival-fmod: 102.0ms (24.7% of total)ival-tan: 70.0ms (16.9% of total)ival-cos: 65.0ms (15.7% of total)ival-exp: 46.0ms (11.1% of total)adjust: 35.0ms (8.5% of total)ival-sin: 24.0ms (5.8% of total)ival-mult!: 17.0ms (4.1% of total)ival-sqrt: 16.0ms (3.9% of total)ival-add!: 11.0ms (2.7% of total)ival-div!: 7.0ms (1.7% of total)ival-acos: 6.0ms (1.5% of total)ival-neg: 6.0ms (1.5% of total)ival-pow: 3.0ms (0.7% of total)ival-sub!: 3.0ms (0.7% of total)ival-pow2: 2.0ms (0.5% of total)Loading profile data...