Herbie run
| Date: | Monday, May 12th, 2025 |
|---|---|
| Commit: | 2ad78556 on artem-rules-updates |
| Seed: | 2025132 |
| 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: | 119 670.9 MB |
Time bar (total: 2.1min)
| 22.0s | 292 890× | 0 | valid |
| 7.6s | 17 836× | 2 | valid |
| 7.0s | 35 601× | 1 | valid |
| 480.0ms | 4 142× | 0 | invalid |
| 389.0ms | 1 002× | 0 | exit |
| 223.0ms | 425× | 3 | valid |
| 111.0ms | 101× | 4 | exit |
| 68.0ms | 101× | 3 | exit |
| 5.0ms | 43× | 1 | exit |
ival-mult!: 6.3s (24.6% of total)ival-div!: 3.1s (12.1% of total)ival-pow: 3.1s (12.1% of total)ival-sin: 2.4s (9.3% of total)ival-sub!: 2.3s (9.1% of total)adjust: 2.3s (9.1% of total)ival-add!: 1.8s (7% of total)ival-cos: 1.7s (6.6% of total)ival-sqrt: 544.0ms (2.1% of total)ival-pow2: 520.0ms (2% of total)ival-exp: 510.0ms (2% of total)ival-neg: 369.0ms (1.4% of total)ival-atan: 211.0ms (0.8% of total)ival-tan: 159.0ms (0.6% of total)ival-log1p: 112.0ms (0.4% of total)ival-expm1: 105.0ms (0.4% of total)ival-fabs: 33.0ms (0.1% of total)ival-hypot: 16.0ms (0.1% of total)ival-<=: 16.0ms (0.1% of total)ival-and: 8.0ms (0% of total)ival-if: 4.0ms (0% of total)ival-==: 2.0ms (0% of total)ival-assert: 1.0ms (0% of total)ival-<: 1.0ms (0% of total)const: 0.0ms (0% of total)| 255× | iter-limit |
| 113× | node-limit |
| 36× | unsound |
| 20× | saturated |
| 26× | done |
| 16× | fuel |
Compiled 3 895 to 2 062 computations (47.1% saved)
| 37× | node-limit |
| 5× | saturated |
Compiled 14 963 to 11 142 computations (25.5% saved)
90 calls:
| 442.0ms | x |
| 367.0ms | b |
| 311.0ms | c |
| 224.0ms | a |
| 172.0ms | r |
Compiled 5 108 to 4 385 computations (14.2% saved)
Compiled 398 287 to 128 563 computations (67.7% saved)
798 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 159.0ms | c | @ | -inf | ((/ (- (* b c) (* a d)) (+ (* c c) (* d d))) (* (- b (* (/ d c) a)) (/ 1 c)) (- b (* (/ d c) a)) b (* (/ d c) a) (/ d c) d c a (/ 1 c) 1 (/ (- (* b c) (* a d)) (+ (* c c) (* d d))) (* b (/ 1 c)) (/ (- (* b c) (* a d)) (+ (* c c) (* d d))) (/ (- (/ (* c b) d) a) d) (* b (/ c (* d d))) (/ c (* d d)) (* d d) (/ (- (* b c) (* a d)) (+ (* c c) (* d d))) (/ (- b (* a (/ d c))) c) (/ (* (neg a) d) (* c c)) (* (neg a) d) (neg a) (* c c) (/ 1 (/ (+ (* c c) (* d d)) (- (* b c) (* a d)))) (/ (+ (* c c) (* d d)) (- (* b c) (* a d))) (+ (* c c) (* d d)) (- (* b c) (* a d)) (* c b)) |
| 93.0ms | d | @ | -inf | ((* (+ a (+ b (+ c d))) 2) (* 2 (+ (+ (+ d c) a) b)) 2 (+ (+ (+ d c) a) b) (+ (+ d c) a) (* c (/ (+ 1 (pow (/ (+ a d) c) 3)) (+ 1 (- (* (/ (+ a d) c) (/ (+ a d) c)) (* 1 (/ (+ a d) c)))))) c (/ (+ 1 (pow (/ (+ a d) c) 3)) (+ 1 (- (* (/ (+ a d) c) (/ (+ a d) c)) (* 1 (/ (+ a d) c))))) (+ 1 (pow (/ (+ a d) c) 3)) 1 (pow (/ (+ a d) c) 3) (/ (+ a d) c) (+ a d) a d 3 (+ 1 (- (* (/ (+ a d) c) (/ (+ a d) c)) (* 1 (/ (+ a d) c)))) (- (* (/ (+ a d) c) (/ (+ a d) c)) (* 1 (/ (+ a d) c))) (* (/ (+ a d) c) (/ (+ a d) c)) (* 1 (/ (+ a d) c)) b (* (+ a (+ (+ c b) d)) 2) (+ a (+ (+ c b) d)) (+ (+ c b) d) (+ c b) (* (+ a (+ b (+ c d))) 2) (+ a (+ b (+ c d))) (+ (* (/ (+ (+ d b) a) c) c) c) (/ (+ (+ d b) a) c) (+ (+ d b) a) (+ d b) (* (+ a (+ b (+ c d))) 2) (* 2 (+ (+ (+ d c) a) b)) (+ (+ (+ d c) a) b) (+ (+ d c) a) (* a (+ 1 (/ (+ c d) a))) (+ 1 (/ (+ c d) a)) (/ (+ a (+ c d)) a) (+ a (+ c d)) (+ c d) (* (+ a (+ b (+ c d))) 2) (* 2 (+ (+ (+ d c) a) b)) (+ (+ (+ d c) a) b) (+ (+ d c) a) (* a (+ 1 (+ (/ c a) (/ d a)))) (+ 1 (+ (/ c a) (/ d a))) (+ (/ c a) (/ d a)) (/ c a) (/ d a)) |
| 72.0ms | v | @ | -inf | ((/ (* (neg t1) (/ v (+ u t1))) (+ u t1)) (* (neg t1) (/ v (+ u t1))) (neg t1) t1 (/ v (+ u t1)) v (+ u t1) u (/ (* (neg t1) v) (* (+ t1 u) (+ t1 u))) (* (neg v) (/ 1 t1)) (neg v) (/ 1 t1) 1 (* (neg t1) (/ v (* (+ u t1) (+ u t1)))) (/ v (* (+ u t1) (+ u t1))) (* (+ u t1) (+ u t1)) (+ u t1) (/ (/ (* v (neg t1)) (+ u t1)) (+ u t1)) (/ (* v (neg t1)) (+ u t1)) (/ (* v (neg t1)) u) (* v (neg t1)) (/ (* (neg t1) v) (* (+ t1 u) (+ t1 u))) (* (neg t1) v) (* (+ t1 u) (+ t1 u)) (* (+ (* 2 t1) u) u) (+ (* 2 t1) u) 2) |
| 67.0ms | eps | @ | -inf | ((- (pow (+ x eps) 5) (pow x 5)) (* (+ (* 5 (/ x eps)) 1) (pow eps 5)) (+ (* 5 (/ x eps)) 1) 5 (/ x eps) x eps 1 (pow eps 5) (- (pow (+ x eps) 5) (pow x 5)) (- (pow (+ x eps) 5) (pow x 5)) (* (* 5 (pow x 4)) eps) (* 5 (pow x 4)) (pow x 4) 4 (- (pow (+ x eps) 5) (pow x 5)) (* (+ (+ (* 4 eps) (neg (/ (+ (* -4 (* eps eps)) (neg (* (* eps eps) 6))) x))) eps) (pow x 4)) (+ (+ (* 4 eps) (neg (/ (+ (* -4 (* eps eps)) (neg (* (* eps eps) 6))) x))) eps) (+ (* 4 eps) (neg (/ (+ (* -4 (* eps eps)) (neg (* (* eps eps) 6))) x))) (neg (/ (+ (* -4 (* eps eps)) (neg (* (* eps eps) 6))) x)) (/ (+ (* -4 (* eps eps)) (neg (* (* eps eps) 6))) x) (+ (* -4 (* eps eps)) (neg (* (* eps eps) 6))) -4 (* eps eps) (neg (* (* eps eps) 6)) (* (* eps eps) 6) 6 (/ (- (pow (+ eps x) 10) (pow x 10)) (+ (pow (+ eps x) 5) (* (* x x) (* (* x x) x)))) (- (pow (+ eps x) 10) (pow x 10)) (pow (+ eps x) 10) (+ eps x) 10 (pow x 10) (+ (pow (+ eps x) 5) (* (* x x) (* (* x x) x))) (pow (+ eps x) 5) (* (* x x) (* (* x x) x)) (* x x) (* (* x x) x)) |
| 65.0ms | v | @ | -inf | ((* (/ (neg t1) (+ u t1)) (/ v (+ u t1))) (/ (neg t1) (+ u t1)) (neg t1) t1 (+ u t1) u (/ v (+ u t1)) v (/ (* (neg t1) v) (* (+ t1 u) (+ t1 u))) (/ (neg v) t1) (neg v) (/ (* (neg t1) v) (* (+ t1 u) (+ t1 u))) (* (neg t1) v) (* (+ t1 u) (+ t1 u)) (+ t1 u) (/ (* (neg t1) v) (* (+ t1 u) (+ t1 u))) (/ (+ (* (* u (/ v t1)) 2) (neg v)) t1) (+ (* (* u (/ v t1)) 2) (neg v)) (* u (/ v t1)) (/ v t1) 2 (/ (/ (* v (neg t1)) (+ u t1)) (+ u t1)) (/ (* v (neg t1)) (+ u t1)) (* v (neg t1))) |
| 43× | search |
| 2× | random |
| Probability | Valid | Unknown | Precondition | Infinite | Domain | Can't | Iter |
|---|---|---|---|---|---|---|---|
| 0% | 0% | 54.5% | 45.5% | 0% | 0% | 0% | 0 |
| 21.4% | 11.7% | 42.9% | 45.5% | 0% | 0% | 0% | 1 |
| 37.4% | 20.4% | 34.1% | 45.5% | 0% | 0% | 0% | 2 |
| 48.7% | 26.2% | 27.7% | 45.5% | 0% | 0.6% | 0% | 3 |
| 57.7% | 30.7% | 22.6% | 45.5% | 0% | 1.2% | 0% | 4 |
| 71.2% | 37.7% | 15.3% | 45.5% | 0% | 1.6% | 0% | 5 |
| 72.9% | 38.4% | 14.3% | 45.5% | 0% | 1.8% | 0% | 6 |
| 77.9% | 40.7% | 11.6% | 45.5% | 0% | 2.2% | 0% | 7 |
| 81.5% | 42.6% | 9.7% | 45.5% | 0% | 2.3% | 0% | 8 |
| 84.1% | 43.8% | 8.3% | 45.5% | 0% | 2.5% | 0% | 9 |
| 86.2% | 44.6% | 7.2% | 45.5% | 0% | 2.7% | 0% | 10 |
| 88.2% | 45.6% | 6.1% | 45.5% | 0% | 2.8% | 0% | 11 |
| 89.1% | 45.9% | 5.6% | 45.5% | 0% | 2.9% | 0% | 12 |
Compiled 1 402 to 721 computations (48.6% saved)
Compiled 62 268 to 47 053 computations (24.4% saved)
| 154× | binary-search |
| 51× | left-value |
| 144× | narrow-enough |
| 9× | predicate-same |
| 1× | predicate-failed |
| 826.0ms | 8 808× | 0 | valid |
| 258.0ms | 1 139× | 1 | valid |
| 201.0ms | 498× | 2 | valid |
| 68.0ms | 1 056× | 0 | invalid |
| 1.0ms | 3× | 3 | valid |
| 1.0ms | 6× | 1 | exit |
Compiled 67 378 to 55 804 computations (17.2% saved)
ival-mult!: 275.0ms (30.8% of total)ival-pow: 213.0ms (23.9% of total)ival-div!: 123.0ms (13.8% of total)adjust: 114.0ms (12.8% of total)ival-add!: 61.0ms (6.8% of total)ival-sub!: 52.0ms (5.8% of total)ival-neg: 28.0ms (3.1% of total)ival-sqrt: 24.0ms (2.7% of total)ival-log1p: 3.0ms (0.3% of total)Loading profile data...