Herbie run
| Date: | Friday, April 25th, 2025 |
|---|---|
| Commit: | e1b60cb6 on time-nightly |
| Seed: | 2025115 |
| 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: | 940 982.1 MB |
Time bar (total: 13.3min)
| 2.5min | 2 144 791× | 0 | valid |
| 21.0s | 69 316× | 1 | valid |
| 6.8s | 64 570× | 0 | invalid |
| 1.3s | 6 065× | 2 | valid |
| 896.0ms | 1 196× | 5 | exit |
| 413.0ms | 1 889× | 1 | invalid |
| 252.0ms | 440× | 4 | exit |
| 156.0ms | 689× | 3 | valid |
| 3.0ms | 31× | 1 | exit |
| 1.0ms | 3× | 4 | valid |
ival-mult!: 39.5s (38% of total)ival-sub!: 12.4s (12% of total)ival-div!: 10.6s (10.2% of total)ival-add!: 9.4s (9% of total)ival-log: 8.2s (7.9% of total)ival-cos: 6.5s (6.2% of total)ival-sqrt: 6.3s (6.1% of total)adjust: 4.0s (3.8% of total)ival-sin: 3.9s (3.7% of total)ival-exp: 1.8s (1.7% of total)ival-acos: 272.0ms (0.3% of total)ival-tan: 268.0ms (0.3% of total)ival-cosh: 244.0ms (0.2% of total)ival-fabs: 187.0ms (0.2% of total)ival-sinh: 164.0ms (0.2% of total)ival-hypot: 164.0ms (0.2% of total)ival-tanh: 96.0ms (0.1% of total)| 2 201× | iter-limit |
| 836× | node-limit |
| 71× | unsound |
| 14× | saturated |
512 calls:
| 10.7s | x |
| 9.3s | z |
| 8.9s | y |
| 3.9s | t |
| 2.5s | (*.f64 x y) |
Compiled 33 612 to 56 035 computations (-66.7% saved)
| 140× | fuel |
| 129× | done |
Compiled 30 582 to 18 567 computations (39.3% saved)
| 174× | node-limit |
| 95× | saturated |
Compiled 142 957 to 113 259 computations (20.8% saved)
8808 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 1.0s | y | @ | 0 | ((+ (+ (+ (+ (+ (* x (log y)) z) t) a) (* (- b 1/2) (log c))) (* y i)) (+ (+ (+ (+ (* x (log y)) z) t) a) (* (- b 1/2) (log c))) (+ (+ (+ (* x (log y)) z) t) a) (+ (+ (* x (log y)) z) t) (+ (* (log y) x) z) (log y) y x z a (* (- b 1/2) (log c)) (- b 1/2) b 1/2 (log c) c (* y i) i (+ (+ (+ (+ (+ (* x (log y)) z) t) a) (* (- b 1/2) (log c))) (* y i)) (+ (+ (+ (+ (+ (* x (log y)) z) t) a) (* (- b 1/2) (log c))) (* y i)) (+ (+ (+ (+ (* x (log y)) z) t) a) (* (- b 1/2) (log c))) (+ (+ (+ (+ (+ (* x (log y)) z) t) a) (* (- b 1/2) (log c))) (* y i)) (+ (+ (+ (+ (* x (log y)) z) t) a) (* (- b 1/2) (log c))) (+ (+ (+ (* x (log y)) z) t) a) (+ (+ (+ (+ (+ (* x (log y)) z) t) a) (* (- b 1/2) (log c))) (* y i)) (* (neg i) (+ (neg (/ (+ (+ (+ (+ (* (log c) (- b 1/2)) (* (log y) x)) z) t) a) i)) (neg y))) (neg i) (+ (neg (/ (+ (+ (+ (+ (* (log c) (- b 1/2)) (* (log y) x)) z) t) a) i)) (neg y)) (neg (/ (+ (+ (+ (+ (* (log c) (- b 1/2)) (* (log y) x)) z) t) a) i)) (/ (+ (+ (+ (+ (* (log c) (- b 1/2)) (* (log y) x)) z) t) a) i) (+ (+ (+ (+ (* (log c) (- b 1/2)) (* (log y) x)) z) t) a) (+ (+ (+ (* (log c) (- b 1/2)) (* (log y) x)) z) t) (+ (+ (* (log c) (- b 1/2)) (* (log y) x)) z) (+ (* (log c) (- b 1/2)) (* (log y) x)) (* (log y) x) t (neg y)) |
| 394.0ms | z | @ | -inf | ((+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (+ (log (+ x y)) (log z)) t) (+ (log (+ x y)) (log z)) (log (+ x y)) (+ x y) x y (log z) z t (* (- a 1/2) (log t)) (- a 1/2) a 1/2 (log t)) |
| 371.0ms | t | @ | inf | ((* (* (- (* x 1/2) y) (sqrt (* z 2))) (pow (exp t) (/ t 2))) (* (- (* x 1/2) y) (sqrt (* z 2))) (- (* x 1/2) y) (* x 1/2) x 1/2 y (sqrt (* z 2)) (* z 2) z 2 (pow (exp t) (/ t 2)) (exp t) t (/ t 2) (* (* (- (* x 1/2) y) (sqrt (* z 2))) (exp (/ (* t t) 2))) (* (sqrt (+ z z)) (- (* 1/2 x) y)) (sqrt (+ z z)) (+ z z) (- (* 1/2 x) y) (* 1/2 x) (* (* (- (* x 1/2) y) (sqrt (* z 2))) (exp (/ (* t t) 2))) (* (neg (sqrt (* (+ z z) (exp (* t t))))) y) (neg (sqrt (* (+ z z) (exp (* t t))))) (sqrt (* (+ z z) (exp (* t t)))) (* (+ z z) (exp (* t t))) (exp (* t t)) (* t t) (* (* (* (sqrt 2) (- (* 1/2 x) y)) (sqrt (exp (* t t)))) (sqrt z)) (* (* (sqrt 2) (- (* 1/2 x) y)) (sqrt (exp (* t t)))) (* (sqrt 2) (- (* 1/2 x) y)) (sqrt 2) (sqrt (exp (* t t))) (sqrt z) (* (* (- (* x 1/2) y) (sqrt (* z 2))) (exp (/ (* t t) 2))) (* (- (* x 1/2) y) (sqrt (* z 2))) (- (* x 1/2) y) (* (+ (* (/ x y) 1/2) -1) y) (+ (* (/ x y) 1/2) -1) (/ x y) -1 (exp (/ (* t t) 2)) (/ (* t t) 2)) |
| 302.0ms | y | @ | 0 | ((+ (* a 120) (/ (* (- x y) 60) (- z t))) a 120 (/ (* (- x y) 60) (- z t)) (* (- x y) 60) (- x y) x y 60 (- z t) z t (+ (/ (* 60 (- x y)) (- z t)) (* a 120)) (* 120 a) (+ (/ (* 60 (- x y)) (- z t)) (* a 120)) (* (/ y (- z t)) -60) (/ y (- z t)) -60 (+ (/ (* 60 (- x y)) (- z t)) (* a 120)) (+ (* (/ y (- z t)) -60) (* 120 a)) (+ (/ (* 60 (- x y)) (- z t)) (* a 120)) (+ (* (/ (- x y) z) 60) (* 120 a)) (/ (- x y) z)) |
| 185.0ms | x | @ | 0 | ((+ (+ (+ (+ (+ (* x (log y)) z) t) a) (* (- b 1/2) (log c))) (* y i)) (+ (+ (+ (+ (* x (log y)) z) t) a) (* (- b 1/2) (log c))) (+ (+ (+ (* x (log y)) z) t) a) (+ (+ (* x (log y)) z) t) (+ (* (log y) x) z) (log y) y x z a (* (- b 1/2) (log c)) (- b 1/2) b 1/2 (log c) c (* y i) i (+ (+ (+ (+ (+ (* x (log y)) z) t) a) (* (- b 1/2) (log c))) (* y i)) (+ (+ (+ (+ (+ (* x (log y)) z) t) a) (* (- b 1/2) (log c))) (* y i)) (+ (+ (+ (+ (* x (log y)) z) t) a) (* (- b 1/2) (log c))) (+ (+ (+ (+ (+ (* x (log y)) z) t) a) (* (- b 1/2) (log c))) (* y i)) (+ (+ (+ (+ (* x (log y)) z) t) a) (* (- b 1/2) (log c))) (+ (+ (+ (* x (log y)) z) t) a) (+ (+ (+ (+ (+ (* x (log y)) z) t) a) (* (- b 1/2) (log c))) (* y i)) (* (neg i) (+ (neg (/ (+ (+ (+ (+ (* (log c) (- b 1/2)) (* (log y) x)) z) t) a) i)) (neg y))) (neg i) (+ (neg (/ (+ (+ (+ (+ (* (log c) (- b 1/2)) (* (log y) x)) z) t) a) i)) (neg y)) (neg (/ (+ (+ (+ (+ (* (log c) (- b 1/2)) (* (log y) x)) z) t) a) i)) (/ (+ (+ (+ (+ (* (log c) (- b 1/2)) (* (log y) x)) z) t) a) i) (+ (+ (+ (+ (* (log c) (- b 1/2)) (* (log y) x)) z) t) a) (+ (+ (+ (* (log c) (- b 1/2)) (* (log y) x)) z) t) (+ (+ (* (log c) (- b 1/2)) (* (log y) x)) z) (+ (* (log c) (- b 1/2)) (* (log y) x)) (* (log y) x) t (neg y)) |
Compiled 2 923 662 to 937 407 computations (67.9% saved)
| 1 837× | binary-search |
| 1 165× | left-value |
| 1 801× | narrow-enough |
| 36× | predicate-same |
| 12.1s | 141 031× | 0 | valid |
| 677.0ms | 3 770× | 1 | valid |
| 216.0ms | 2 691× | 0 | invalid |
| 49.0ms | 13× | 3 | valid |
| 34.0ms | 226× | 2 | valid |
| 5.0ms | 22× | 1 | invalid |
Compiled 691 247 to 698 492 computations (-1% saved)
ival-mult!: 3.7s (48.4% of total)ival-sub!: 1.2s (15.2% of total)ival-div!: 674.0ms (8.9% of total)ival-add!: 641.0ms (8.5% of total)ival-sin: 440.0ms (5.8% of total)ival-log: 393.0ms (5.2% of total)adjust: 224.0ms (3% of total)ival-cos: 190.0ms (2.5% of total)ival-sqrt: 70.0ms (0.9% of total)ival-exp: 69.0ms (0.9% of total)ival-fabs: 31.0ms (0.4% of total)ival-cosh: 8.0ms (0.1% of total)ival-sinh: 6.0ms (0.1% of total)ival-tanh: 5.0ms (0.1% of total)Compiled 495 812 to 431 807 computations (12.9% saved)
| 269× | search |
| Probability | Valid | Unknown | Precondition | Infinite | Domain | Can't | Iter |
|---|---|---|---|---|---|---|---|
| 0% | 0% | 99.9% | 0.1% | 0% | 0% | 0% | 0 |
| 46.8% | 46.8% | 53.1% | 0.1% | 0% | 0% | 0% | 1 |
| 50.5% | 50.1% | 49.2% | 0.1% | 0% | 0.6% | 0% | 2 |
| 58.6% | 57% | 40.3% | 0.1% | 0% | 2.6% | 0% | 3 |
| 65.2% | 62.7% | 33.5% | 0.1% | 0% | 3.6% | 0% | 4 |
| 71.2% | 68.2% | 27.5% | 0.1% | 0% | 4.1% | 0% | 5 |
| 75.9% | 72.3% | 23% | 0.1% | 0% | 4.6% | 0% | 6 |
| 79.8% | 75.6% | 19.1% | 0.1% | 0% | 5.1% | 0% | 7 |
| 81.7% | 77% | 17.3% | 0.1% | 0% | 5.6% | 0% | 8 |
| 84.3% | 79.3% | 14.7% | 0.1% | 0% | 5.9% | 0% | 9 |
| 85.9% | 80.5% | 13.2% | 0.1% | 0% | 6.2% | 0% | 10 |
| 88.5% | 82.8% | 10.8% | 0.1% | 0% | 6.2% | 0% | 11 |
| 89.6% | 83.6% | 9.8% | 0.1% | 0% | 6.5% | 0% | 12 |
Compiled 3 462 to 2 977 computations (14% saved)
Loading profile data...