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: | 73 390.5 MB |
Time bar (total: 1.2min)
| 18.9s | 20 948× | 5 | exit |
| 6.8s | 39 043× | 1 | valid |
| 6.2s | 109 769× | 0 | valid |
| 4.6s | 16 308× | 2 | valid |
| 567.0ms | 5 787× | 0 | invalid |
| 295.0ms | 1 168× | 1 | exit |
| 159.0ms | 1 470× | 0 | exit |
| 1.0ms | 1× | 3 | exit |
ival-exp: 6.3s (20.4% of total)ival-cos: 4.4s (14.4% of total)adjust: 4.4s (14.2% of total)ival-pow: 3.5s (11.4% of total)ival-log: 1.7s (5.6% of total)ival-tan: 1.7s (5.4% of total)ival-sqrt: 1.5s (5% of total)ival-mult!: 1.5s (4.7% of total)ival-sinh: 1.2s (3.8% of total)ival-fmod: 1.1s (3.6% of total)ival-sin: 696.0ms (2.3% of total)ival-div!: 684.0ms (2.2% of total)ival-acos: 545.0ms (1.8% of total)ival-add!: 415.0ms (1.3% of total)ival-pow2: 358.0ms (1.2% of total)ival-sub!: 343.0ms (1.1% of total)ival-neg: 239.0ms (0.8% of total)ival-hypot: 143.0ms (0.5% of total)ival-<=: 57.0ms (0.2% of total)ival-atan: 51.0ms (0.2% of total)ival-and: 31.0ms (0.1% of total)ival-or: 14.0ms (0% of total)ival-assert: 3.0ms (0% of total)ival->: 2.0ms (0% of total)ival-<: 2.0ms (0% of total)| 175× | iter-limit |
| 48× | node-limit |
| 15× | unsound |
| 4× | saturated |
53 calls:
| 623.0ms | c |
| 540.0ms | x |
| 429.0ms | a |
| 315.0ms | b |
| 238.0ms | r |
Compiled 1 500 to 1 974 computations (-31.6% saved)
| 10× | fuel |
| 10× | done |
Compiled 1 378 to 910 computations (34% saved)
| 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)
372 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 61.0ms | x | @ | 0 | ((/ (- x lo) (- hi lo)) (+ (- 1 (/ x lo)) (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ hi lo))) (- 1 (/ x lo)) 1 (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ hi lo)) (/ hi lo) hi lo (/ (- x hi) (neg lo)) (- x hi) x (neg lo) (/ (- x lo) (- hi lo)) (+ (+ (- 1 (/ x lo)) (* (neg (/ (- x hi) lo)) (/ hi lo))) (/ hi lo)) (- 1 (/ x lo)) (/ x lo) (/ (- x lo) (- hi lo)) (+ (/ hi lo) (- (- 1 (/ x lo)) (* (/ (- x hi) lo) (/ hi lo)))) (- (- 1 (/ x lo)) (* (/ (- x hi) lo) (/ hi lo))) (* (/ (- x hi) lo) (/ hi lo)) (/ (- x hi) lo) (/ (- x lo) (- hi lo)) (+ (+ (- 1 (/ x lo)) (* (neg (/ (- x hi) lo)) (/ hi lo))) (/ hi lo)) (+ (- 1 (/ x lo)) (* (neg (/ (- x hi) lo)) (/ hi lo))) (* (neg (/ (- x hi) lo)) (/ hi lo)) (neg (/ (- x hi) lo)) (/ (- x hi) lo) (* (/ (- (/ x hi) 1) lo) hi) (/ (- (/ x hi) 1) lo) (- (/ x hi) 1) (/ x hi) (/ (- x lo) (- hi lo)) (+ (/ (- (* (- 1 (/ x lo)) (- 1 (/ x lo))) (* (* (/ (- x hi) lo) (/ hi lo)) (* (/ (- x hi) lo) (/ hi lo)))) (- (- 1 (/ x lo)) (* (/ hi lo) (/ (- x hi) (neg lo))))) (/ hi lo)) (/ (- (* (- 1 (/ x lo)) (- 1 (/ x lo))) (* (* (/ (- x hi) lo) (/ hi lo)) (* (/ (- x hi) lo) (/ hi lo)))) (- (- 1 (/ x lo)) (* (/ hi lo) (/ (- x hi) (neg lo))))) (- (* (- 1 (/ x lo)) (- 1 (/ x lo))) (* (* (/ (- x hi) lo) (/ hi lo)) (* (/ (- x hi) lo) (/ hi lo)))) (* (- 1 (/ x lo)) (- 1 (/ x lo))) (* (* (/ (- x hi) lo) (/ hi lo)) (* (/ (- x hi) lo) (/ hi lo))) (- (- 1 (/ x lo)) (* (/ hi lo) (/ (- x hi) (neg lo)))) (* (/ hi lo) (/ (- x hi) (neg lo)))) |
| 56.0ms | x | @ | inf | ((log (/ (sinh x) x)) (* (+ (* (+ (* (* x x) 1/2835) -1/180) (* (* x x) x)) (* 1/6 x)) x) (+ (* (+ (* (* x x) 1/2835) -1/180) (* (* x x) x)) (* 1/6 x)) (+ (* (* x x) 1/2835) -1/180) (* x x) x 1/2835 -1/180 (* (* x x) x) (* 1/6 x) 1/6 (log (/ (sinh x) x)) (* (* x x) 1/6) (log (/ (sinh x) x)) (/ (sinh x) x) (+ (* (+ (* 1/120 (* x x)) 1/6) (* x x)) 1) (* (* (* (* x x) 1/120) x) x) (* (* (* x x) 1/120) x) (* (* x x) 1/120) 1/120 (log (/ (sinh x) x)) (/ (sinh x) x) (+ (* (* (+ (* (+ (* 1/5040 (* x x)) 1/120) (* x x)) 1/6) x) x) 1) (* (* 1/5040 (* (* x x) x)) (* (* x x) x)) (* 1/5040 (* (* x x) x)) 1/5040 (- (log (sinh (neg x))) (log (neg x))) (log (sinh (neg x))) (sinh (neg x)) (neg x) (log (neg x))) |
| 47.0ms | hi | @ | 0 | ((/ (- x lo) (- hi lo)) (+ (+ (- 1 (/ x lo)) (* (neg (/ (- x hi) lo)) (/ hi lo))) (/ hi lo)) (+ (- 1 (/ x lo)) (* (neg (/ (- x hi) lo)) (/ hi lo))) (- 1 (/ x lo)) 1 (* (neg (/ (- x hi) lo)) (/ hi lo)) (neg (/ (- x hi) lo)) (/ (- x hi) lo) (- x hi) x hi lo (/ hi lo) (/ (- x lo) (- hi lo)) (+ (* (neg lo) (+ (/ 1 hi) (/ (neg x) (* hi hi)))) (/ x hi)) (/ (neg lo) hi) (neg lo) (/ (- x lo) (- hi lo)) (/ (+ (* (/ (- x lo) hi) lo) (- x lo)) hi) (+ (* (/ (- x lo) hi) lo) (- x lo)) (/ (- x lo) hi) (- x lo) (/ (- x lo) (- hi lo)) (+ (+ (- 1 (/ x lo)) (* (neg (/ (- x hi) lo)) (/ hi lo))) (/ hi lo)) (+ (- 1 (/ x lo)) (* (neg (/ (- x hi) lo)) (/ hi lo))) (- 1 (/ x lo)) (/ (neg x) lo) (neg x) (/ (- x lo) (- hi lo)) (+ (* (neg lo) (+ (exp (* (log hi) -1)) (/ (neg x) (* hi hi)))) (/ x hi)) (+ (exp (* (log hi) -1)) (/ (neg x) (* hi hi))) (exp (* (log hi) -1)) (* (log hi) -1) (log hi) -1 (/ (neg x) (* hi hi)) (* hi hi) (/ x hi)) |
| 45.0ms | z | @ | 0 | ((+ x (- (+ (/ (tan y) (- 1 (* (tan y) (/ (sin z) (cos z))))) (/ (tan z) (- 1 (* (tan y) (tan z))))) (tan a))) x (- (+ (/ (tan y) (- 1 (* (tan y) (/ (sin z) (cos z))))) (/ (tan z) (- 1 (* (tan y) (tan z))))) (tan a)) (+ (/ (tan y) (- 1 (* (tan y) (/ (sin z) (cos z))))) (/ (tan z) (- 1 (* (tan y) (tan z))))) (/ (tan y) (- 1 (* (tan y) (/ (sin z) (cos z))))) (tan y) y (- 1 (* (tan y) (/ (sin z) (cos z)))) 1 (* (tan y) (/ (sin z) (cos z))) (/ (sin z) (cos z)) (sin z) z (cos z) (/ (tan z) (- 1 (* (tan y) (tan z)))) (tan z) (- 1 (* (tan y) (tan z))) (* (tan y) (tan z)) (tan a) a (+ x (- (tan (+ y z)) (tan a))) (- (tan (+ y z)) (tan a)) (tan (+ y z)) (+ y z) (tan a) (+ x (- (tan (+ y z)) (tan (+ (+ a (PI)) (PI))))) (- (tan (+ y z)) (tan (+ (+ a (PI)) (PI)))) (tan (+ y z)) (+ y z) (tan (+ (+ a (PI)) (PI))) (+ (+ a (PI)) (PI)) (+ a (PI)) (PI) (+ x (/ (sin (- (+ z y) a)) (* (sin (+ (+ z y) (/ (PI) 2))) (cos a)))) (/ (sin (- (+ z y) a)) (* (sin (+ (+ z y) (/ (PI) 2))) (cos a))) (sin (- (+ z y) a)) (- (+ z y) a) (+ z y) (* (sin (+ (+ z y) (/ (PI) 2))) (cos a)) (sin (+ (+ z y) (/ (PI) 2))) (+ (+ z y) (/ (PI) 2)) (/ (PI) 2) 2 (cos a) (+ x (- (/ (+ (tan z) (tan y)) (- 1 (* (tan z) (tan y)))) (tan a))) (- (/ (+ (tan z) (tan y)) (- 1 (* (tan z) (tan y)))) (tan a)) (/ (+ (tan z) (tan y)) (- 1 (* (tan z) (tan y)))) (+ (tan z) (tan y)) (- 1 (* (tan z) (tan y))) (* (tan z) (tan y))) |
| 44.0ms | r | @ | -inf | ((/ (* r (sin b)) (- (* (cos b) (cos a)) (* (sin b) (sin a)))) (* r (sin b)) r (sin b) b (- (* (cos b) (cos a)) (* (sin b) (sin a))) (* (cos b) (cos a)) (cos b) (cos a) a (* (sin b) (sin a)) (sin a) (/ (* r (sin b)) (cos (+ a b))) (* r (tan b)) (tan b) (/ (* r (sin b)) (cos (+ a b))) (cos (+ a b)) (+ a b) (/ (* r (sin b)) (cos (+ a b))) (cos (+ a b)) (+ a b) (* (+ (/ b a) 1) a) (+ (/ b a) 1) (/ b a) 1 (/ (* r (sin b)) (cos (+ a b))) (* (+ (* b (/ (* (sin a) r) (+ 1/2 (* 1/2 (cos (* 2 a)))))) (/ r (cos a))) b) (+ (* b (/ (* (sin a) r) (+ 1/2 (* 1/2 (cos (* 2 a)))))) (/ r (cos a))) (/ (* (sin a) r) (+ 1/2 (* 1/2 (cos (* 2 a))))) (* (sin a) r) (+ 1/2 (* 1/2 (cos (* 2 a)))) 1/2 (* 1/2 (cos (* 2 a))) (cos (* 2 a)) (* 2 a) 2 (/ r (cos a))) |
| 15× | node-limit |
| 5× | saturated |
Compiled 6 907 to 6 030 computations (12.7% saved)
Compiled 206 904 to 74 594 computations (63.9% saved)
Compiled 51 320 to 41 765 computations (18.6% saved)
| 35× | left-value |
| 20× | binary-search |
| 20× | narrow-enough |
| 212.0ms | 952× | 1 | valid |
| 105.0ms | 1 208× | 0 | valid |
| 1.0ms | 13× | 0 | exit |
Compiled 5 919 to 6 202 computations (-4.8% saved)
ival-cos: 52.0ms (21.4% of total)ival-tan: 49.0ms (20.1% of total)ival-sin: 41.0ms (16.8% of total)ival-div!: 35.0ms (14.4% of total)adjust: 22.0ms (9% of total)ival-mult!: 11.0ms (4.5% of total)ival-exp: 10.0ms (4.1% of total)ival-pow: 10.0ms (4.1% of total)ival-add!: 9.0ms (3.7% of total)ival-neg: 2.0ms (0.8% of total)ival-sub!: 1.0ms (0.4% of total)ival-pow2: 1.0ms (0.4% of total)Loading profile data...