Herbie run
| Date: | Saturday, May 3rd, 2025 |
|---|---|
| Commit: | 1cbc6d8b on time-nightly |
| Seed: | 2025123 |
| 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 006 200.0 MB |
Time bar (total: 13.9min)
| 2.8min | 2 145 201× | 0 | valid |
| 18.8s | 69 097× | 1 | valid |
| 8.3s | 64 452× | 0 | invalid |
| 1.4s | 5 834× | 2 | valid |
| 1.3s | 1 851× | 1 | invalid |
| 712.0ms | 1 204× | 5 | exit |
| 264.0ms | 731× | 3 | valid |
| 259.0ms | 380× | 4 | exit |
| 3.0ms | 29× | 1 | exit |
| 0.0ms | 1× | 4 | valid |
ival-mult!: 37.4s (36.9% of total)ival-div!: 12.3s (12.1% of total)ival-add!: 11.3s (11.2% of total)ival-sub!: 10.1s (10% of total)ival-log: 8.8s (8.7% of total)ival-sqrt: 5.2s (5.1% of total)ival-cos: 4.3s (4.3% of total)ival-sin: 4.3s (4.3% of total)adjust: 3.9s (3.9% of total)ival-exp: 1.9s (1.9% of total)ival-hypot: 374.0ms (0.4% of total)ival-tan: 334.0ms (0.3% of total)ival-cosh: 330.0ms (0.3% of total)ival-sinh: 277.0ms (0.3% of total)ival-fabs: 218.0ms (0.2% of total)ival-acos: 183.0ms (0.2% of total)ival-tanh: 105.0ms (0.1% of total)| 2 201× | iter-limit |
| 844× | node-limit |
| 71× | unsound |
| 14× | saturated |
| 237× | node-limit |
| 32× | saturated |
Compiled 144 015 to 115 708 computations (19.7% saved)
| 151× | fuel |
| 118× | done |
Compiled 30 774 to 18 676 computations (39.3% saved)
512 calls:
| 8.9s | x |
| 8.6s | y |
| 6.6s | z |
| 5.3s | t |
| 3.1s | a |
Compiled 33 411 to 56 147 computations (-68% saved)
8898 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 4.0s | y4 | @ | 0 | ((+ (- (+ (+ (- (* (- (* x y) (* z t)) (- (* a b) (* c i))) (* (- (* x j) (* z k)) (- (* y0 b) (* y1 i)))) (* (- (* x y2) (* z y3)) (- (* y0 c) (* y1 a)))) (* (- (* t j) (* y k)) (- (* y4 b) (* y5 i)))) (* (- (* t y2) (* y y3)) (- (* y4 c) (* y5 a)))) (* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0)))) (* x (- (+ (* y (- (* a b) (* c i))) (* y2 (- (* c y0) (* a y1)))) (* j (- (* b y0) (* i y1))))) x (- (+ (* y (- (* a b) (* c i))) (* y2 (- (* c y0) (* a y1)))) (* j (- (* b y0) (* i y1)))) (+ (* y (- (* a b) (* c i))) (* y2 (- (* c y0) (* a y1)))) y (- (* a b) (* c i)) (* a b) a b (* c i) c i (* y2 (- (* c y0) (* a y1))) y2 (- (* c y0) (* a y1)) (* c y0) y0 (* a y1) y1 (* j (- (* b y0) (* i y1))) j (- (* b y0) (* i y1)) (* b y0) (* i y1) (+ (- (+ (+ (- (* (- (* x y) (* z t)) (- (* a b) (* c i))) (* (- (* x j) (* z k)) (- (* y0 b) (* y1 i)))) (* (- (* x y2) (* z y3)) (- (* y0 c) (* y1 a)))) (* (- (* t j) (* y k)) (- (* y4 b) (* y5 i)))) (* (- (* t y2) (* y y3)) (- (* y4 c) (* y5 a)))) (* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0)))) (* -1 (* y3 (- (+ (* j (- (* y1 y4) (* y0 y5))) (* z (- (* c y0) (* a y1)))) (* y (- (* c y4) (* a y5)))))) (* a (* y3 (- (* y1 z) (* y y5)))) (* y3 (- (* y1 z) (* y y5))) y3 (- (* y1 z) (* y y5)) (* y1 z) z (* y y5) y5 (+ (- (+ (+ (- (* (- (* x y) (* z t)) (- (* a b) (* c i))) (* (- (* x j) (* z k)) (- (* y0 b) (* y1 i)))) (* (- (* x y2) (* z y3)) (- (* y0 c) (* y1 a)))) (* (- (* t j) (* y k)) (- (* y4 b) (* y5 i)))) (* (- (* t y2) (* y y3)) (- (* y4 c) (* y5 a)))) (* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0)))) (* b (- (+ (* a (- (* x y) (* t z))) (* y4 (- (* j t) (* k y)))) (* y0 (- (* j x) (* k z))))) (- (+ (* a (- (* x y) (* t z))) (* y4 (- (* j t) (* k y)))) (* y0 (- (* j x) (* k z)))) (* x (- (* a y) (* j y0))) (- (* a y) (* j y0)) (* a y) (* j y0) (+ (- (+ (+ (- (* (- (* x y) (* z t)) (- (* a b) (* c i))) (* (- (* x j) (* z k)) (- (* y0 b) (* y1 i)))) (* (- (* x y2) (* z y3)) (- (* y0 c) (* y1 a)))) (* (- (* t j) (* y k)) (- (* y4 b) (* y5 i)))) (* (- (* t y2) (* y y3)) (- (* y4 c) (* y5 a)))) (* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0)))) (* k (- (+ (* -1 (* y (- (* b y4) (* i y5)))) (* y2 (- (* y1 y4) (* y0 y5)))) (* -1 (* z (- (* b y0) (* i y1)))))) k (- (+ (* -1 (* y (- (* b y4) (* i y5)))) (* y2 (- (* y1 y4) (* y0 y5)))) (* -1 (* z (- (* b y0) (* i y1))))) (* y2 (- (* y1 y4) (* y0 y5))) (- (* y1 y4) (* y0 y5)) (* y1 y4) y4 (* y0 y5) (+ (- (+ (+ (- (* (- (* x y) (* z t)) (- (* a b) (* c i))) (* (- (* x j) (* z k)) (- (* y0 b) (* y1 i)))) (* (- (* x y2) (* z y3)) (- (* y0 c) (* y1 a)))) (* (- (* t j) (* y k)) (- (* y4 b) (* y5 i)))) (* (- (* t y2) (* y y3)) (- (* y4 c) (* y5 a)))) (* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0)))) (* b (- (+ (* a (- (* x y) (* t z))) (* y4 (- (* j t) (* k y)))) (* y0 (- (* j x) (* k z))))) (- (+ (* a (- (* x y) (* t z))) (* y4 (- (* j t) (* k y)))) (* y0 (- (* j x) (* k z)))) (* -1 (* z (- (* a t) (* k y0)))) -1 (* z (- (* a t) (* k y0))) (- (* a t) (* k y0)) (* a t) t (* k y0)) |
| 640.0ms | t | @ | inf | ((+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (+ (+ (* (log t) (- a 1/2)) (log y)) (log z)) t) (+ (+ (* (log t) (- a 1/2)) (log y)) (log z)) (+ (* (log t) (- a 1/2)) (log y)) (log t) t (- a 1/2) a 1/2 (log y) y (log z) z (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (+ (+ (* (log t) (- a 1/2)) (neg (neg (log z)))) (log (+ y x))) t) (+ (+ (* (log t) (- a 1/2)) (neg (neg (log z)))) (log (+ y x))) (* a (log t)) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (+ (+ (* (log t) (- a 1/2)) (neg (neg (log y)))) (log z)) t) (+ (log (* y z)) (* (log t) (- a 1/2))) (log (* y z)) (* y z) (* (log t) (- a 1/2)) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (+ (+ (* (log t) (- a 1/2)) (neg (neg (log y)))) (log z)) t) (+ (+ (* (log t) (- a 1/2)) (neg (neg (log y)))) (log z)) (+ (* (log t) (- a 1/2)) (neg (neg (log y)))) (- a 1/2) (neg (neg (log y))) (neg (log y)) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (* (- (+ (/ (log (* z (+ y x))) t) (neg (* (neg (log t)) (/ (- a 1/2) t)))) 1) t) (- (+ (/ (log (* z (+ y x))) t) (neg (* (neg (log t)) (/ (- a 1/2) t)))) 1) (- (/ (+ (neg (neg (log x))) (log z)) t) (+ (* (neg (log t)) (/ (- a 1/2) t)) 1)) (/ (+ (neg (neg (log x))) (log z)) t) (+ (neg (neg (log x))) (log z)) (neg (neg (log x))) (neg (log x)) (log x) x (+ (* (neg (log t)) (/ (- a 1/2) t)) 1) (- 1 (* -1/2 (/ (log t) t))) 1 (* -1/2 (/ (log t) t)) -1/2 (/ (log t) t)) |
| 210.0ms | x | @ | -inf | ((+ (* (neg (log y)) x) (* (log x) x)) (neg (log y)) (log y) y x (* (log x) x) (log x) (* (neg x) (log (/ y x))) (neg x) (log (/ y x)) (/ y x) (+ (* (log x) x) (* (neg x) (log y))) (* (neg x) (log y)) (/ (* (* (log (* x y)) (log (/ x y))) x) (log (* x y))) (* (* (log (* x y)) (log (/ x y))) x) (* (log (* x y)) (log (/ x y))) (log (* x y)) (* x y) (log (/ x y)) (/ x y) (* x (/ (- (* (* (log (* -1 y)) (neg (log (neg y)))) (log (neg x))) (* (log (* -1 y)) (* (log (neg x)) (neg (log (neg x)))))) (* (log (* -1 y)) (log (neg x))))) (/ (- (* (* (log (* -1 y)) (neg (log (neg y)))) (log (neg x))) (* (log (* -1 y)) (* (log (neg x)) (neg (log (neg x)))))) (* (log (* -1 y)) (log (neg x)))) (- (* (* (log (* -1 y)) (neg (log (neg y)))) (log (neg x))) (* (log (* -1 y)) (* (log (neg x)) (neg (log (neg x)))))) (* (* (log (* -1 y)) (neg (log (neg y)))) (log (neg x))) (* (log (* -1 y)) (neg (log (neg y)))) (log (* -1 y)) (* -1 y) -1 (neg (log (neg y))) (log (neg y)) (neg y) (log (neg x)) (* (log (* -1 y)) (* (log (neg x)) (neg (log (neg x))))) (* (log (neg x)) (neg (log (neg x)))) (neg (log (neg x))) (* (log (* -1 y)) (log (neg x)))) |
| 205.0ms | x | @ | 0 | ((+ (* (neg (log y)) x) (* (log x) x)) (neg (log y)) (log y) y x (* (log x) x) (log x) (* (neg x) (log (/ y x))) (neg x) (log (/ y x)) (/ y x) (+ (* (log x) x) (* (neg x) (log y))) (* (neg x) (log y)) (/ (* (* (log (* x y)) (log (/ x y))) x) (log (* x y))) (* (* (log (* x y)) (log (/ x y))) x) (* (log (* x y)) (log (/ x y))) (log (* x y)) (* x y) (log (/ x y)) (/ x y) (* x (/ (- (* (* (log (* -1 y)) (neg (log (neg y)))) (log (neg x))) (* (log (* -1 y)) (* (log (neg x)) (neg (log (neg x)))))) (* (log (* -1 y)) (log (neg x))))) (/ (- (* (* (log (* -1 y)) (neg (log (neg y)))) (log (neg x))) (* (log (* -1 y)) (* (log (neg x)) (neg (log (neg x)))))) (* (log (* -1 y)) (log (neg x)))) (- (* (* (log (* -1 y)) (neg (log (neg y)))) (log (neg x))) (* (log (* -1 y)) (* (log (neg x)) (neg (log (neg x)))))) (* (* (log (* -1 y)) (neg (log (neg y)))) (log (neg x))) (* (log (* -1 y)) (neg (log (neg y)))) (log (* -1 y)) (* -1 y) -1 (neg (log (neg y))) (log (neg y)) (neg y) (log (neg x)) (* (log (* -1 y)) (* (log (neg x)) (neg (log (neg x))))) (* (log (neg x)) (neg (log (neg x)))) (neg (log (neg x))) (* (log (* -1 y)) (log (neg x)))) |
| 190.0ms | z | @ | 0 | ((+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (+ (+ (* (log t) (- a 1/2)) (neg (neg (log z)))) (log (+ y x))) t) (+ (+ (* (log t) (- a 1/2)) (neg (neg (log z)))) (log (+ y x))) (+ (* (log t) (- a 1/2)) (neg (neg (log z)))) (log t) t (- a 1/2) a 1/2 (neg (neg (log z))) (neg (log z)) (log z) z (log (+ y x)) (+ y x) y x (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (* (log t) a) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (+ (* -1/2 (log t)) (log (* (+ y x) z))) t) (+ (* -1/2 (log t)) (log (* (+ y x) z))) -1/2 (log (* (+ y x) z)) (* (+ y x) z) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (+ (+ (* (log t) (- a 1/2)) (neg (neg (log y)))) (log z)) t) (+ (+ (* (log t) (- a 1/2)) (neg (neg (log y)))) (log z)) (+ (* (log t) (- a 1/2)) (neg (neg (log y)))) (neg (neg (log y))) (neg (log y)) (log y) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (* (- (+ (/ (log (* z (+ y x))) t) (neg (* (neg (log t)) (/ (- a 1/2) t)))) 1) t) (- (+ (/ (log (* z (+ y x))) t) (neg (* (neg (log t)) (/ (- a 1/2) t)))) 1) (- (/ (+ (neg (neg (log x))) (log z)) t) (+ (* (neg (log t)) (/ (- a 1/2) t)) 1)) (/ (+ (neg (neg (log x))) (log z)) t) (+ (neg (neg (log x))) (log z)) (neg (neg (log x))) (neg (log x)) (log x) (+ (* (neg (log t)) (/ (- a 1/2) t)) 1) (neg (log t)) (/ (- a 1/2) t) 1) |
Compiled 3 044 188 to 966 739 computations (68.2% saved)
| 1 787× | binary-search |
| 1 151× | left-value |
| 1 762× | narrow-enough |
| 25× | predicate-same |
| 12.7s | 143 781× | 0 | valid |
| 909.0ms | 3 888× | 1 | valid |
| 163.0ms | 2 668× | 0 | invalid |
| 23.0ms | 178× | 2 | valid |
| 6.0ms | 34× | 1 | invalid |
| 2.0ms | 9× | 3 | valid |
Compiled 647 920 to 656 650 computations (-1.3% saved)
ival-mult!: 3.5s (48.2% of total)ival-sub!: 1.1s (15.5% of total)ival-add!: 739.0ms (10.2% of total)ival-div!: 548.0ms (7.5% of total)ival-log: 509.0ms (7% of total)ival-sin: 225.0ms (3.1% of total)adjust: 205.0ms (2.8% of total)ival-cos: 186.0ms (2.6% of total)ival-exp: 113.0ms (1.6% of total)ival-sqrt: 88.0ms (1.2% of total)ival-fabs: 12.0ms (0.2% of total)ival-tanh: 9.0ms (0.1% of total)ival-cosh: 5.0ms (0.1% of total)Compiled 511 462 to 440 774 computations (13.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...