Herbie run
| Date: | Thursday, April 24th, 2025 |
|---|---|
| Commit: | d5acc5eb on main |
| Seed: | 2025114 |
| 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: | 950 752.9 MB |
Time bar (total: 13.3min)
| 2.4min | 2 144 707× | 0 | valid |
| 18.8s | 69 573× | 1 | valid |
| 7.1s | 64 378× | 0 | invalid |
| 1.6s | 5 967× | 2 | valid |
| 700.0ms | 1 227× | 5 | exit |
| 324.0ms | 1 888× | 1 | invalid |
| 213.0ms | 614× | 3 | valid |
| 169.0ms | 426× | 4 | exit |
| 2.0ms | 21× | 1 | exit |
| 1.0ms | 3× | 4 | valid |
ival-mult!: 30.5s (33.5% of total)ival-div!: 14.1s (15.5% of total)ival-sub!: 9.9s (10.8% of total)ival-log: 9.1s (10% of total)ival-add!: 8.9s (9.7% of total)ival-sqrt: 4.7s (5.2% of total)ival-sin: 4.0s (4.4% of total)adjust: 3.9s (4.2% of total)ival-cos: 2.7s (2.9% of total)ival-exp: 1.7s (1.9% of total)ival-fabs: 327.0ms (0.4% of total)ival-hypot: 287.0ms (0.3% of total)ival-cosh: 269.0ms (0.3% of total)ival-tan: 265.0ms (0.3% of total)ival-sinh: 226.0ms (0.2% of total)ival-acos: 193.0ms (0.2% of total)ival-tanh: 100.0ms (0.1% of total)const: 0.0ms (0% of total)| 2 234× | iter-limit |
| 850× | node-limit |
| 71× | unsound |
| 14× | saturated |
512 calls:
| 12.0s | x |
| 8.8s | y |
| 6.4s | z |
| 3.9s | t |
| 3.1s | (-.f64 (*.f64 y z) (*.f64 t z)) |
Compiled 33 339 to 56 081 computations (-68.2% saved)
| 147× | fuel |
| 122× | done |
Compiled 30 947 to 18 935 computations (38.8% saved)
8928 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 4.2s | x | @ | 0 | ((- (* x x) (* (* y 4) (- (* z z) t))) (* x x) x (* (* y 4) (- (* z z) t)) (* y 4) y 4 (- (* z z) t) (* (+ (* z (/ z t)) -1) t) (+ (* z (/ z t)) -1) (* (/ z t) z) (/ z t) z t (/ (- (* (* (* x x) x) x) (* (* (- (* z z) t) (- (* z z) t)) (* 16 (* y y)))) (+ (* (* 4 y) (- (* z z) t)) (* x x))) (- (* (* (* x x) x) x) (* (* (- (* z z) t) (- (* z z) t)) (* 16 (* y y)))) (* (* (* x x) x) x) (* (* x x) x) (* (* (- (* z z) t) (- (* z z) t)) (* 16 (* y y))) (* (- (* z z) t) (- (* z z) t)) (- (* z z) t) (* z z) (* 16 (* y y)) 16 (* y y) (+ (* (* 4 y) (- (* z z) t)) (* x x)) (* 4 y)) |
| 2.0s | y | @ | 0 | ((+ (* (/ (- z t) (- a t)) y) x) (/ (- z t) (- a t)) (- z t) z t (- a t) a y x (+ x (/ (* y (- z t)) (- a t))) (+ x (/ (* y (- z t)) (- a t))) (+ (* y (/ z a)) x) (/ z a) (+ x (/ (* y (- z t)) (- a t))) (/ (* y (- z t)) (- a t)) (/ (* z y) a) (* z y) (+ x (/ (* y (- z t)) (- a t))) (- x (/ (* (- z t) y) t)) (/ (* (- z t) y) t) (* (- z t) y)) |
| 643.0ms | t | @ | 0 | ((- x (/ (log (+ (- 1 y) (* y (exp z)))) t)) x (/ (log (+ (- 1 y) (* y (exp z)))) t) (* (+ (* -1/2 (/ (* (- (exp z) 1) (* (- (exp z) 1) y)) t)) (/ (- (exp z) 1) t)) y) (+ (* -1/2 (/ (* (- (exp z) 1) (* (- (exp z) 1) y)) t)) (/ (- (exp z) 1) t)) -1/2 (/ (* (- (exp z) 1) (* (- (exp z) 1) y)) t) (* (- (exp z) 1) (* (- (exp z) 1) y)) (- (exp z) 1) z (* (- (exp z) 1) y) y t (/ (- (exp z) 1) t) (- x (/ (log (- (+ (* (exp z) y) 1) y)) t)) (/ (log (- (+ (* (exp z) y) 1) y)) t) (log (- (+ (* (exp z) y) 1) y)) (* z y) (- x (/ (log (+ (- 1 y) (* y (exp z)))) t)) (/ (log (+ (- 1 y) (* y (exp z)))) t) (log (+ (- 1 y) (* y (exp z)))) (+ (- 1 y) (* y (exp z))) (* (- (exp z) 1) y) (- (exp z) 1) (- x (/ (log (- (+ (* (exp z) y) 1) y)) t)) (/ (log (- (+ (* (exp z) y) 1) y)) t) (log (- (+ (* (exp z) y) 1) y)) (- (+ (* (exp z) y) 1) y) (+ (* z y) 1) 1 (- x (/ (log (+ (- 1 y) (* y (exp z)))) t)) (+ (* (/ (- (* -1/2 (* (+ (neg (* y y)) y) z)) y) t) z) x) (/ (- (* -1/2 (* (+ (neg (* y y)) y) z)) y) t) (- (* -1/2 (* (+ (neg (* y y)) y) z)) y) (* -1/2 (* (+ (neg (* y y)) y) z)) (* (+ (neg (* y y)) y) z) (* (+ (* (neg y) z) z) y) (+ (* (neg y) z) z) (neg y)) |
| 370.0ms | z | @ | inf | ((* x (- 1 (* y z))) (- x (* (* y x) z)) x (* (* y x) z) (* y x) y z (* x (- 1 (* y z))) (- (/ (* x x) (* (+ (* z y) 1) x)) (/ (* (* (* (* z y) x) z) (* y x)) (* (+ (* z y) 1) x))) (/ (* x x) (* (+ (* z y) 1) x)) (* x x) (* (+ (* z y) 1) x) (+ (* z y) 1) 1 (/ (* (* (* (* z y) x) z) (* y x)) (* (+ (* z y) 1) x)) (* (* (* (* z y) x) z) (* y x)) (* (* (* z y) x) z) (* (* z y) x) (* z y) (* x (- 1 (* y z))) (/ (* (neg x) (+ (* (* (* (* z y) z) y) (* z y)) -1)) (+ (* (* (* z y) z) y) (+ (* z y) 1))) (* (neg x) (+ (* (* (* (* z y) z) y) (* z y)) -1)) (neg x) (+ (* (* (* (* z y) z) y) (* z y)) -1) (* (* (* z y) z) y) (* (* z y) z) -1 (+ (* (* (* z y) z) y) (+ (* z y) 1)) (- x (* (* z y) x)) (* (* (neg x) z) y) (* (neg x) z)) |
| 295.0ms | x | @ | 0 | ((* (neg x) (log (/ y x))) (neg x) x (log (/ y x)) (/ y x) y (* x (- (log x) (log y))) (- (log x) (log y)) (log x) (log y) (- (* (log (neg x)) x) (* (log (neg y)) x)) (* (log (neg x)) x) (log (neg x)) (* (log (neg y)) x) (log (neg y)) (neg y) (* x (/ (- (* (log (* (/ -1 y) -1)) (log (* (/ -1 y) -1))) (* (log x) (log x))) (- (log (* (/ -1 y) -1)) (log x)))) (/ (- (* (log (* (/ -1 y) -1)) (log (* (/ -1 y) -1))) (* (log x) (log x))) (- (log (* (/ -1 y) -1)) (log x))) (- (* (log (* (/ -1 y) -1)) (log (* (/ -1 y) -1))) (* (log x) (log x))) (* (log (* (/ -1 y) -1)) (log (* (/ -1 y) -1))) (log (* (/ -1 y) -1)) (* (/ -1 y) -1) (/ -1 y) -1 (* (log x) (log x)) (- (log (* (/ -1 y) -1)) (log x)) (- (/ (* (* x x) (* (log x) (log x))) (+ (* (log x) x) (* (log y) x))) (/ (* (* x x) (* (log y) (log y))) (+ (* (log x) x) (* (log y) x)))) (/ (* (* x x) (* (log x) (log x))) (+ (* (log x) x) (* (log y) x))) (* (* x x) (* (log x) (log x))) (* x x) (+ (* (log x) x) (* (log y) x)) (* (log y) x) (/ (* (* x x) (* (log y) (log y))) (+ (* (log x) x) (* (log y) x))) (* (* x x) (* (log y) (log y))) (* (log y) (log y))) |
| 174× | node-limit |
| 95× | saturated |
Compiled 138 742 to 111 311 computations (19.8% saved)
Compiled 3 285 372 to 1 021 342 computations (68.9% saved)
| 1 863× | binary-search |
| 1 087× | left-value |
| 1 829× | narrow-enough |
| 34× | predicate-same |
| 12.1s | 147 609× | 0 | valid |
| 660.0ms | 3 791× | 1 | valid |
| 227.0ms | 2 866× | 0 | invalid |
| 29.0ms | 181× | 2 | valid |
| 0.0ms | 3× | 3 | valid |
Compiled 703 686 to 715 833 computations (-1.7% saved)
ival-mult!: 3.7s (49.2% of total)ival-sub!: 1.1s (14.7% of total)ival-add!: 831.0ms (11.2% of total)ival-div!: 569.0ms (7.7% of total)ival-sin: 348.0ms (4.7% of total)ival-log: 335.0ms (4.5% of total)ival-cos: 256.0ms (3.4% of total)adjust: 209.0ms (2.8% of total)ival-exp: 52.0ms (0.7% of total)ival-sqrt: 50.0ms (0.7% of total)ival-sinh: 10.0ms (0.1% of total)ival-cosh: 9.0ms (0.1% of total)ival-tanh: 8.0ms (0.1% of total)ival-fabs: 5.0ms (0.1% of total)Compiled 506 868 to 442 174 computations (12.8% 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...