Herbie run
| Date: | Thursday, April 3rd, 2025 |
|---|---|
| Commit: | f7a7cb35 on main |
| Seed: | 2025093 |
| 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: | 160 269.1 MB |
Time bar (total: 2.1min)
| 19.5s | 293 302× | 0 | valid |
| 7.7s | 35 441× | 1 | valid |
| 7.1s | 17 557× | 2 | valid |
| 332.0ms | 4 229× | 0 | invalid |
| 168.0ms | 452× | 3 | valid |
| 159.0ms | 101× | 4 | exit |
| 123.0ms | 951× | 0 | exit |
| 49.0ms | 101× | 3 | exit |
| 4.0ms | 32× | 1 | exit |
ival-mult!: 5.4s (23.3% of total)ival-pow: 3.3s (14.2% of total)adjust: 2.9s (12.4% of total)ival-add!: 2.8s (12.2% of total)ival-div!: 1.9s (8.3% of total)ival-sin: 1.8s (7.6% of total)ival-sub!: 1.5s (6.6% of total)ival-cos: 1.3s (5.7% of total)ival-sqrt: 533.0ms (2.3% of total)ival-exp: 495.0ms (2.1% of total)ival-neg: 436.0ms (1.9% of total)ival-pow2: 276.0ms (1.2% of total)ival-tan: 109.0ms (0.5% of total)ival-hypot: 103.0ms (0.4% of total)ival-log1p: 88.0ms (0.4% of total)ival-expm1: 82.0ms (0.4% of total)ival-atan: 77.0ms (0.3% 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)| 362× | iter-limit |
| 146× | node-limit |
| 9× | saturated |
| 3× | unsound |
| Operator | Subexpression | Explanation | Count | |
|---|---|---|---|---|
-.f64 | #f | cancellation | 1289 | 1 |
+.f64 | #f | cancellation | 354 | 84 |
-.f64 | (-.f64 (*.f64 #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64) t) #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64)) | oflow-left | 221 | 0 |
sqrt.f64 | #f | oflow-rescue | 184 | 0 |
/.f64 | #f | o/o | 178 | 0 |
log.f64 | (log.f64 (+.f64 #s(literal 1 binary64) x)) | sensitivity | 163 | 0 |
/.f64 | #f | n/o | 142 | 0 |
pow.f64 | (pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n) | sensitivity | 129 | 0 |
-.f64 | #f | nan-rescue | 103 | 0 |
/.f64 | #f | u/n | 97 | 0 |
/.f64 | #f | n/u | 67 | 0 |
+.f64 | #f | nan-rescue | 53 | 0 |
/.f64 | #f | o/n | 50 | 0 |
/.f64 | (/.f64 (*.f64 (-.f64 x y) (+.f64 x y)) (+.f64 (*.f64 x x) (*.f64 y y))) | u/u | 34 | 0 |
| ↳ | (*.f64 (-.f64 x y) (+.f64 x y)) | underflow | 34 | |
| ↳ | (*.f64 y y) | underflow | 85 | |
| ↳ | (*.f64 x x) | underflow | 123 | |
| ↳ | (+.f64 (*.f64 x x) (*.f64 y y)) | underflow | 34 | |
*.f64 | #f | n*u | 28 | 0 |
*.f64 | #f | n*o | 24 | 0 |
pow.f64 | (pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n) | oflow-rescue | 16 | 0 |
| ↳ | (pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n) | overflow | 22 | |
| ↳ | (/.f64 i n) | overflow | 16 | |
| ↳ | (+.f64 #s(literal 1 binary64) (/.f64 i n)) | overflow | 16 | |
sqrt.f64 | #f | uflow-rescue | 10 | 0 |
| Predicted + | Predicted - | |
|---|---|---|
| + | 3805 | 224 |
| - | 112 | 6611 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 3805 | 159 | 65 |
| - | 112 | 182 | 6429 |
| number | freq |
|---|---|
| 0 | 6835 |
| 1 | 3470 |
| 2 | 394 |
| 3 | 53 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 30 | 1 | 0 |
| - | 2 | 0 | 9 |
| 1.9s | 16 820× | 0 | valid |
| 724.0ms | 3 172× | 1 | valid |
| 559.0ms | 1 472× | 2 | valid |
| 79.0ms | 40× | 3 | valid |
Compiled 7 535 to 1 486 computations (80.3% saved)
ival-mult!: 365.0ms (23.5% of total)ival-pow: 248.0ms (16% of total)adjust: 178.0ms (11.5% of total)ival-div!: 150.0ms (9.7% of total)ival-sin: 140.0ms (9% of total)ival-add!: 139.0ms (9% of total)ival-sub!: 136.0ms (8.8% of total)ival-cos: 66.0ms (4.3% of total)ival-exp: 31.0ms (2% of total)ival-sqrt: 30.0ms (1.9% of total)ival-log1p: 24.0ms (1.5% of total)ival-pow2: 14.0ms (0.9% of total)ival-neg: 14.0ms (0.9% of total)ival-tan: 7.0ms (0.5% of total)ival-atan: 5.0ms (0.3% of total)ival-expm1: 3.0ms (0.2% of total)const: 0.0ms (0% of total)Compiled 2 711 435 to 212 182 computations (92.2% saved)
| 25× | fuel |
| 17× | done |
Compiled 30 169 to 2 740 computations (90.9% saved)
96 calls:
| 510.0ms | x |
| 360.0ms | b |
| 247.0ms | a |
| 218.0ms | c |
| 197.0ms | (*.f64 (cos.f64 x) (exp.f64 (*.f64 #s(literal 10 binary64) (*.f64 x x)))) |
Compiled 8 140 to 5 554 computations (31.8% saved)
897 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 141.0ms | b | @ | 0 | ((* (+ a (+ b (+ c d))) 2) (* 2 (+ b (+ (+ d c) a))) 2 (+ b (+ (+ d c) a)) b (+ (+ d c) a) (* c (+ 1 (/ (+ a d) c))) c (+ 1 (/ (+ a d) c)) 1 (/ (+ a d) c) (+ a d) a d (* (- (/ (* a a) (- a (+ (+ d c) b))) (/ (pow (+ (+ d c) b) 2) (- a (+ (+ d c) b)))) 2) (- (/ (* a a) (- a (+ (+ d c) b))) (/ (pow (+ (+ d c) b) 2) (- a (+ (+ d c) b)))) (* (+ a (+ b (+ c d))) 2) (+ a (+ b (+ c d))) (+ b (+ c d)) (* (+ a (+ b (+ c d))) 2) (* (+ (* (/ (+ (+ c b) a) d) 2) 2) d) (+ (* (/ (+ (+ c b) a) d) 2) 2) (/ (+ (+ c b) a) d) (+ (+ c b) a) (+ c b) (* (+ a (+ b (+ c d))) 2) (* (+ (* (/ (+ (+ d c) b) a) 2) 2) a) (+ (* (/ (+ (+ d c) b) a) 2) 2) (/ (+ (+ d c) b) a) (+ (+ d c) b) (+ d c)) |
| 98.0ms | i | @ | -inf | ((* 100 (* (/ (- (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) i) (- (exp (* (log (+ 1 (/ i n))) n)) 1) (* (log (+ 1 (/ i n))) n) i n (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (/ (* (- (exp i) 1) n) i) (+ (* (* n i) 1/2) n) (* n 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 (/ i n) (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (/ (* (log (/ i n)) (* n n)) i) (* (log (/ i n)) (* n n)) (log (/ i n)) (* n n) (* 100 (* (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i) n)) (* (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i) n) (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i) (* n (/ (+ (* -1 (log n)) (log i)) i)) (/ (+ (* -1 (log n)) (log i)) i) (+ (* -1 (log n)) (log i)) -1 (log n) (log i)) |
| 79.0ms | x | @ | inf | ((/ (- x (sin x)) (tan x)) (* (+ (* (- (* (* (- (* -143/604800 (* x x)) 11/15120) x) x) 23/360) (* x x)) 1/6) (* x x)) (+ (* (- (* (* (- (* -143/604800 (* x x)) 11/15120) x) x) 23/360) (* x x)) 1/6) (- (* (* (- (* -143/604800 (* x x)) 11/15120) x) x) 23/360) (* (* (- (* -143/604800 (* x x)) 11/15120) x) x) (* (- (* -143/604800 (* x x)) 11/15120) x) (- (* -143/604800 (* x x)) 11/15120) (* -143/604800 (* x x)) -143/604800 (* x x) x 11/15120 23/360 1/6 (/ (- x (sin x)) (tan x)) (* (* x x) 1/6) (/ (- x (sin x)) (tan x)) (* (* (+ (* (- (* -11/15120 (* x x)) 23/360) (* x x)) 1/6) x) x) (* (+ (* (- (* -11/15120 (* x x)) 23/360) (* x x)) 1/6) x) (+ (* (- (* -11/15120 (* x x)) 23/360) (* x x)) 1/6) (- (* -11/15120 (* x x)) 23/360) (* -11/15120 (* x x)) -11/15120 (/ (- x (sin x)) (tan (+ (PI) x))) (- x (sin x)) (sin x) (tan (+ (PI) x)) (+ (PI) x) (PI) (- (/ x (tan x)) (/ (sin x) (tan x))) (/ x (tan x)) (tan x) (/ (sin x) (tan x))) |
| 75.0ms | i | @ | -inf | ((* 100 (* (/ (- (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) i) (- (exp (* (log (+ 1 (/ i n))) n)) 1) (* (log (+ 1 (/ i n))) n) (log (+ 1 (/ i n))) (/ i n) i n (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (/ (* (- (exp i) 1) n) i) (* (- (exp i) 1) n) (- (exp i) 1) (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (* (* 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))) (/ (* (* n 100) (- (exp (* (- (log i) (log n)) n)) 1)) i) (* (* n 100) (- (exp (* (- (log i) (log n)) n)) 1)) (* n 100) (- (exp (* (- (log i) (log n)) n)) 1) (* (- (log i) (log n)) n)) |
| 64.0ms | b | @ | -inf | ((* (/ (PI) (* 2 (+ a b))) (* (pow (- b a) -1) (- (pow a -1) (pow b -1)))) (/ (PI) (* 2 (+ a b))) (PI) (* 2 (+ a b)) 2 (+ a b) a b (* (pow (- b a) -1) (- (pow a -1) (pow b -1))) (pow (* b a) -1) (* b a) -1 (* (/ (PI) (* 2 (+ a b))) (* (pow (- b a) -1) (- (pow a -1) (pow b -1)))) (* (/ (PI) (* (* b b) a)) 1/2) (/ (PI) (* (* b b) a)) (* (* b b) a) (* b b) 1/2 (* (* (/ (PI) 2) (/ 1 (- (* b b) (* a a)))) (- (/ 1 a) (/ 1 b))) (/ (+ (* (/ (PI) b) -1/2) (* (/ (PI) a) 1/2)) (* b b)) (+ (* (/ (PI) b) -1/2) (* (/ (PI) a) 1/2)) (/ (PI) b) -1/2 (* (/ (PI) a) 1/2) (/ (PI) a) (* (* (/ (/ (PI) 2) (+ b a)) (/ 1 (- b a))) (- (/ 1 a) (/ 1 b))) (* (/ (/ (PI) 2) (+ b a)) (/ 1 (- b a))) (/ (/ (PI) 2) (+ b a)) (* (/ (PI) b) 1/2) (/ 1 (- b a)) 1 (- b a) (- (/ 1 a) (/ 1 b)) (/ 1 a) (/ 1 b) (* (/ (PI) (* 2 (+ a b))) (* (pow (- b a) -1) (/ (- (* 1 b) (* a 1)) (* b a)))) (* (pow (- b a) -1) (/ (- (* 1 b) (* a 1)) (* b a))) (pow (- b a) -1) (/ (- (* 1 b) (* a 1)) (* b a)) (- (* 1 b) (* a 1)) (* 1 b) (* a 1)) |
| 32× | node-limit |
| 10× | saturated |
Compiled 80 796 to 16 078 computations (80.1% saved)
Compiled 150 350 to 62 661 computations (58.3% 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)
| 184× | binary-search |
| 75× | left-value |
| 168× | narrow-enough |
| 15× | predicate-same |
| 1× | predicate-failed |
| 1.0s | 10 802× | 0 | valid |
| 355.0ms | 1 206× | 1 | valid |
| 316.0ms | 510× | 2 | valid |
| 111.0ms | 1 411× | 0 | invalid |
| 19.0ms | 200× | 0 | exit |
| 11.0ms | 10× | 3 | valid |
| 0.0ms | 2× | 1 | exit |
Compiled 187 325 to 83 779 computations (55.3% saved)
ival-mult!: 449.0ms (33.7% of total)ival-pow: 240.0ms (18% of total)ival-div!: 164.0ms (12.3% of total)ival-sqrt: 121.0ms (9.1% of total)ival-neg: 89.0ms (6.7% of total)ival-add!: 83.0ms (6.2% of total)ival-sub!: 69.0ms (5.2% of total)adjust: 67.0ms (5% of total)ival-exp: 49.0ms (3.7% of total)ival-expm1: 3.0ms (0.2% of total)Loading profile data...