Herbie run
| Date: | Saturday, April 26th, 2025 |
|---|---|
| Commit: | 45de6ef9 on artem-rules-updates |
| Seed: | 2025116 |
| 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: | 147 064.6 MB |
Time bar (total: 2.0min)
| 19.5s | 292 824× | 0 | valid |
| 6.5s | 17 633× | 2 | valid |
| 6.5s | 35 854× | 1 | valid |
| 570.0ms | 4 203× | 0 | invalid |
| 182.0ms | 441× | 3 | valid |
| 91.0ms | 988× | 0 | exit |
| 71.0ms | 101× | 4 | exit |
| 47.0ms | 101× | 3 | exit |
| 5.0ms | 43× | 1 | exit |
ival-mult!: 4.7s (21.5% of total)ival-pow: 3.5s (15.9% of total)ival-div!: 2.8s (12.6% of total)adjust: 2.2s (9.8% of total)ival-add!: 2.1s (9.4% of total)ival-sin: 2.0s (8.9% of total)ival-sub!: 1.4s (6.4% of total)ival-cos: 1.3s (5.9% of total)ival-sqrt: 568.0ms (2.6% of total)ival-exp: 522.0ms (2.4% of total)ival-pow2: 261.0ms (1.2% of total)ival-neg: 249.0ms (1.1% of total)ival-log1p: 224.0ms (1% of total)ival-atan: 78.0ms (0.4% of total)ival-expm1: 63.0ms (0.3% of total)ival-tan: 55.0ms (0.2% of total)ival-hypot: 30.0ms (0.1% of total)ival-<=: 12.0ms (0.1% of total)ival-and: 8.0ms (0% of total)ival-fabs: 4.0ms (0% of total)ival-if: 4.0ms (0% of total)ival-==: 3.0ms (0% of total)ival-assert: 1.0ms (0% of total)const: 0.0ms (0% of total)ival-<: 0.0ms (0% of total)| 348× | iter-limit |
| 143× | node-limit |
| 10× | saturated |
| 4× | unsound |
Compiled 588 053 to 196 392 computations (66.6% saved)
| 24× | fuel |
| 18× | done |
Compiled 5 249 to 2 666 computations (49.2% saved)
888 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 967.0ms | c | @ | -inf | ((/ (- (* b c) (* a d)) (+ (* c c) (* d d))) (neg (/ (+ (* a (/ d c)) (neg b)) c)) (/ (+ (* a (/ d c)) (neg b)) c) (+ (* a (/ d c)) (neg b)) a (/ d c) d c (neg b) b (/ (- (* b c) (* a d)) (+ (* c c) (* d d))) (* (/ (- (/ (* c b) a) d) (+ (* d d) (* c c))) a) (/ (- (/ (* c b) a) d) (+ (* d d) (* c c))) (/ -1 d) -1 (/ (- (* b c) (* a d)) (+ (* c c) (* d d))) (/ (- (* b (/ c d)) a) d) (- (* b (/ c d)) a) (* (/ c d) b) (/ c d) (/ (- (* b c) (* a d)) (+ (* c c) (* d d))) (/ (- b (/ (* d a) c)) c) (- b (/ (* d a) c)) (/ (* d a) c) (* d a) (/ (- (* b c) (* a d)) (+ (* c c) (* d d))) (* (/ (- (/ (* c b) a) d) (+ (* d d) (* c c))) a) (/ (- (/ (* c b) a) d) (+ (* d d) (* c c))) (- (/ (* c b) a) d) (neg d) (+ (* d d) (* c c)) (* c c)) |
| 189.0ms | b | @ | inf | ((/ (- (* b c) (* a d)) (+ (* c c) (* d d))) (neg (/ (+ (* a (/ d c)) (neg b)) c)) (/ (+ (* a (/ d c)) (neg b)) c) (+ (* a (/ d c)) (neg b)) a (/ d c) d c (neg b) b (/ (- (* b c) (* a d)) (+ (* c c) (* d d))) (* (/ (- (/ (* c b) a) d) (+ (* d d) (* c c))) a) (/ (- (/ (* c b) a) d) (+ (* d d) (* c c))) (/ -1 d) -1 (/ (- (* b c) (* a d)) (+ (* c c) (* d d))) (/ (- (* b (/ c d)) a) d) (- (* b (/ c d)) a) (* (/ c d) b) (/ c d) (/ (- (* b c) (* a d)) (+ (* c c) (* d d))) (/ (- b (/ (* d a) c)) c) (- b (/ (* d a) c)) (/ (* d a) c) (* d a) (/ (- (* b c) (* a d)) (+ (* c c) (* d d))) (* (/ (- (/ (* c b) a) d) (+ (* d d) (* c c))) a) (/ (- (/ (* c b) a) d) (+ (* d d) (* c c))) (- (/ (* c b) a) d) (neg d) (+ (* d d) (* c c)) (* c c)) |
| 84.0ms | b | @ | -inf | ((* (* (/ (/ (PI) 2) (+ b a)) (/ 1 (- b a))) (- (/ 1 a) (/ 1 b))) (* (/ (/ (PI) 2) (+ b a)) (/ 1 (- b a))) (/ (/ (PI) 2) (+ b a)) (/ (PI) 2) (PI) 2 (+ b a) b a (/ 1 (- b a)) 1 (- b a) (- (/ 1 a) (/ 1 b)) (/ 1 a) (/ 1 b) (* (* (/ (PI) 2) (/ 1 (- (* b b) (* a a)))) (- (/ 1 a) (/ 1 b))) (* (/ (PI) (* (* a a) b)) 1/2) (/ (PI) (* (* a a) b)) (* (* a a) b) (* a a) 1/2 (* (* (/ (PI) 2) (/ 1 (- (* b b) (* a a)))) (- (/ 1 a) (/ 1 b))) (* (/ (PI) 2) (/ 1 (- (* b b) (* a a)))) (* (/ (PI) (* a a)) -1/2) (/ (PI) (* a a)) -1/2 (* (* (/ (PI) 2) (/ 1 (- (* b b) (* a a)))) (- (/ 1 a) (/ 1 b))) (/ (+ (* (/ (PI) (* b b)) 1/2) (/ (* -1/2 (* (PI) a)) (* (* b b) b))) a) (+ (* (/ (PI) (* b b)) 1/2) (/ (* -1/2 (* (PI) a)) (* (* b b) b))) (/ (PI) (* b b)) (* b b) (/ (* -1/2 (* (PI) a)) (* (* b b) b)) (* -1/2 (* (PI) a)) (* (PI) a) (* (* b b) b) (* (* (/ (PI) 2) (* (/ 1 (+ b a)) (/ 1 (- b a)))) (- (/ 1 a) (/ 1 b))) (* (/ (PI) 2) (* (/ 1 (+ b a)) (/ 1 (- b a)))) (* (/ 1 (+ b a)) (/ 1 (- b a))) (/ 1 (+ b a))) |
| 74.0ms | n | @ | 0 | ((* (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) (/ i n)) 100) (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) (/ i n)) (- (exp (* (log (+ 1 (/ i n))) n)) 1) (* (log (+ 1 (/ i n))) n) (log (+ 1 (/ i n))) (/ i n) i n 100 (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (+ (* (* (- 1/2 (/ 1/2 n)) n) i) n) (* -1/2 i) -1/2 (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (- (pow (+ 1 (/ i n)) n) 1) (pow (+ 1 (/ i n)) n) 1 (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (* (* (* n n) (/ (- (log i) (log n)) i)) 100) (* (* n n) (/ (- (log i) (log n)) i)) (* n n) (/ (- (log i) (log n)) i) (- (log i) (log n)) (log i) (log n) (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (* (* (- (exp (* (- (log i) (log n)) n)) 1) n) 100) i) (* (* (- (exp (* (- (log i) (log n)) n)) 1) n) 100) (* (- (exp (* (- (log i) (log n)) n)) 1) n) (- (exp (* (- (log i) (log n)) n)) 1) (* (- (log i) (log n)) n)) |
| 67.0ms | c | @ | 0 | ((/ (- (neg b) (exp (* (log (+ (* b b) (* (* a -4) c))) 1/2))) (+ a a)) (- (neg b) (exp (* (log (+ (* b b) (* (* a -4) c))) 1/2))) (neg b) b (exp (* (log (+ (* b b) (* (* a -4) c))) 1/2)) (* (log (+ (* b b) (* (* a -4) c))) 1/2) (log (+ (* b b) (* (* a -4) c))) (+ (* b b) (* (* a -4) c)) (* (* a -4) c) (* a -4) a -4 c 1/2 (+ a a) (/ (- (neg b) (sqrt (- (* b b) (* 4 (* a c))))) (* 2 a)) (/ (neg b) a) (/ (- (neg b) (sqrt (- (* b b) (* 4 (* a c))))) (* 2 a)) (+ (/ c b) (/ (neg b) a)) (/ c b) (/ (- (neg b) (sqrt (- (* b b) (* 4 (* a c))))) (* 2 a)) (* (+ (sqrt (* (/ c a) -4)) (/ b a)) -1/2) (+ (sqrt (* (/ c a) -4)) (/ b a)) (sqrt (* (/ c a) -4)) (* (/ c a) -4) (/ c a) (/ b a) -1/2 (/ (- (neg b) (sqrt (- (* b b) (* 4 (* a c))))) (* 2 a)) (- (neg b) (sqrt (- (* b b) (* 4 (* a c))))) (* (- (/ (neg b) c) (sqrt (* -4 (/ a c)))) c) (- (/ (neg b) c) (sqrt (* -4 (/ a c)))) (/ (- (neg b) (sqrt (* (* a -4) c))) c) (- (neg b) (sqrt (* (* a -4) c))) (sqrt (* (* a -4) c)) (* 2 a) 2) |
| 33× | node-limit |
| 9× | saturated |
Compiled 19 143 to 13 604 computations (28.9% saved)
96 calls:
| 574.0ms | x |
| 340.0ms | b |
| 236.0ms | (*.f64 (cos.f64 x) (exp.f64 (*.f64 #s(literal 10 binary64) (*.f64 x x)))) |
| 225.0ms | a |
| 184.0ms | d |
Compiled 7 041 to 5 604 computations (20.4% saved)
| 43× | search |
| 2× | random |
| Probability | Valid | Unknown | Precondition | Infinite | Domain | Can't | Iter |
|---|---|---|---|---|---|---|---|
| 0% | 0% | 54.5% | 45.5% | 0% | 0% | 0% | 0 |
| 21.4% | 11.7% | 42.9% | 45.5% | 0% | 0% | 0% | 1 |
| 37.4% | 20.4% | 34.1% | 45.5% | 0% | 0% | 0% | 2 |
| 48.7% | 26.2% | 27.7% | 45.5% | 0% | 0.6% | 0% | 3 |
| 57.7% | 30.7% | 22.6% | 45.5% | 0% | 1.2% | 0% | 4 |
| 71.2% | 37.7% | 15.3% | 45.5% | 0% | 1.6% | 0% | 5 |
| 72.9% | 38.4% | 14.3% | 45.5% | 0% | 1.8% | 0% | 6 |
| 77.9% | 40.7% | 11.6% | 45.5% | 0% | 2.2% | 0% | 7 |
| 81.5% | 42.6% | 9.7% | 45.5% | 0% | 2.3% | 0% | 8 |
| 84.1% | 43.8% | 8.3% | 45.5% | 0% | 2.5% | 0% | 9 |
| 86.2% | 44.6% | 7.2% | 45.5% | 0% | 2.7% | 0% | 10 |
| 88.2% | 45.6% | 6.1% | 45.5% | 0% | 2.8% | 0% | 11 |
| 89.1% | 45.9% | 5.6% | 45.5% | 0% | 2.9% | 0% | 12 |
Compiled 1 402 to 721 computations (48.6% saved)
Compiled 85 461 to 65 340 computations (23.5% saved)
| 217× | binary-search |
| 80× | left-value |
| 204× | narrow-enough |
| 12× | predicate-same |
| 1× | predicate-failed |
| 791.0ms | 10 642× | 0 | valid |
| 178.0ms | 566× | 2 | valid |
| 162.0ms | 824× | 1 | valid |
| 86.0ms | 1 315× | 0 | invalid |
| 11.0ms | 16× | 3 | valid |
| 2.0ms | 17× | 1 | exit |
| 1.0ms | 16× | 0 | exit |
Compiled 110 694 to 86 938 computations (21.5% saved)
ival-mult!: 309.0ms (36% of total)ival-pow: 132.0ms (15.4% of total)ival-div!: 101.0ms (11.8% of total)ival-sub!: 92.0ms (10.7% of total)ival-add!: 58.0ms (6.7% of total)adjust: 53.0ms (6.2% of total)ival-neg: 48.0ms (5.6% of total)ival-exp: 37.0ms (4.3% of total)ival-sqrt: 27.0ms (3.1% of total)ival-log1p: 4.0ms (0.5% of total)Loading profile data...