Herbie run
| Date: | Wednesday, April 30th, 2025 |
|---|---|
| Commit: | 77680327 on prove-soundness |
| Seed: | 2025120 |
| 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: | 133 807.8 MB |
Time bar (total: 2.1min)
| 21.7s | 292 999× | 0 | valid |
| 8.1s | 17 658× | 2 | valid |
| 8.0s | 35 657× | 1 | valid |
| 381.0ms | 4 294× | 0 | invalid |
| 237.0ms | 438× | 3 | valid |
| 159.0ms | 972× | 0 | exit |
| 58.0ms | 101× | 4 | exit |
| 54.0ms | 101× | 3 | exit |
| 8.0ms | 55× | 1 | exit |
ival-mult!: 6.2s (24.3% of total)ival-pow: 5.0s (19.5% of total)adjust: 2.5s (9.8% of total)ival-sin: 2.5s (9.6% of total)ival-div!: 2.2s (8.5% of total)ival-cos: 1.8s (6.9% of total)ival-add!: 1.8s (6.8% of total)ival-sub!: 1.4s (5.5% of total)ival-sqrt: 747.0ms (2.9% of total)ival-exp: 464.0ms (1.8% of total)ival-neg: 456.0ms (1.8% of total)ival-pow2: 263.0ms (1% of total)ival-expm1: 110.0ms (0.4% of total)ival-tan: 92.0ms (0.4% of total)ival-log1p: 81.0ms (0.3% of total)ival-atan: 75.0ms (0.3% of total)ival-hypot: 15.0ms (0.1% of total)ival-<=: 12.0ms (0% of total)ival-and: 7.0ms (0% of total)ival-if: 4.0ms (0% of total)ival-fabs: 4.0ms (0% of total)ival-<: 4.0ms (0% of total)ival-==: 2.0ms (0% of total)ival-assert: 1.0ms (0% of total)ival-pi: 0.0ms (0% of total)const: 0.0ms (0% of total)| 360× | iter-limit |
| 141× | node-limit |
| 10× | saturated |
| 5× | unsound |
| 37× | node-limit |
| 5× | saturated |
Compiled 17 117 to 12 314 computations (28.1% saved)
| 25× | fuel |
| 17× | done |
Compiled 5 277 to 2 614 computations (50.5% saved)
Compiled 574 659 to 178 274 computations (69% saved)
885 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 474.0ms | x2 | @ | -inf | ((+ x1 (+ (+ (+ (+ (* (+ (* (* (* 2 x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) (- (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)) 3)) (* (* x1 x1) (- (* 4 (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) 6))) (+ (* x1 x1) 1)) (* (* (* 3 x1) x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)))) (* (* x1 x1) x1)) x1) (* 3 (/ (- (- (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))))) x1 (+ (+ (+ (+ (* (+ (* (* (* 2 x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) (- (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)) 3)) (* (* x1 x1) (- (* 4 (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) 6))) (+ (* x1 x1) 1)) (* (* (* 3 x1) x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)))) (* (* x1 x1) x1)) x1) (* 3 (/ (- (- (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)))) (+ (+ (+ (* (+ (* (* (* 2 x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) (- (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)) 3)) (* (* x1 x1) (- (* 4 (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) 6))) (+ (* x1 x1) 1)) (* (* (* 3 x1) x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)))) (* (* x1 x1) x1)) x1) (+ (+ (* (+ (* (* (* 2 x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) (- (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)) 3)) (* (* x1 x1) (- (* 4 (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) 6))) (+ (* x1 x1) 1)) (* (* (* 3 x1) x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)))) (* (* x1 x1) x1)) (+ (* (+ (* (* (* 2 x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) (- (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)) 3)) (* (* x1 x1) (- (* 4 (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) 6))) (+ (* x1 x1) 1)) (* (* (* 3 x1) x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)))) (* (+ (* (* (* 2 x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) (- (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)) 3)) (* (* x1 x1) (- (* 4 (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) 6))) (+ (* x1 x1) 1)) (+ (* (* (* 2 x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) (- (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)) 3)) (* (* x1 x1) (- (* 4 (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) 6))) (* (* (* 2 x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) (- (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)) 3)) (* (* 2 x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) (* 2 x1) 2 (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)) (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* (* 3 x1) x1) (* 2 x2)) (* (* 3 x1) x1) (* 3 x1) 3 (* 2 x2) x2 (+ (* x1 x1) 1) (* x1 x1) 1 (- (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)) 3) (* (* x1 x1) (- (* 4 (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) 6)) (- (* 4 (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) 6) (* 4 (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) 4 6 (* (* (* 3 x1) x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) (* (* x1 x1) x1) (* 3 (/ (- (- (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) (/ (- (- (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)) (- (- (* (* 3 x1) x1) (* 2 x2)) x1) (- (* (* 3 x1) x1) (* 2 x2))) |
| 97.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) 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) x) (- (* (* (- (* -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 x)) (- x (sin x)) (* (* (+ (* -1/120 (* x x)) 1/6) x) (* x x)) (* (+ (* -1/120 (* x x)) 1/6) x) (+ (* -1/120 (* x x)) 1/6) -1/120 (tan x) (/ (- x (sin x)) (tan x)) (- x (sin x)) (* (+ (* (* (- (* (* (+ (* -1/362880 (* x x)) 1/5040) x) x) 1/120) x) x) 1/6) (* (* x x) x)) (+ (* (* (- (* (* (+ (* -1/362880 (* x x)) 1/5040) x) x) 1/120) x) x) 1/6) (* (- (* (* (+ (* -1/362880 (* x x)) 1/5040) x) x) 1/120) x) (- (* (* (+ (* -1/362880 (* x x)) 1/5040) x) x) 1/120) (* (* (+ (* -1/362880 (* x x)) 1/5040) x) x) (* (+ (* -1/362880 (* x x)) 1/5040) x) (+ (* -1/362880 (* x x)) 1/5040) -1/362880 1/5040 1/120 (* (* x x) x)) |
| 89.0ms | n | @ | -inf | ((* (* (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) n) 100) (* (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) n) (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) (- (exp (* (log (+ (/ i n) 1)) n)) 1) (- (exp i) 1) i n 100 (* 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 i) (* (* (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) n) 100) (* (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) n) (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) (+ (* (- 1/2 (/ 1/2 n)) i) 1) (- 1/2 (/ 1/2 n)) 1/2 (/ 1/2 n) 1 (* (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) (* n 100)) (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) (- (exp (* (log (+ (/ i n) 1)) n)) 1) (* (log (* (/ 1 n) i)) n) (log (* (/ 1 n) i)) (* (/ 1 n) i) (/ 1 n) (* n 100) (* (* (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) n) 100) (* (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) n) (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) (- (exp (* (log (+ (/ i n) 1)) n)) 1) (+ (* (log i) n) (* (neg n) (log n))) (log i) (* (neg n) (log n)) (neg n) (log n)) |
| 72.0ms | n | @ | 0 | ((* (* (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) n) 100) (* (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) n) (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) (- (exp (* (log (+ (/ i n) 1)) n)) 1) (- (exp i) 1) i n 100 (* 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 i) (* (* (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) n) 100) (* (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) n) (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) (+ (* (- 1/2 (/ 1/2 n)) i) 1) (- 1/2 (/ 1/2 n)) 1/2 (/ 1/2 n) 1 (* (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) (* n 100)) (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) (- (exp (* (log (+ (/ i n) 1)) n)) 1) (* (log (* (/ 1 n) i)) n) (log (* (/ 1 n) i)) (* (/ 1 n) i) (/ 1 n) (* n 100) (* (* (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) n) 100) (* (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) n) (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) (- (exp (* (log (+ (/ i n) 1)) n)) 1) (+ (* (log i) n) (* (neg n) (log n))) (log i) (* (neg n) (log n)) (neg n) (log n)) |
| 69.0ms | i | @ | 0 | ((/ (* 100 (- (exp (* (log (+ 1 (/ i n))) n)) 1)) (/ i n)) (* 100 (- (exp (* (log (+ 1 (/ i n))) n)) 1)) 100 (- (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)) (/ (* (- (exp i) 1) n) i) (* (- (exp i) 1) n) (- (exp i) 1) (/ (* 100 (- (exp (* (log (+ (/ i n) 1)) n)) 1)) (/ i n)) (* 100 (- (exp (* (log (+ (/ i n) 1)) n)) 1)) (- (exp (* (log (+ (/ i n) 1)) n)) 1) (* (log (+ (/ i n) 1)) n) (* (* (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) n) 100) (* (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) n) (/ (- (exp (* (log (+ (/ i n) 1)) n)) 1) i) (- (exp (* (log (+ (/ i n) 1)) n)) 1) (* (log (* (/ 1 n) i)) n) (log (* (/ 1 n) i)) (* (/ 1 n) i) (/ 1 n) 1 (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (- (pow (+ 1 (/ i n)) n) 1) (+ (* (log i) n) (* (neg (log n)) n)) (log i) (* (neg (log n)) n) (neg (log n)) (log n)) |
96 calls:
| 414.0ms | x |
| 274.0ms | b |
| 210.0ms | c |
| 210.0ms | a |
| 199.0ms | d |
Compiled 6 809 to 5 477 computations (19.6% 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 89 979 to 65 629 computations (27.1% saved)
| 153× | binary-search |
| 101× | left-value |
| 143× | narrow-enough |
| 9× | predicate-same |
| 1× | predicate-failed |
| 813.0ms | 9 594× | 0 | valid |
| 413.0ms | 1 294× | 1 | valid |
| 380.0ms | 683× | 2 | valid |
| 125.0ms | 1 790× | 0 | invalid |
| 12.0ms | 13× | 3 | valid |
Compiled 76 585 to 60 190 computations (21.4% saved)
ival-pow: 352.0ms (27.7% of total)ival-mult!: 338.0ms (26.6% of total)ival-div!: 242.0ms (19.1% of total)adjust: 128.0ms (10.1% of total)ival-add!: 96.0ms (7.6% of total)ival-sub!: 52.0ms (4.1% of total)ival-sqrt: 34.0ms (2.7% of total)ival-neg: 20.0ms (1.6% of total)ival-log1p: 3.0ms (0.2% of total)ival-expm1: 3.0ms (0.2% of total)ival-exp: 2.0ms (0.2% of total)Loading profile data...