Herbie run
| Date: | Monday, May 19th, 2025 |
|---|---|
| Commit: | 0e5c6bc4 on main |
| Seed: | 2025139 |
| 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 007 440.8 MB |
Time bar (total: 13.9min)
| 2.7min | 2 144 687× | 0 | valid |
| 19.6s | 69 521× | 1 | valid |
| 8.6s | 64 030× | 0 | invalid |
| 1.4s | 5 970× | 2 | valid |
| 936.0ms | 1 222× | 5 | exit |
| 394.0ms | 1 751× | 1 | invalid |
| 311.0ms | 407× | 4 | exit |
| 251.0ms | 684× | 3 | valid |
| 3.0ms | 26× | 1 | exit |
| 0.0ms | 2× | 4 | valid |
ival-mult!: 33.6s (30.6% of total)ival-add!: 18.2s (16.6% of total)ival-sub!: 13.1s (11.9% of total)ival-div!: 11.8s (10.8% of total)ival-log: 9.7s (8.9% of total)ival-sqrt: 6.5s (5.9% of total)ival-sin: 5.5s (5% of total)adjust: 4.3s (3.9% of total)ival-cos: 3.0s (2.7% of total)ival-exp: 2.2s (2% of total)ival-cosh: 404.0ms (0.4% of total)ival-tan: 250.0ms (0.2% of total)ival-hypot: 249.0ms (0.2% of total)ival-sinh: 242.0ms (0.2% of total)ival-fabs: 212.0ms (0.2% of total)ival-acos: 197.0ms (0.2% of total)ival-tanh: 195.0ms (0.2% of total)| 2 227× | iter-limit |
| 868× | node-limit |
| 67× | unsound |
| 16× | saturated |
| 152× | fuel |
| 117× | done |
Compiled 30 038 to 18 735 computations (37.6% saved)
512 calls:
| 9.3s | x |
| 8.7s | y |
| 7.7s | z |
| 4.2s | t |
| 2.7s | a |
Compiled 32 060 to 54 272 computations (-69.3% saved)
9021 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 3.7s | y | @ | inf | ((/ (* (/ y (+ y x)) (/ x (+ y x))) (+ (+ y x) 1)) (* (/ y (+ y x)) (/ x (+ y x))) (/ y (+ y x)) y (+ y x) x (/ x (+ y x)) (+ (+ y x) 1) 1 (/ (* x y) (* (* (+ x y) (+ x y)) (+ (+ x y) 1))) (/ y (* x x)) (* x x) (/ (/ (* y x) (* (+ y x) (+ y x))) (+ (+ y x) 1)) (/ (* y x) (* (+ y x) (+ y x))) (/ x y) (/ (/ (* y x) (* (+ y x) (+ y x))) (+ (+ x y) 1)) (/ (* y x) (* (+ y x) (+ y x))) (* y x) (* (+ y x) (+ y x)) (+ (+ x y) 1) (+ 1 x) (/ (/ (* y x) (* (+ y x) (+ y x))) (+ (+ y x) 1)) (/ (* y x) (* (+ y x) (+ y x))) (* (+ y x) (+ y x)) (* (+ (* 2 x) y) y) (+ (* 2 x) y) 2) |
| 1.6s | t | @ | 0 | ((* (/ (- x y) (- z y)) t) (neg (/ (* (- x y) t) y)) (* (- 1 (/ x y)) t) (- 1 (/ x y)) 1 (/ x y) x y t (* (/ (- x y) (- z y)) t) (/ (- x y) (- z y)) (/ x z) z (* (/ (- x y) (- z y)) t) (* (- x y) (/ t z)) (- x y) (neg y) (/ t z) (* (/ (- x y) (- z y)) t) (neg (/ (* (- x y) t) y)) (/ (* t (- y x)) y) (* t (- y x)) (- y x) (/ (* (- x y) t) (- z y)) (* (- x y) t) (* t x) (- z y)) |
| 1.1s | 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) (* (- 1 (/ 1/2 a)) a) (- 1 (/ 1/2 a)) 1 (/ 1/2 a) 1/2 a (log t) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (neg t) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (+ (log (* z (+ y x))) (* -1/2 (log t))) t) (+ (log (* z (+ y x))) (* -1/2 (log t))) (log (* z (+ y x))) (* z (+ y x)) (+ y x) (* -1/2 (log t)) -1/2 (+ (- (+ (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)) (log x) (* (- a 1/2) (log t)) (- a 1/2) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (+ (log (* z x)) (+ (* (+ (* (/ y (* x x)) -1/2) (/ 1 x)) y) (* (log t) (- a 1/2)))) t) (+ (log (* z x)) (+ (* (+ (* (/ y (* x x)) -1/2) (/ 1 x)) y) (* (log t) (- a 1/2)))) (log (* z x)) (* z x) (+ (* (+ (* (/ y (* x x)) -1/2) (/ 1 x)) y) (* (log t) (- a 1/2))) (+ (* (/ y (* x x)) -1/2) (/ 1 x)) (/ y (* x x)) (* x x) (/ 1 x) (* (log t) (- a 1/2))) |
| 819.0ms | z | @ | -inf | ((/ x (+ x (* y (exp (* 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3)))))))))) x (+ x (* y (exp (* 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3))))))))) (* y (exp (* 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3)))))))) y (exp (* 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3))))))) (* 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3)))))) 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3))))) (* b (- (* 2/3 (/ 1 t)) (+ 5/6 a))) b (- (* 2/3 (/ 1 t)) (+ 5/6 a)) (* -1 (+ 5/6 a)) -1 (+ 5/6 a) 5/6 a (/ x (+ x (* y (exp (* 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3)))))))))) (+ x (* y (exp (* 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3))))))))) (* y (exp (* 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3)))))))) (exp (* 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3))))))) (* 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3)))))) (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3))))) (* c (- (+ 5/6 a) (* 2/3 (/ 1 t)))) c (- (+ 5/6 a) (* 2/3 (/ 1 t))) (+ 5/6 a) (/ x (+ x (* y (exp (* 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3)))))))))) (+ x (* y (exp (* 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3))))))))) (* y (exp (* 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3)))))))) (exp (* 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3))))))) (* 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3)))))) (* 2 (/ (* z (sqrt (+ a t))) t)) (* -2 (* z (/ 1 (sqrt t)))) -2 (* z (/ 1 (sqrt t))) (/ z (sqrt t)) z (sqrt t) t (/ x (+ x (* y (exp (* 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3)))))))))) (+ x (* y (exp (* 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3))))))))) (* y (exp (* 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3)))))))) (exp (* 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3))))))) (* 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3)))))) (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3))))) (* b (- (* 2/3 (/ 1 t)) (+ 5/6 a))) (- (* 2/3 (/ 1 t)) (+ 5/6 a)) (* -1 a) (/ x (+ x (* y (exp (* 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3)))))))))) (+ x (* y (exp (* 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3))))))))) (* y (exp (* 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3)))))))) (exp (* 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3))))))) (* 2 (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3)))))) (- (/ (* z (sqrt (+ t a))) t) (* (- b c) (- (+ a (/ 5 6)) (/ 2 (* t 3))))) (* c (- (+ 5/6 a) (* 2/3 (/ 1 t)))) (- (+ 5/6 a) (* 2/3 (/ 1 t))) (/ -2/3 t) -2/3) |
| 592.0ms | z | @ | inf | ((- x (/ (log (+ (- 1 y) (* y (exp z)))) t)) x (/ (log (+ (- 1 y) (* y (exp z)))) t) (log (+ (- 1 y) (* y (exp z)))) (* (- (exp z) 1) y) (- (exp z) 1) z y t (- x (/ (log (+ (- 1 y) (* y (exp z)))) t)) (/ (log (+ (- 1 y) (* y (exp z)))) t) (log (+ (- 1 y) (* y (exp z)))) (* z y) (- x (/ (log (+ (- 1 y) (* y (exp z)))) t)) (/ (log (+ (- 1 y) (* y (exp z)))) t) (log (+ (- 1 y) (* y (exp z)))) (log (* (- (exp z) 1) y)) (- x (/ (log (+ (- 1 y) (* y (exp z)))) t)) (neg (* (- (/ (log (- (+ (* (exp z) y) 1) y)) (* t x)) 1) x)) (* (- (/ (log (- (+ (* (exp z) y) 1) y)) (* t x)) 1) x) (- (/ (log (- (+ (* (exp z) y) 1) y)) (* t x)) 1) (/ (log (- (+ (* (exp z) y) 1) y)) (* t x)) (log (- (+ (* (exp z) y) 1) y)) (- (+ (* (exp z) y) 1) y) (+ (* (exp z) y) 1) (exp z) 1 (* t x) (- x (/ (log (+ (- 1 y) (* y (exp z)))) t)) (- (- x (/ (log y) t)) (+ (/ 1 (* (* (- (exp z) 1) y) t)) (/ (log (- (exp z) 1)) t))) (- x (/ (log y) t)) (/ (log y) t) (log y) (+ (/ 1 (* (* (- (exp z) 1) y) t)) (/ (log (- (exp z) 1)) t)) (/ 1 (* (* (- (exp z) 1) y) t)) (* (* (- (exp z) 1) y) t) (/ (log (- (exp z) 1)) t) (log (- (exp z) 1))) |
| 237× | node-limit |
| 32× | saturated |
Compiled 127 179 to 103 683 computations (18.5% saved)
Compiled 3 005 382 to 986 027 computations (67.2% saved)
| 1 700× | binary-search |
| 1 043× | left-value |
| 1 669× | narrow-enough |
| 31× | predicate-same |
| 13.2s | 135 548× | 0 | valid |
| 823.0ms | 4 173× | 1 | valid |
| 228.0ms | 2 583× | 0 | invalid |
| 23.0ms | 162× | 2 | valid |
| 9.0ms | 51× | 1 | invalid |
| 4.0ms | 5× | 3 | valid |
Compiled 694 877 to 697 425 computations (-0.4% saved)
ival-mult!: 3.5s (45.2% of total)ival-sub!: 1.3s (16.4% of total)ival-div!: 835.0ms (10.7% of total)ival-add!: 714.0ms (9.2% of total)ival-log: 529.0ms (6.8% of total)ival-sin: 224.0ms (2.9% of total)ival-cos: 208.0ms (2.7% of total)adjust: 179.0ms (2.3% of total)ival-sqrt: 176.0ms (2.3% of total)ival-exp: 110.0ms (1.4% of total)ival-tanh: 7.0ms (0.1% of total)ival-fabs: 7.0ms (0.1% of total)ival-cosh: 5.0ms (0.1% of total)ival-sinh: 1.0ms (0% of total)Compiled 520 332 to 449 612 computations (13.6% 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...