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: | 917 967.3 MB |
Time bar (total: 13.6min)
| 2.5min | 2 145 007× | 0 | valid |
| 19.7s | 69 241× | 1 | valid |
| 7.6s | 63 830× | 0 | invalid |
| 1.7s | 5 928× | 2 | valid |
| 733.0ms | 1 150× | 5 | exit |
| 348.0ms | 1 758× | 1 | invalid |
| 237.0ms | 383× | 4 | exit |
| 205.0ms | 678× | 3 | valid |
| 2.0ms | 16× | 1 | exit |
| 2.0ms | 10× | 4 | valid |
ival-mult!: 37.8s (38.8% of total)ival-div!: 11.1s (11.3% of total)ival-sub!: 10.5s (10.7% of total)ival-add!: 9.5s (9.7% of total)ival-log: 8.9s (9.1% of total)ival-sqrt: 5.2s (5.3% of total)adjust: 4.0s (4.1% of total)ival-sin: 3.9s (4% of total)ival-cos: 3.3s (3.4% of total)ival-exp: 1.9s (2% of total)ival-hypot: 297.0ms (0.3% of total)ival-tan: 265.0ms (0.3% of total)ival-cosh: 228.0ms (0.2% of total)ival-fabs: 211.0ms (0.2% of total)ival-acos: 205.0ms (0.2% of total)ival-sinh: 175.0ms (0.2% of total)ival-tanh: 93.0ms (0.1% of total)| 2 215× | iter-limit |
| 850× | node-limit |
| 65× | unsound |
| 13× | saturated |
512 calls:
| 9.9s | z |
| 9.9s | x |
| 8.7s | y |
| 4.6s | t |
| 2.8s | a |
Compiled 32 725 to 56 166 computations (-71.6% saved)
| 148× | fuel |
| 121× | done |
Compiled 30 288 to 18 467 computations (39% saved)
| 237× | node-limit |
| 32× | saturated |
Compiled 142 603 to 113 883 computations (20.1% saved)
8889 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 4.9s | x | @ | -inf | ((- 1 (log (- 1 (/ (- x y) (- 1 y))))) 1 (log (- 1 (/ (- x y) (- 1 y)))) (- 1 (/ (- x y) (- 1 y))) (* (neg x) (+ (neg (/ (- 1 (/ (neg y) (- 1 y))) x)) (/ 1 (- 1 y)))) (+ (neg (- (/ (neg y) (- 1 y)) 1)) (/ (neg x) (- 1 y))) (neg (- (/ (neg y) (- 1 y)) 1)) (- (/ (neg y) (- 1 y)) 1) (/ (neg y) (- 1 y)) (neg y) y (- 1 y) (/ (neg x) (- 1 y)) (neg x) x (- 1 (log (- 1 (/ (- x y) (- 1 y))))) (- (+ (/ x (* (+ (/ y (- 1 y)) 1) (- 1 y))) 1) (log (+ (/ y (- 1 y)) 1))) (+ x 1) (- 1 (log (- 1 (/ (- x y) (- 1 y))))) (log (- 1 (/ (- x y) (- 1 y)))) (- 1 (/ (- x y) (- 1 y))) (/ (- x y) (- 1 y)) (- 1 (log (- 1 (/ (- x y) (- 1 y))))) (log (- 1 (/ (- x y) (- 1 y)))) (- 1 (/ (- x y) (- 1 y))) (neg (/ (- 1 x) y)) (/ x y) (- 1 (log (- 1 (/ (- x y) (- 1 y))))) (log (- 1 (/ (- x y) (- 1 y)))) (- 1 (/ (- x y) (- 1 y))) (neg (/ (- 1 x) y)) (/ (- x 1) y) (- x 1)) |
| 1.9s | b | @ | -inf | ((* x (exp (+ (* y (- (log z) t)) (* a (- (log (- 1 z)) b))))) x (exp (+ (* y (- (log z) t)) (* a (- (log (- 1 z)) b)))) (+ (* y (- (log z) t)) (* a (- (log (- 1 z)) b))) (+ (* (neg a) b) (+ (* (+ (* (* a z) -1/2) (neg a)) z) (* (- (log z) t) y))) (* (neg a) (+ (* (+ (* 1/2 z) 1) z) b)) (neg a) a (+ (* (+ (* 1/2 z) 1) z) b) (+ (* 1/2 z) 1) 1/2 z 1 b (* x (exp (+ (* y (- (log z) t)) (* a (- (log (- 1 z)) b))))) (* (exp (* (- (log (- 1 z)) b) a)) x) (* (exp (+ (* y (- (log z) t)) (* a (- (log (- 1 z)) b)))) x) (exp (+ (* y (- (log z) t)) (* a (- (log (- 1 z)) b)))) (+ (* y (- (log z) t)) (* a (- (log (- 1 z)) b))) (* (neg a) b) (* x (exp (+ (* y (- (log z) t)) (* a (- (log (- 1 z)) b))))) (* (exp (* (- (log z) t) y)) x) (exp (* (- (log z) t) y)) (pow z y) y (* x (exp (+ (* y (- (log z) t)) (* a (- (log (- 1 z)) b))))) (* (exp (* (- (log (- 1 z)) b) a)) x) (exp (* (- (log (- 1 z)) b) a)) (* (- (log (- 1 z)) b) a) (- (log (- 1 z)) b) (log (- 1 z)) (neg z)) |
| 409.0ms | z | @ | 0 | ((- x (/ (- (/ y 3) (/ t (* 3 y))) z)) x (/ (- (/ y 3) (/ t (* 3 y))) z) (- (/ y 3) (/ t (* 3 y))) (/ y 3) y 3 (/ t (* 3 y)) t (* 3 y) z (+ (- x (/ y (* z 3))) (/ t (* (* z 3) y))) (/ (* (- (/ t y) y) 1/3) z) (* (* 1/3 (/ (- (/ t (* y y)) 1) z)) y) (* 1/3 (/ (- (/ t (* y y)) 1) z)) (/ -1/3 z) -1/3 (+ (- x (/ y (* z 3))) (/ t (* (* z 3) y))) (/ (* 1/3 t) (* z y)) (* 1/3 t) 1/3 (* z y) (+ (/ t (* (* 3 y) z)) (- x (/ y (* z 3)))) (/ t (* (* 3 y) z)) (* (* 3 y) z) (- x (/ y (* z 3))) (- x (- (/ y (* 3 z)) (/ t (* (* 3 z) y)))) (- (/ y (* 3 z)) (/ t (* (* 3 z) y))) (/ (* 1/3 (/ (- (* y y) t) z)) y) (* 1/3 (/ (- (* y y) t) z)) (/ (- (* y y) t) z) (- (* y y) t) (* y y)) |
| 249.0ms | z | @ | -inf | ((+ (- (+ (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 (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (+ (log x) (- (+ (* (log t) (- a 1/2)) (log z)) t)) (log x) x (- (+ (* (log t) (- a 1/2)) (log z)) t) (neg 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 t) (- a 1/2)) (neg (neg (log y)))) (log z)) (+ (* (log t) (- a 1/2)) (neg (neg (log y)))) (* (log t) a) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (+ (* (- a 1/2) (log t)) (log (* y z))) t) (+ (* (- a 1/2) (log t)) (log (* y z))) (log (* y z)) (* y z) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (+ (log (* z x)) (* (log t) (- a 1/2))) t) (log (* (pow t (- a 1/2)) (* z x))) (* (pow t (- a 1/2)) (* z x)) (pow t (- a 1/2)) (* z x)) |
| 225.0ms | x | @ | 0 | ((/ (/ 1 (+ (* (* z y) z) y)) x) (/ 1 (+ (* (* z y) z) y)) 1 (+ (* (* z y) z) y) (* z y) z y x (/ (/ 1 x) (* y (+ 1 (* z z)))) (/ (/ 1 y) x) (/ 1 y) (/ (/ 1 x) (+ (* (* y z) z) y)) (/ 1 (* (* (* z z) y) x)) (* (* (* z z) y) x) (* (* z z) y) (* z z) (/ (/ 1 y) (* x (+ (* z z) 1))) (* x (+ (* z z) 1)) (+ (* z z) 1) (/ 1 (* (+ (* (* z y) z) y) x)) (* (+ (* (* z y) z) y) x)) |
Compiled 2 963 776 to 931 041 computations (68.6% saved)
Compiled 503 011 to 438 389 computations (12.8% saved)
| 1 833× | binary-search |
| 1 058× | left-value |
| 1 813× | narrow-enough |
| 20× | predicate-same |
| 12.4s | 141 635× | 0 | valid |
| 915.0ms | 4 062× | 1 | valid |
| 126.0ms | 2 037× | 0 | invalid |
| 24.0ms | 151× | 2 | valid |
| 9.0ms | 50× | 1 | invalid |
| 5.0ms | 19× | 3 | valid |
| 1.0ms | 5× | 4 | valid |
Compiled 679 920 to 685 722 computations (-0.9% saved)
ival-mult!: 3.5s (47.8% of total)ival-sub!: 993.0ms (13.5% of total)ival-add!: 957.0ms (13% of total)ival-div!: 543.0ms (7.4% of total)ival-log: 479.0ms (6.5% of total)ival-sin: 244.0ms (3.3% of total)ival-cos: 234.0ms (3.2% of total)adjust: 155.0ms (2.1% of total)ival-exp: 108.0ms (1.5% of total)ival-sqrt: 108.0ms (1.5% of total)ival-tanh: 13.0ms (0.2% of total)ival-cosh: 7.0ms (0.1% of total)ival-fabs: 6.0ms (0.1% of total)| 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...