Herbie run
| Date: | Friday, May 16th, 2025 |
|---|---|
| Commit: | 7acd8706 on new-rules |
| Seed: | 2025136 |
| 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: | 1 026 098.4 MB |
Time bar (total: 14.3min)
| 2.8min | 2 144 398× | 0 | valid |
| 18.1s | 69 795× | 1 | valid |
| 9.9s | 63 926× | 0 | invalid |
| 1.8s | 5 945× | 2 | valid |
| 904.0ms | 1 216× | 5 | exit |
| 363.0ms | 1 770× | 1 | invalid |
| 234.0ms | 371× | 4 | exit |
| 207.0ms | 725× | 3 | valid |
| 4.0ms | 26× | 1 | exit |
| 0.0ms | 1× | 4 | valid |
ival-mult!: 34.1s (33.6% of total)ival-sub!: 13.1s (12.9% of total)ival-log: 12.5s (12.3% of total)ival-div!: 11.5s (11.3% of total)ival-add!: 9.9s (9.7% of total)ival-sqrt: 4.7s (4.7% of total)adjust: 4.4s (4.3% of total)ival-sin: 4.1s (4% of total)ival-cos: 3.3s (3.2% of total)ival-exp: 2.2s (2.2% of total)ival-fabs: 399.0ms (0.4% of total)ival-tan: 277.0ms (0.3% of total)ival-cosh: 276.0ms (0.3% of total)ival-sinh: 274.0ms (0.3% of total)ival-acos: 216.0ms (0.2% of total)ival-hypot: 149.0ms (0.1% of total)ival-tanh: 99.0ms (0.1% of total)| 2 221× | iter-limit |
| 877× | node-limit |
| 71× | unsound |
| 13× | saturated |
512 calls:
| 10.1s | x |
| 9.2s | t |
| 9.0s | y |
| 6.6s | z |
| 2.7s | a |
Compiled 32 728 to 54 805 computations (-67.5% saved)
| 155× | fuel |
| 114× | done |
Compiled 30 255 to 18 824 computations (37.8% saved)
| 253× | node-limit |
| 16× | saturated |
Compiled 137 810 to 111 340 computations (19.2% saved)
9099 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 2.2s | z | @ | inf | ((+ (* (/ (- t z) (- t a)) y) x) (/ (- t z) (- t a)) (/ (- t z) t) (- t z) t z y x (+ x (/ (* y (- z t)) (- a t))) (+ (* y (/ z a)) x) (/ (* y z) a) (* y z) a (+ x (/ (* y (- z t)) (- a t))) (* y (/ z (- a t))) (/ z (- a t)) (/ (neg z) t) (neg z) (+ x (/ (* y (- z t)) (- a t))) (/ (* y z) (- a t)) (- a t) (+ x (/ (* y (- z t)) (- a t))) (/ (* (- z t) y) (- a t)) (* (- z t) y) (- z t)) |
| 204.0ms | y | @ | 0 | ((+ (- (- (* x (log y)) y) z) (log t)) (- (+ (* (log y) x) (log t)) z) (+ (* (log y) x) (log t)) (log y) y x (log t) t z (+ (- (- (* x (log y)) y) z) (log t)) (* (+ (log y) (/ (- (- (log t) y) z) x)) x) (+ (log y) (/ (- (- (log t) y) z) x)) (/ (neg z) x) (neg z) (+ (- (- (* x (log y)) y) z) (log t)) (- (- (log t) y) z) (- (log t) y) (+ (- (- (* x (log y)) y) z) (log t)) (- (log (* (pow y x) t)) y) (log (* (pow y x) t)) (* (pow y x) t) (pow y x) (+ (- (- (* x (log y)) y) z) (log t)) (- (- (* x (log y)) y) z) (* (+ (* x (/ (log y) z)) (- -1 (/ y z))) z) (+ (* x (/ (log y) z)) (- -1 (/ y z))) (* (- (- (/ (neg (* (neg (log y)) x)) (* z y)) (/ 1 y)) (/ 1 z)) y) (- (- (/ (neg (* (neg (log y)) x)) (* z y)) (/ 1 y)) (/ 1 z)) (- (/ (neg (* (neg (log y)) x)) (* z y)) (/ 1 y)) (/ (neg (* (neg (log y)) x)) (* z y)) (neg (* (neg (log y)) x)) (* (neg (log y)) x) (neg (log y)) (* z y) (/ 1 y) 1 (/ 1 z)) |
| 198.0ms | x | @ | -inf | ((+ (* y y) (* (+ (* y 2) x) x)) y (* (+ (* y 2) x) x) (+ (* y 2) x) 2 x (+ (+ (* x x) (* (* x 2) y)) (* y y)) (* y y) (+ (+ (* x x) (* (* x 2) y)) (* y y)) (* (+ (* 2 x) y) y) (+ (* 2 x) y) (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+ (+ (* x x) (* (* x 2) y)) (* y y)) (+ (* x x) (* (* x 2) y)) (* (+ x x) y) (+ x x)) |
| 177.0ms | x | @ | 0 | ((* x (- (log x) (log y))) x (- (log x) (log y)) (log x) (log y) y (* x (neg (log (* (/ 1 x) y)))) (neg (log (* (/ 1 x) y))) (log (* (/ 1 x) y)) (* (/ 1 x) y) (/ 1 x) 1 (* (* (/ x (log (* x y))) (log (/ x y))) (log (* x y))) (* (/ x (log (* x y))) (log (/ x y))) (/ x (log (* x y))) (log (* x y)) (* x y) (log (/ x y)) (/ x y) (* x (/ (- 0 (* (log (/ y x)) (log (/ y x)))) (+ 0 (log (/ y x))))) (/ (- 0 (* (log (/ y x)) (log (/ y x)))) (+ 0 (log (/ y x)))) (- 0 (* (log (/ y x)) (log (/ y x)))) 0 (* (log (/ y x)) (log (/ y x))) (log (/ y x)) (/ y x) (+ 0 (log (/ y x))) (* x (/ (- (* (* (log (neg x)) (log (neg x))) (log (* y x))) (* (log (* y x)) (* (log (neg y)) (log (neg y))))) (* (log (* y x)) (log (* y x))))) (/ (- (* (* (log (neg x)) (log (neg x))) (log (* y x))) (* (log (* y x)) (* (log (neg y)) (log (neg y))))) (* (log (* y x)) (log (* y x)))) (- (* (* (log (neg x)) (log (neg x))) (log (* y x))) (* (log (* y x)) (* (log (neg y)) (log (neg y))))) (* (* (log (neg x)) (log (neg x))) (log (* y x))) (* (log (neg x)) (log (neg x))) (log (neg x)) (neg x) (log (* y x)) (* y x) (* (log (* y x)) (* (log (neg y)) (log (neg y)))) (* (log (neg y)) (log (neg y))) (log (neg y)) (neg y) (* (log (* y x)) (log (* y x)))) |
| 176.0ms | x | @ | 0 | ((* (* x 1) (log (+ 1 (* (neg y) (/ 1 x))))) (* x 1) x (log (+ 1 (* (neg y) (/ 1 x)))) (* (neg y) (/ 1 x)) (neg y) y (/ 1 x) 1 (* (log (- 1 (/ y x))) x) (log (- 1 (/ y x))) (- 1 (/ y x)) (* (* x 1) (log (- 1 (/ y x)))) (log (- 1 (/ y x))) (log (/ (neg y) x)) (/ (neg y) x) (* (* x 1) (log (- 1 (/ y x)))) (* (+ (neg (neg (log y))) (neg (log (neg x)))) x) (+ (neg (neg (log y))) (neg (log (neg x)))) (neg (neg (log y))) (neg (log y)) (log y) (neg (log (neg x))) (log (neg x)) (neg x) (* (* x 1) (- (log (- 1 (/ (* (* y y) y) (* (* x x) x)))) (log (+ 1 (+ (* (/ y x) (/ y x)) (/ y x)))))) (* (+ (* 3 (log (neg y))) (- (* -3 (log x)) (log (/ (* y y) (* x x))))) x) (+ (* 3 (log (neg y))) (- (* -3 (log x)) (log (/ (* y y) (* x x))))) 3 (log (neg y)) (- (* -3 (log x)) (log (/ (* y y) (* x x)))) (* -3 (log x)) -3 (log x) (log (/ (* y y) (* x x))) (/ (* y y) (* x x)) (* y y) (* x x)) |
Compiled 3 125 617 to 1 034 579 computations (66.9% saved)
| 1 725× | binary-search |
| 1 070× | left-value |
| 1 700× | narrow-enough |
| 25× | predicate-same |
| 14.2s | 138 541× | 0 | valid |
| 905.0ms | 3 634× | 1 | valid |
| 194.0ms | 2 434× | 0 | invalid |
| 33.0ms | 107× | 2 | valid |
| 1.0ms | 6× | 3 | valid |
Compiled 650 484 to 663 552 computations (-2% saved)
ival-mult!: 4.1s (47.3% of total)ival-sub!: 1.5s (17.3% of total)ival-div!: 709.0ms (8.2% of total)ival-log: 708.0ms (8.2% of total)ival-add!: 702.0ms (8.1% of total)ival-cos: 280.0ms (3.2% of total)ival-sin: 204.0ms (2.4% of total)adjust: 194.0ms (2.2% of total)ival-exp: 149.0ms (1.7% of total)ival-sqrt: 91.0ms (1% of total)ival-tanh: 9.0ms (0.1% of total)ival-cosh: 8.0ms (0.1% of total)ival-fabs: 7.0ms (0.1% of total)| 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)
Compiled 484 198 to 425 513 computations (12.1% saved)
Loading profile data...