Herbie run
| Date: | Wednesday, May 14th, 2025 |
|---|---|
| Commit: | 79007786 on artem-rules-updates |
| Seed: | 2025134 |
| 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: | 78 719.3 MB |
Time bar (total: 1.4min)
| 22.5s | 21 456× | 5 | exit |
| 7.2s | 109 933× | 0 | valid |
| 6.7s | 38 844× | 1 | valid |
| 5.0s | 16 343× | 2 | valid |
| 892.0ms | 5 908× | 0 | invalid |
| 314.0ms | 1 190× | 1 | exit |
| 118.0ms | 1 367× | 0 | exit |
ival-exp: 8.2s (23.3% of total)ival-cos: 4.9s (14% of total)adjust: 4.5s (12.8% of total)ival-pow: 3.9s (11.1% of total)ival-mult!: 2.0s (5.6% of total)ival-fmod: 1.9s (5.3% of total)ival-log: 1.9s (5.3% of total)ival-sqrt: 1.5s (4.3% of total)ival-tan: 1.4s (3.9% of total)ival-sinh: 1.2s (3.3% of total)ival-sin: 805.0ms (2.3% of total)ival-div!: 760.0ms (2.2% of total)ival-acos: 488.0ms (1.4% of total)ival-sub!: 438.0ms (1.2% of total)ival-pow2: 415.0ms (1.2% of total)ival-add!: 345.0ms (1% of total)ival-neg: 326.0ms (0.9% of total)ival-hypot: 139.0ms (0.4% of total)ival-<=: 61.0ms (0.2% of total)ival-atan: 49.0ms (0.1% 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)| 107× | iter-limit |
| 68× | saturated |
| 48× | node-limit |
| 17× | unsound |
55 calls:
| 733.0ms | x |
| 422.0ms | a |
| 319.0ms | y |
| 263.0ms | (tan.f64 a) |
| 248.0ms | r |
Compiled 1 674 to 2 222 computations (-32.7% saved)
| 11× | fuel |
| 9× | done |
Compiled 1 538 to 984 computations (36% saved)
| 19× | node-limit |
| 1× | saturated |
Compiled 14 849 to 12 906 computations (13.1% saved)
381 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 81.0ms | c | @ | -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)) (* (pow c 2) (* (* x (pow s 2)) x))) (/ 1 (* (* (* c s) s) c)) 1 (* (* (* c s) s) c) (* (* c s) s) (/ (cos (* 2 x)) (* (pow c 2) (* (* x (pow s 2)) x))) (/ 1 (* (* s (* (* c s) (* x x))) c)) (* (* s (* (* c s) (* x x))) c) (* s (* (* c s) (* x x))) (* (* c s) (* x x)) (* x x) (/ (cos (* 2 x)) (* (pow c 2) (* (* x (pow s 2)) x))) (* (/ 1 (* (* c s) x)) (/ 1 (* (* c s) x))) (/ 1 (* (* c s) x)) (/ (cos (+ x x)) (* (* (* (* (* s s) x) x) c) c)) (cos (+ x x)) (+ x x) (* (* (* (* (* s s) x) x) c) c) (* (* (* (* s s) x) x) c) (* (* (* s s) x) x) (* (* s s) x) (* s s)) |
| 72.0ms | c | @ | -inf | ((/ (+ (* (cos x) (cos x)) (* (neg (sin x)) (sin x))) (* (* (* c s) x) (* (* c s) x))) (+ (* (cos x) (cos x)) (* (neg (sin x)) (sin x))) (cos x) x (* (neg (sin x)) (sin x)) (neg (sin x)) (sin x) (* (* (* c s) x) (* (* c s) x)) (* (* c s) x) (* c s) c s (/ (cos (+ x x)) (* (* (* (* (* s s) x) x) c) c)) (/ -1 (* (* (* s s) c) c)) -1 (* (* (* s s) c) c) (* (* s s) c) (* s s) (/ (cos (* 2 x)) (* (pow c 2) (* (* x (pow s 2)) x))) (/ 1 (* (* (* s (* (* s x) x)) c) c)) 1 (* (* (* s (* (* s x) x)) c) c) (* (* s (* (* s x) x)) c) (* s (* (* s x) x)) (* (* s x) x) (* s x) (/ (cos (* 2 x)) (* (pow c 2) (* (* x (pow s 2)) x))) (* (/ 1 (* s c)) (/ 1 (* (* (* s c) x) x))) (/ 1 (* s c)) (* s c) (/ 1 (* (* (* s c) x) x)) (* (* (* s c) x) x) (* (* s c) x) (/ (/ (cos -2) (* s c)) (* (* (* s c) x) x)) (/ (cos -2) (* s c)) (cos -2) -2) |
| 71.0ms | x | @ | 0 | ((/ (- x lo) (- hi lo)) (+ (+ (- 1 (/ x lo)) (* (neg (/ (- x hi) lo)) (/ hi lo))) (/ hi lo)) (+ (neg (* (+ (* (/ (- x hi) lo) hi) (- x hi)) (/ 1 lo))) 1) (neg (* (+ (* (/ (- x hi) lo) hi) (- x hi)) (/ 1 lo))) (* (+ (* (/ (- x hi) lo) hi) (- x hi)) (/ 1 lo)) (+ (* (/ (- x hi) lo) hi) (- x hi)) (/ (- x hi) lo) (- x hi) x hi lo (/ 1 lo) 1 (/ (- x lo) (- hi lo)) (- x lo) (- hi lo) (/ (- x lo) (- hi lo)) (/ (+ (* (/ (- x lo) hi) lo) (- x lo)) hi) (+ (* (/ (- x lo) hi) lo) (- x lo)) (/ (- x lo) hi) (/ (- x lo) (- hi lo)) (+ (neg (/ (- (+ (* hi (- (/ x lo) (/ hi lo))) x) hi) lo)) 1) (neg (/ (- (+ (* hi (- (/ x lo) (/ hi lo))) x) hi) lo)) (/ (- (+ (* hi (- (/ x lo) (/ hi lo))) x) hi) lo) (- (+ (* hi (- (/ x lo) (/ hi lo))) x) hi) (+ (* hi (- (/ x lo) (/ hi lo))) x) (- (/ x lo) (/ hi lo)) (/ x lo) (/ hi lo) (/ (- x lo) (- hi lo)) (+ (+ (- 1 (/ x lo)) (/ (* (/ (- hi x) lo) hi) lo)) (/ hi lo)) (+ (- 1 (/ x lo)) (/ (* (/ (- hi x) lo) hi) lo)) (- 1 (/ x lo)) (/ (* (/ (- hi x) lo) hi) lo) (* (/ (- hi x) lo) hi) (/ (- hi x) lo) (- hi x)) |
| 65.0ms | a | @ | 0 | ((sqrt (* (+ a b) (- a b))) (+ a (* 1/2 (/ (* b (+ a (* -1 a))) a))) a (* 1/2 (/ (* b (+ a (* -1 a))) a)) 1/2 (/ (* b (+ a (* -1 a))) a) (* b (+ a (* -1 a))) b (+ a (* -1 a)) (* -1 a) -1 (sqrt (* (+ a b) (- a b))) (* (+ a b) (- a b)) (+ a b) (- a b) (sqrt (* (+ a b) (- a b))) (* (+ a b) (- a b)) (+ a b) (- a b) (* -1 b) (sqrt (* (+ a b) (- a b))) (* (+ a b) (- a b)) (- a b) (* b (- (/ a b) 1)) (- (/ a b) 1) (/ a b) 1 (sqrt (* (+ a b) (- a b))) (+ a (* b (+ (* -1/2 (/ (* b (+ 1 (* 1/4 (/ (pow (+ a (* -1 a)) 2) (pow a 2))))) a)) (* 1/2 (/ (+ a (* -1 a)) a))))) (* b (+ (* -1/2 (/ (* b (+ 1 (* 1/4 (/ (pow (+ a (* -1 a)) 2) (pow a 2))))) a)) (* 1/2 (/ (+ a (* -1 a)) a)))) (+ (* -1/2 (/ (* b (+ 1 (* 1/4 (/ (pow (+ a (* -1 a)) 2) (pow a 2))))) a)) (* 1/2 (/ (+ a (* -1 a)) a))) -1/2 (/ (* b (+ 1 (* 1/4 (/ (pow (+ a (* -1 a)) 2) (pow a 2))))) a) (* b (+ 1 (* 1/4 (/ (pow (+ a (* -1 a)) 2) (pow a 2))))) (+ 1 (* 1/4 (/ (pow (+ a (* -1 a)) 2) (pow a 2)))) (* 1/4 (/ (pow (+ a (* -1 a)) 2) (pow a 2))) 1/4 (/ (pow (+ a (* -1 a)) 2) (pow a 2)) (pow (+ a (* -1 a)) 2) 2 (pow a 2) (* 1/2 (/ (+ a (* -1 a)) a)) (/ (+ a (* -1 a)) a)) |
| 61.0ms | l | @ | inf | ((* (exp (neg w)) (pow l (exp w))) (exp (neg w)) (neg w) w (pow l (exp w)) l (exp w)) |
| 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)
Compiled 158 668 to 60 546 computations (61.8% saved)
Compiled 44 922 to 38 119 computations (15.1% saved)
| 36× | left-value |
| 31× | binary-search |
| 30× | narrow-enough |
| 1× | predicate-same |
| 193.0ms | 1 790× | 0 | valid |
| 154.0ms | 818× | 1 | valid |
| 1.0ms | 8× | 0 | exit |
Compiled 8 338 to 8 488 computations (-1.8% saved)
ival-tan: 82.0ms (37.3% of total)ival-cos: 28.0ms (12.7% of total)ival-exp: 27.0ms (12.3% of total)adjust: 21.0ms (9.5% of total)ival-pow: 18.0ms (8.2% of total)ival-mult!: 10.0ms (4.5% of total)ival-add!: 9.0ms (4.1% of total)ival-neg: 6.0ms (2.7% of total)ival-sin: 5.0ms (2.3% of total)ival-div!: 4.0ms (1.8% of total)ival-fmod: 4.0ms (1.8% of total)ival-sub!: 3.0ms (1.4% of total)ival-pow2: 2.0ms (0.9% of total)ival-sqrt: 1.0ms (0.5% of total)Loading profile data...