Herbie run
| Date: | Saturday, May 31st, 2025 |
|---|---|
| Commit: | a88f6b81 on fighting-unsoundness |
| Seed: | 2025151 |
| 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: | 117 385.6 MB |
Time bar (total: 1.7min)
| 19.4s | 21 647× | 5 | exit |
| 8.0s | 109 717× | 0 | valid |
| 7.7s | 39 229× | 1 | valid |
| 5.1s | 16 174× | 2 | valid |
| 636.0ms | 6 030× | 0 | invalid |
| 162.0ms | 1 130× | 1 | exit |
| 102.0ms | 1 446× | 0 | exit |
ival-exp: 6.4s (19.2% of total)ival-cos: 4.9s (14.7% of total)adjust: 3.8s (11.5% of total)ival-pow: 3.1s (9.2% of total)ival-sqrt: 2.2s (6.5% of total)ival-log: 2.2s (6.5% of total)ival-tan: 1.9s (5.8% of total)ival-mult!: 1.4s (4.2% of total)ival-sinh: 1.4s (4.2% of total)ival-fmod: 1.2s (3.7% of total)ival-pow2: 1.1s (3.3% of total)ival-div!: 768.0ms (2.3% of total)ival-sin: 757.0ms (2.3% of total)ival-add!: 643.0ms (1.9% of total)ival-acos: 507.0ms (1.5% of total)ival-sub!: 465.0ms (1.4% of total)ival-neg: 194.0ms (0.6% of total)ival-hypot: 155.0ms (0.5% of total)ival-<=: 118.0ms (0.4% of total)ival-atan: 55.0ms (0.2% of total)ival-and: 30.0ms (0.1% of total)ival-or: 13.0ms (0% of total)ival-assert: 3.0ms (0% of total)ival->: 2.0ms (0% of total)ival-<: 2.0ms (0% of total)| 152× | iter-limit |
| 68× | node-limit |
| 5× | saturated |
| 3× | unsound |
Compiled 1 014 205 to 326 698 computations (67.8% saved)
53 calls:
| 1.1s | x |
| 760.0ms | a |
| 440.0ms | b |
| 395.0ms | (tan.f64 (+.f64 y z)) |
| 383.0ms | r |
Compiled 1 562 to 2 059 computations (-31.8% saved)
| 71× | iter-limit |
| 1× | saturated |
393 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 161.0ms | x | @ | inf | ((log (/ (sinh x) x)) (+ (* (* 1/6 x) x) (* (* (* (* x x) x) (+ (* 1/2835 (* x x)) -1/180)) x)) (* 1/6 x) 1/6 x (* (* (* (* x x) x) (+ (* 1/2835 (* x x)) -1/180)) x) (* (* (* x x) x) (+ (* 1/2835 (* x x)) -1/180)) (* (* x x) x) (* x x) (+ (* 1/2835 (* x x)) -1/180) 1/2835 -1/180 (log (/ (exp x) x)) (* -1 (log x)) -1 (log x) (log (/ (cosh x) x)) (/ (cosh x) x) (cosh x) (+ (log (/ -1 x)) (log (sinh (neg x)))) (log (/ -1 x)) (/ -1 x) (log (sinh (neg x))) (sinh (neg x)) (neg x) (log (/ (sinh x) x)) (/ (sinh x) x) (+ 1 (* (pow x 2) (+ 1/6 (* (pow x 2) (+ 1/120 (* 1/5040 (pow x 2))))))) 1 (* (pow x 2) (+ 1/6 (* (pow x 2) (+ 1/120 (* 1/5040 (pow x 2)))))) (pow x 2) 2 (+ 1/6 (* (pow x 2) (+ 1/120 (* 1/5040 (pow x 2))))) (* (pow x 2) (+ 1/120 (* 1/5040 (pow x 2)))) (+ 1/120 (* 1/5040 (pow x 2))) 1/120 (* 1/5040 (pow x 2)) 1/5040) |
| 105.0ms | r | @ | 0 | ((/ (* r (sin b)) (- (* (cos b) (cos a)) (* (sin a) (sin b)))) (* r (sin b)) r (sin b) b (- (* (cos b) (cos a)) (* (sin a) (sin b))) (* (cos b) (cos a)) (cos b) (cos a) a (* (sin a) (sin b)) (sin a) (/ (* r (sin b)) (cos (+ a b))) (/ 1 (/ (cos a) (* b r))) 1 (/ (cos a) (* b r)) (cos a) (* b r) (/ (* r (sin b)) (cos (+ a b))) (/ (* b r) (cos a)) (cos a) (+ 1 (* (pow a 2) (- (* (pow a 2) (+ 1/24 (* -1/720 (pow a 2)))) 1/2))) (* (pow a 2) (- (* (pow a 2) (+ 1/24 (* -1/720 (pow a 2)))) 1/2)) (pow a 2) 2 (- (* (pow a 2) (+ 1/24 (* -1/720 (pow a 2)))) 1/2) (* (pow a 2) (+ 1/24 (* -1/720 (pow a 2)))) (+ 1/24 (* -1/720 (pow a 2))) 1/24 (* -1/720 (pow a 2)) -1/720 1/2 (/ (* r (sin b)) (sin (- (- (* (PI) 1/2) a) b))) (sin (- (- (* (PI) 1/2) a) b)) (- (- (* (PI) 1/2) a) b) (- (* (PI) 1/2) a) (* (PI) 1/2) (PI) (* (/ (- (* (sin b) 1) (* (cos b) (sin (neg (+ (PI) (PI)))))) (cos (+ a b))) r) (/ (* r (- (sin b) (* (cos b) (sin (neg (* 2 (PI))))))) (cos (+ a b))) (* r (- (sin b) (* (cos b) (sin (neg (* 2 (PI))))))) (- (sin b) (* (cos b) (sin (neg (* 2 (PI)))))) (* (cos b) (sin (neg (* 2 (PI))))) (sin (neg (* 2 (PI)))) (neg (* 2 (PI))) (* 2 (PI)) (cos (+ a b)) (+ a b)) |
| 91.0ms | lo | @ | 0 | ((/ (- x lo) (- hi lo)) (- x lo) x lo (- hi lo) hi) |
| 75.0ms | x | @ | -inf | ((log (/ (sinh x) x)) (+ (* (* 1/6 x) x) (* (* (* (* x x) x) (+ (* 1/2835 (* x x)) -1/180)) x)) (* 1/6 x) 1/6 x (* (* (* (* x x) x) (+ (* 1/2835 (* x x)) -1/180)) x) (* (* (* x x) x) (+ (* 1/2835 (* x x)) -1/180)) (* (* x x) x) (* x x) (+ (* 1/2835 (* x x)) -1/180) 1/2835 -1/180 (log (/ (exp x) x)) (* -1 (log x)) -1 (log x) (log (/ (cosh x) x)) (/ (cosh x) x) (cosh x) (+ (log (/ -1 x)) (log (sinh (neg x)))) (log (/ -1 x)) (/ -1 x) (log (sinh (neg x))) (sinh (neg x)) (neg x) (log (/ (sinh x) x)) (/ (sinh x) x) (+ 1 (* (pow x 2) (+ 1/6 (* (pow x 2) (+ 1/120 (* 1/5040 (pow x 2))))))) 1 (* (pow x 2) (+ 1/6 (* (pow x 2) (+ 1/120 (* 1/5040 (pow x 2)))))) (pow x 2) 2 (+ 1/6 (* (pow x 2) (+ 1/120 (* 1/5040 (pow x 2))))) (* (pow x 2) (+ 1/120 (* 1/5040 (pow x 2)))) (+ 1/120 (* 1/5040 (pow x 2))) 1/120 (* 1/5040 (pow x 2)) 1/5040) |
| 66.0ms | hi | @ | -inf | ((/ (- x lo) (- hi lo)) (+ (* -1 (/ (- x lo) lo)) (* hi (- (+ (+ (* (/ lo -1) (/ 1 (* lo lo))) (/ 2 lo)) (/ (* hi (- (+ (* (/ lo -1) (/ 1 (* lo lo))) (/ 2 lo)) (/ x (pow lo 2)))) lo)) (/ x (pow lo 2))))) -1 (/ (- x lo) lo) (- x lo) x lo (* hi (- (+ (+ (* (/ lo -1) (/ 1 (* lo lo))) (/ 2 lo)) (/ (* hi (- (+ (* (/ lo -1) (/ 1 (* lo lo))) (/ 2 lo)) (/ x (pow lo 2)))) lo)) (/ x (pow lo 2)))) hi (- (+ (+ (* (/ lo -1) (/ 1 (* lo lo))) (/ 2 lo)) (/ (* hi (- (+ (* (/ lo -1) (/ 1 (* lo lo))) (/ 2 lo)) (/ x (pow lo 2)))) lo)) (/ x (pow lo 2))) (+ (+ (* (/ lo -1) (/ 1 (* lo lo))) (/ 2 lo)) (/ (* hi (- (+ (* (/ lo -1) (/ 1 (* lo lo))) (/ 2 lo)) (/ x (pow lo 2)))) lo)) (+ (* (/ lo -1) (/ 1 (* lo lo))) (/ 2 lo)) (/ lo -1) (/ 1 (* lo lo)) 1 (* lo lo) (/ 2 lo) 2 (/ (* hi (- (+ (* (/ lo -1) (/ 1 (* lo lo))) (/ 2 lo)) (/ x (pow lo 2)))) lo) (* hi (- (+ (* (/ lo -1) (/ 1 (* lo lo))) (/ 2 lo)) (/ x (pow lo 2)))) (- (+ (* (/ lo -1) (/ 1 (* lo lo))) (/ 2 lo)) (/ x (pow lo 2))) (/ x (pow lo 2)) (pow lo 2) (/ (- x lo) (- hi lo)) (+ 1 (* -1 (/ (- x hi) lo))) (+ 1 (/ hi lo)) (/ hi lo) (/ (- x lo) (- hi lo)) (+ 1 (* -1 (/ (- x hi) lo))) (* x (- (+ (/ 1 x) (/ hi (* lo x))) (/ 1 lo))) (- (+ (/ 1 x) (/ hi (* lo x))) (/ 1 lo)) (+ (/ 1 x) (/ hi (* lo x))) (/ 1 x) (/ hi (* lo x)) (* lo x) (/ 1 lo) (/ (- x lo) (- hi lo)) (+ (* -1 (* lo (+ (* -1 (/ x (pow hi 2))) (/ 1 hi)))) (/ x hi)) (* x (+ (* -1 (/ lo (* hi x))) (+ (/ 1 hi) (/ lo (pow hi 2))))) (+ (* -1 (/ lo (* hi x))) (+ (/ 1 hi) (/ lo (pow hi 2)))) (/ lo (* hi x)) (* hi x) (+ (/ 1 hi) (/ lo (pow hi 2))) (/ 1 hi) (/ lo (pow hi 2)) (pow hi 2) (/ (- x lo) (- hi lo)) (+ (* -1 (/ (- x lo) lo)) (* hi (- (+ (/ 1 lo) (/ (* (/ (- lo x) lo) (/ hi lo)) lo)) (/ x (pow lo 2))))) (* hi (- (+ (/ 1 lo) (/ (* (/ (- lo x) lo) (/ hi lo)) lo)) (/ x (pow lo 2)))) (- (+ (/ 1 lo) (/ (* (/ (- lo x) lo) (/ hi lo)) lo)) (/ x (pow lo 2))) (+ (/ 1 lo) (/ (* (/ (- lo x) lo) (/ hi lo)) lo)) (/ (* (/ (- lo x) lo) (/ hi lo)) lo) (* (/ (- lo x) lo) (/ hi lo)) (/ (- lo x) lo) (- lo x)) |
Compiled 64 761 to 51 818 computations (20% saved)
| 11× | fuel |
| 9× | done |
Compiled 1 407 to 876 computations (37.7% saved)
| 19× | node-limit |
| 1× | saturated |
Compiled 7 348 to 6 230 computations (15.2% 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)
| 24× | left-value |
| 15× | binary-search |
| 14× | narrow-enough |
| 1× | predicate-same |
| 128.0ms | 532× | 1 | valid |
| 19.0ms | 284× | 0 | valid |
Compiled 2 629 to 2 828 computations (-7.6% saved)
ival-cos: 80.0ms (64.7% of total)ival-sin: 14.0ms (11.3% of total)adjust: 11.0ms (8.9% of total)ival-div!: 5.0ms (4% of total)ival-mult!: 5.0ms (4% of total)ival-add!: 3.0ms (2.4% of total)ival-pow: 3.0ms (2.4% of total)ival-exp: 2.0ms (1.6% of total)ival-neg: 1.0ms (0.8% of total)ival-pow2: 0.0ms (0% of total)Loading profile data...