Herbie run
| Date: | Sunday, May 11th, 2025 |
|---|---|
| Commit: | 32d50127 on autofix-28-1 |
| Seed: | 2025131 |
| 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: | 995 178.7 MB |
Time bar (total: 13.9min)
| 2.7min | 2 144 343× | 0 | valid |
| 17.7s | 69 811× | 1 | valid |
| 8.0s | 64 019× | 0 | invalid |
| 1.8s | 6 054× | 2 | valid |
| 717.0ms | 1 204× | 5 | exit |
| 483.0ms | 1 895× | 1 | invalid |
| 256.0ms | 360× | 4 | exit |
| 161.0ms | 653× | 3 | valid |
| 2.0ms | 23× | 1 | exit |
| 1.0ms | 3× | 4 | valid |
ival-mult!: 43.1s (42.6% of total)ival-div!: 10.6s (10.5% of total)ival-add!: 9.9s (9.8% of total)ival-sub!: 9.4s (9.3% of total)ival-log: 7.7s (7.6% of total)ival-sqrt: 5.3s (5.2% of total)adjust: 4.2s (4.1% of total)ival-sin: 3.9s (3.9% of total)ival-cos: 3.1s (3% of total)ival-exp: 2.2s (2.2% of total)ival-cosh: 410.0ms (0.4% of total)ival-tan: 323.0ms (0.3% of total)ival-acos: 297.0ms (0.3% of total)ival-sinh: 215.0ms (0.2% of total)ival-hypot: 209.0ms (0.2% of total)ival-fabs: 195.0ms (0.2% of total)ival-tanh: 104.0ms (0.1% of total)const: 0.0ms (0% of total)| 2 248× | iter-limit |
| 853× | node-limit |
| 72× | unsound |
| 16× | saturated |
| 156× | fuel |
| 113× | done |
Compiled 30 313 to 18 732 computations (38.2% saved)
512 calls:
| 10.0s | x |
| 8.5s | y |
| 7.3s | z |
| 4.0s | t |
| 2.5s | a |
Compiled 32 849 to 55 158 computations (-67.9% saved)
8955 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 3.7s | x | @ | inf | ((/ (* x (exp (- (+ (* y (log z)) (* (- t 1) (log a))) b))) y) (* x (exp (- (+ (* y (log z)) (* (- t 1) (log a))) b))) x (exp (- (+ (* y (log z)) (* (- t 1) (log a))) b)) (- (+ (* y (log z)) (* (- t 1) (log a))) b) (+ (* y (log z)) (* (- t 1) (log a))) (* y (log z)) y (log z) z (* (- t 1) (log a)) (- t 1) t 1 (log a) a b) |
| 322.0ms | a | @ | -inf | ((/ (* x (exp (- (+ (* y (log z)) (* (- t 1) (log a))) b))) y) (* x (exp (- (+ (* y (log z)) (* (- t 1) (log a))) b))) x (exp (- (+ (* y (log z)) (* (- t 1) (log a))) b)) (* (/ 1 a) (exp (- (* (log z) y) b))) (/ (pow z y) a) (pow z y) z y a (* x (/ (exp (- (+ (* y (log z)) (* (- t 1) (log a))) b)) y)) (/ (exp (- (+ (* y (log z)) (* (- t 1) (log a))) b)) y) (exp (- (+ (* y (log z)) (* (- t 1) (log a))) b)) (- (+ (* y (log z)) (* (- t 1) (log a))) b) (neg b) b (/ (* x (exp (- (+ (* y (log z)) (* (- t 1) (log a))) b))) y) (* x (/ (* (/ 1 a) (exp (- (* (log z) y) b))) y)) (/ (* (/ 1 a) (exp (- (* (log z) y) b))) y) (* (/ 1 a) (exp (- (* (log z) y) b))) (/ (exp (neg b)) a) (exp (neg b)) (/ (* x (exp (- (+ (* y (log z)) (* (- t 1) (log a))) b))) y) (* x (/ (* (/ 1 a) (exp (- (* (log z) y) b))) y)) (/ (* (pow z y) x) (* a y)) (* (pow z y) x) (* a y) (* x (/ (exp (- (+ (* y (log z)) (* (- t 1) (log a))) b)) y)) (/ (exp (- (+ (* y (log z)) (* (- t 1) (log a))) b)) y) (exp (- (+ (* y (log z)) (* (- t 1) (log a))) b)) (- (+ (* y (log z)) (* (- t 1) (log a))) b) (* (log a) t) (log a) t) |
| 305.0ms | x | @ | inf | ((+ x (* (* y z) z)) (* (+ (* z (/ (* z y) x)) 1) x) (+ (* z (/ (* z y) x)) 1) z (/ (* z y) x) (* z y) y x 1 (+ x (* (* y z) z)) (* (neg (+ (* (neg y) (/ (* z z) x)) -1)) x) (neg (+ (* (neg y) (/ (* z z) x)) -1)) (+ x (* (* y z) z)) (* (* z y) z) (+ x (* (* y z) z)) (* (neg (+ (* (neg y) (/ (* z z) x)) -1)) x) (neg (+ (* (neg y) (/ (* z z) x)) -1)) (+ (* (neg y) (/ (* z z) x)) -1) (* (* (neg z) y) (/ z x)) (* (neg z) y) (neg z) (/ z x) (+ x (* (* y z) z)) (* (+ (* z (* (/ z x) y)) 1) x) (+ (* z (* (/ z x) y)) 1) (* (/ z x) y)) |
| 228.0ms | x | @ | -inf | ((- (* x (- 0 (log (/ y x)))) z) (* x (- 0 (log (/ y x)))) x (- 0 (log (/ y x))) 0 (log (/ y x)) (/ y x) y z (- (* x (log (/ x y))) z) (neg z) (- (* x (log (/ x y))) z) (* (+ (* (/ (log (/ x y)) z) x) -1) z) (+ (* (/ (log (/ x y)) z) x) -1) (/ (log (/ x y)) z) (log (/ x y)) (/ x y) -1 (- (+ (* (neg (log y)) x) (* (log x) x)) z) (+ (* (neg (log y)) x) (* (log x) x)) (neg (log y)) (log y) (* (log x) x) (log x) (/ (+ (* (* z z) z) (pow (* (log (/ x y)) x) 3)) (+ (* (* (log (/ x y)) x) (- (* (log (/ x y)) x) (neg z))) (* z z))) (+ (* (* z z) z) (pow (* (log (/ x y)) x) 3)) (* z z) (pow (* (log (/ x y)) x) 3) (* (log (/ x y)) x) 3 (+ (* (* (log (/ x y)) x) (- (* (log (/ x y)) x) (neg z))) (* z z)) (- (* (log (/ x y)) x) (neg z))) |
| 215.0ms | x | @ | -inf | ((/ (+ 2 (* (* (* (sqrt 2) (- (sin x) (/ (sin y) 16))) (- (sin y) (/ (sin x) 16))) (- (cos x) (cos y)))) (+ (* (+ (* (cos x) (/ (- (sqrt 5) 1) 2)) 1) 3) (* (* (/ 4 (* (+ (sqrt 5) 3) 2)) (cos y)) 3))) (+ 2 (* (* (* (sqrt 2) (- (sin x) (/ (sin y) 16))) (- (sin y) (/ (sin x) 16))) (- (cos x) (cos y)))) 2 (* (* (* (sqrt 2) (- (sin x) (/ (sin y) 16))) (- (sin y) (/ (sin x) 16))) (- (cos x) (cos y))) (* (* (sqrt 2) (- (sin x) (/ (sin y) 16))) (- (sin y) (/ (sin x) 16))) (* (sqrt 2) (- (sin x) (/ (sin y) 16))) (sqrt 2) (- (sin x) (/ (sin y) 16)) (sin x) x (/ (sin y) 16) (sin y) y 16 (- (sin y) (/ (sin x) 16)) (/ (sin x) 16) (- (cos x) (cos y)) (cos x) (cos y) (+ (* (+ (* (cos x) (/ (- (sqrt 5) 1) 2)) 1) 3) (* (* (/ 4 (* (+ (sqrt 5) 3) 2)) (cos y)) 3)) (+ (* (cos x) (/ (- (sqrt 5) 1) 2)) 1) (/ (- (sqrt 5) 1) 2) (- (sqrt 5) 1) (sqrt 5) 5 1 3 (* (* (/ 4 (* (+ (sqrt 5) 3) 2)) (cos y)) 3) (* (/ 4 (* (+ (sqrt 5) 3) 2)) (cos y)) (/ 4 (* (+ (sqrt 5) 3) 2)) 4 (* (+ (sqrt 5) 3) 2) (+ (sqrt 5) 3) (/ (+ 2 (* (* (* (sqrt 2) (- (sin x) (/ (sin y) 16))) (- (sin y) (/ (sin x) 16))) (- (cos x) (cos y)))) (* 3 (+ (+ 1 (* (/ (- (sqrt 5) 1) 2) (cos x))) (* (/ (- 3 (sqrt 5)) 2) (cos y))))) (* (/ (+ (* (* -1/16 (- 1/2 (* 1/2 (cos (* 2 x))))) (* (- (cos x) 1) (sqrt 2))) 2) (+ (* 1/2 (+ (* (- (sqrt 5) 1) (cos x)) (- 3 (sqrt 5)))) 1)) 1/3) 1/3 (/ (+ (* (- (cos x) (cos y)) (* (- (sin y) (/ (sin x) 16)) (* (- (sin x) (/ (sin y) 16)) (sqrt 2)))) 2) (* (+ (* (cos y) (/ (- 3 (sqrt 5)) 2)) (+ (* (cos x) (/ (- (sqrt 5) 1) 2)) 1)) 3)) (+ (* (- (cos x) (cos y)) (* (- (sin y) (/ (sin x) 16)) (* (- (sin x) (/ (sin y) 16)) (sqrt 2)))) 2) (+ (* (* (- (cos x) 1) (sqrt 2)) (* (- 1/2 (* (cos (+ x x)) 1/2)) -1/16)) 2) (* (- (cos x) 1) (sqrt 2)) (- (cos x) 1) (* (- 1/2 (* (cos (+ x x)) 1/2)) -1/16) (- 1/2 (* (cos (+ x x)) 1/2)) 1/2 (* (cos (+ x x)) 1/2) (cos (+ x x)) (+ x x) -1/16 (* (+ (* (cos y) (/ (- 3 (sqrt 5)) 2)) (+ (* (cos x) (/ (- (sqrt 5) 1) 2)) 1)) 3) (+ (* (cos y) (/ (- 3 (sqrt 5)) 2)) (+ (* (cos x) (/ (- (sqrt 5) 1) 2)) 1)) (/ (- 3 (sqrt 5)) 2) (- 3 (sqrt 5)) (/ (/ (+ (* (* (* (- (sin x) (/ (sin y) 16)) (sqrt 2)) (- (sin y) (/ (sin x) 16))) (- (cos x) (cos y))) 2) 3) (+ (* (cos y) (/ (- 3 (sqrt 5)) 2)) (+ (* (cos x) (/ (- (sqrt 5) 1) 2)) 1))) (/ (+ (* (* (* (- (sin x) (/ (sin y) 16)) (sqrt 2)) (- (sin y) (/ (sin x) 16))) (- (cos x) (cos y))) 2) 3) (+ (* (* (* (- (sin x) (/ (sin y) 16)) (sqrt 2)) (- (sin y) (/ (sin x) 16))) (- (cos x) (cos y))) 2) (* (* (- (sin x) (/ (sin y) 16)) (sqrt 2)) (- (sin y) (/ (sin x) 16))) (* (- (sin x) (/ (sin y) 16)) (sqrt 2)) (- (cos x) (cos y)) (cos y) (+ (* (* y y) -1/2) 1) (* y y) -1/2 (+ (* (cos y) (/ (- 3 (sqrt 5)) 2)) (+ (* (cos x) (/ (- (sqrt 5) 1) 2)) 1)) (/ (+ 2 (* (* (* (sqrt 2) (- (sin x) (/ (sin y) 16))) (- (sin y) (/ (sin x) 16))) (- (cos x) (cos y)))) (* 3 (+ (+ 1 (* (/ (- (sqrt 5) 1) 2) (cos x))) (* (/ (/ (- 9 (* (sqrt 5) (sqrt 5))) (+ (sqrt 5) 3)) 2) (cos y))))) (+ 2 (* (* (* (sqrt 2) (- (sin x) (/ (sin y) 16))) (- (sin y) (/ (sin x) 16))) (- (cos x) (cos y)))) (* (* (* (sqrt 2) (- (sin x) (/ (sin y) 16))) (- (sin y) (/ (sin x) 16))) (- (cos x) (cos y))) (* (* (sqrt 2) (- (sin x) (/ (sin y) 16))) (- (sin y) (/ (sin x) 16))) (* (sqrt 2) (- (sin x) (/ (sin y) 16))) (- (sin x) (/ (sin y) 16)) (/ (sin y) 16) (sin y) (* (+ (* (- (* (* y y) 1/120) 1/6) (* y y)) 1) y) (+ (* (- (* (* y y) 1/120) 1/6) (* y y)) 1) (- (* (* y y) 1/120) 1/6) (* (* y y) 1/120) 1/120 1/6 (- (sin y) (/ (sin x) 16)) (* 3 (+ (+ 1 (* (/ (- (sqrt 5) 1) 2) (cos x))) (* (/ (/ (- 9 (* (sqrt 5) (sqrt 5))) (+ (sqrt 5) 3)) 2) (cos y)))) (+ (+ 1 (* (/ (- (sqrt 5) 1) 2) (cos x))) (* (/ (/ (- 9 (* (sqrt 5) (sqrt 5))) (+ (sqrt 5) 3)) 2) (cos y))) (+ 1 (* (/ (- (sqrt 5) 1) 2) (cos x))) (* (/ (- (sqrt 5) 1) 2) (cos x)) (* (/ (/ (- 9 (* (sqrt 5) (sqrt 5))) (+ (sqrt 5) 3)) 2) (cos y)) (/ (/ (- 9 (* (sqrt 5) (sqrt 5))) (+ (sqrt 5) 3)) 2) (/ (- 9 (* (sqrt 5) (sqrt 5))) (+ (sqrt 5) 3)) (- 9 (* (sqrt 5) (sqrt 5))) 9 (* (sqrt 5) (sqrt 5))) |
| 237× | node-limit |
| 32× | saturated |
Compiled 136 920 to 109 878 computations (19.8% saved)
Compiled 3 103 245 to 958 785 computations (69.1% saved)
| 1 728× | binary-search |
| 997× | left-value |
| 1 708× | narrow-enough |
| 20× | predicate-same |
| 13.0s | 135 823× | 0 | valid |
| 683.0ms | 3 313× | 1 | valid |
| 229.0ms | 2 959× | 0 | invalid |
| 29.0ms | 113× | 1 | invalid |
| 16.0ms | 108× | 2 | valid |
| 1.0ms | 4× | 3 | valid |
Compiled 710 712 to 716 077 computations (-0.8% saved)
ival-mult!: 4.5s (53.1% of total)ival-sub!: 1.3s (15.4% of total)ival-add!: 612.0ms (7.3% of total)ival-log: 516.0ms (6.1% of total)ival-div!: 489.0ms (5.8% of total)ival-cos: 336.0ms (4% of total)ival-sin: 298.0ms (3.5% of total)adjust: 134.0ms (1.6% of total)ival-exp: 124.0ms (1.5% of total)ival-sqrt: 122.0ms (1.4% of total)ival-cosh: 9.0ms (0.1% of total)ival-fabs: 7.0ms (0.1% of total)ival-tanh: 5.0ms (0.1% of total)ival-sinh: 1.0ms (0% of total)Compiled 506 169 to 440 908 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...