Herbie run
| Date: | Friday, May 9th, 2025 |
|---|---|
| Commit: | 2f8ddb36 on artem-rules-updates |
| Seed: | 2025129 |
| 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: | 207 858.7 MB |
Time bar (total: 2.7min)
| 29.0s | 224 629× | 0 | valid |
| 7.5s | 65 375× | 0 | invalid |
| 6.3s | 23 404× | 1 | valid |
| 4.2s | 14 576× | 1 | invalid |
| 2.7s | 9 723× | 2 | valid |
| 2.3s | 6 420× | 3 | valid |
| 130.0ms | 564× | 2 | invalid |
| 46.0ms | 251× | 0 | exit |
| 6.0ms | 16× | 4 | valid |
| 0.0ms | 1× | 5 | exit |
ival-mult!: 9.8s (25.7% of total)ival-div!: 4.8s (12.7% of total)adjust: 3.4s (8.9% of total)ival-pow2: 3.1s (8% of total)ival-sin: 2.5s (6.5% of total)ival-sqrt: 2.3s (6% of total)ival-exp: 2.2s (5.9% of total)ival-pow: 2.1s (5.5% of total)ival-sub!: 1.9s (5% of total)ival-add!: 1.5s (3.8% of total)ival-cos: 993.0ms (2.6% of total)ival-tan: 886.0ms (2.3% of total)ival-neg: 747.0ms (2% of total)ival-acos: 585.0ms (1.5% of total)ival-hypot: 399.0ms (1% of total)ival-log: 370.0ms (1% of total)ival-asin: 298.0ms (0.8% of total)ival-tanu: 186.0ms (0.5% of total)ival-atan: 75.0ms (0.2% of total)ival-fabs: 42.0ms (0.1% of total)ival-<: 1.0ms (0% of total)ival-and: 1.0ms (0% of total)exact: 0.0ms (0% of total)ival-pi: 0.0ms (0% of total)ival-assert: 0.0ms (0% of total)| 306× | iter-limit |
| 90× | node-limit |
| 35× | unsound |
150 calls:
| 599.0ms | l |
| 575.0ms | (sqrt.f64 (+.f64 #s(literal 1 binary64) (*.f64 (pow.f64 (/.f64 (*.f64 #s(literal 2 binary64) l) Om) #s(literal 2 binary64)) (+.f64 (pow.f64 (sin.f64 kx) #s(literal 2 binary64)) (pow.f64 (sin.f64 ky) #s(literal 2 binary64)))))) |
| 459.0ms | k |
| 432.0ms | t |
| 324.0ms | x |
Compiled 10 486 to 11 856 computations (-13.1% saved)
1164 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 186.0ms | U* | @ | 0 | ((sqrt (* (* (* 2 n) U) (- (- t (* 2 (/ (* l l) Om))) (* (* n (pow (/ l Om) 2)) (- U U*))))) (* (* (* 2 n) U) (- (- t (* 2 (/ (* l l) Om))) (* (* n (pow (/ l Om) 2)) (- U U*)))) (* 2 (* U (* n (- t (* 2 (/ (pow l 2) Om)))))) 2 (* U (* n (- t (* 2 (/ (pow l 2) Om))))) U (* n (- t (* 2 (/ (pow l 2) Om)))) n (- t (* 2 (/ (pow l 2) Om))) t (* 2 (/ (pow l 2) Om)) (/ (pow l 2) Om) (pow l 2) l Om (sqrt (* (* (* 2 n) U) (- (- t (* 2 (/ (* l l) Om))) (* (* n (pow (/ l Om) 2)) (- U U*))))) (* (/ (* l (* n (sqrt 2))) Om) (sqrt (* U U*))) (/ (* l (* n (sqrt 2))) Om) (* l (* n (sqrt 2))) (* n (sqrt 2)) (sqrt 2) (sqrt (* U U*)) (* U U*) U* (sqrt (* (* (* 2 n) U) (- (- t (* 2 (/ (* l l) Om))) (* (* n (pow (/ l Om) 2)) (- U U*))))) (* (* (* 2 n) U) (- (- t (* 2 (/ (* l l) Om))) (* (* n (pow (/ l Om) 2)) (- U U*)))) (+ (* -4 (/ (* U (* (pow l 2) n)) Om)) (* 2 (* U (* n t)))) (* n (+ (* -4 (/ (* U (pow l 2)) Om)) (* 2 (* U t)))) (+ (* -4 (/ (* U (pow l 2)) Om)) (* 2 (* U t))) -4 (/ (* U (pow l 2)) Om) (* U (pow l 2)) (* 2 (* U t)) (* U t) (sqrt (* (* (* 2 n) U) (- (- t (* 2 (/ (* l l) Om))) (* (* n (pow (/ l Om) 2)) (- U U*))))) (+ (* -1 (* (/ (* (pow l 2) (sqrt 2)) Om) (sqrt (/ (* U n) t)))) (* (sqrt (* U (* n t))) (sqrt 2))) (* U (+ (* -1 (* (/ (* (pow l 2) (sqrt 2)) Om) (sqrt (/ n (* U t))))) (* (sqrt (/ (* n t) U)) (sqrt 2)))) (+ (* -1 (* (/ (* (pow l 2) (sqrt 2)) Om) (sqrt (/ n (* U t))))) (* (sqrt (/ (* n t) U)) (sqrt 2))) -1 (* (/ (* (pow l 2) (sqrt 2)) Om) (sqrt (/ n (* U t)))) (/ (* (pow l 2) (sqrt 2)) Om) (* (pow l 2) (sqrt 2)) (sqrt (/ n (* U t))) (/ n (* U t)) (* (sqrt (/ (* n t) U)) (sqrt 2)) (sqrt (/ (* n t) U)) (/ (* n t) U) (* n t) (sqrt (* (* (* 2 n) U) (- (- t (* 2 (/ (* l l) Om))) (* (* n (pow (/ l Om) 2)) (- U U*))))) (+ (* -1 (* (/ (* (pow l 2) (sqrt 2)) Om) (sqrt (/ (* U n) t)))) (* (sqrt (* U (* n t))) (sqrt 2))) (* t (+ (* -1 (* (/ (* (pow l 2) (sqrt 2)) Om) (sqrt (/ (* U n) (pow t 3))))) (* (sqrt (/ (* U n) t)) (sqrt 2)))) (+ (* -1 (* (/ (* (pow l 2) (sqrt 2)) Om) (sqrt (/ (* U n) (pow t 3))))) (* (sqrt (/ (* U n) t)) (sqrt 2))) (* (/ (* (pow l 2) (sqrt 2)) Om) (sqrt (/ (* U n) (pow t 3)))) (sqrt (/ (* U n) (pow t 3))) (/ (* U n) (pow t 3)) (* U n) (pow t 3) 3 (* (sqrt (/ (* U n) t)) (sqrt 2)) (sqrt (/ (* U n) t)) (/ (* U n) t)) |
| 154.0ms | f | @ | -inf | ((/ (* (log (/ (cosh (* (* -1/4 f) (PI))) (sinh (* (* 1/4 f) (PI))))) -4) (PI)) (* (log (/ (cosh (* (* -1/4 f) (PI))) (sinh (* (* 1/4 f) (PI))))) -4) (log (/ (cosh (* (* -1/4 f) (PI))) (sinh (* (* 1/4 f) (PI))))) (/ (cosh (* (* -1/4 f) (PI))) (sinh (* (* 1/4 f) (PI)))) (cosh (* (* -1/4 f) (PI))) (* (* -1/4 f) (PI)) (* -1/4 f) -1/4 f (PI) (sinh (* (* 1/4 f) (PI))) (* (* 1/4 f) (PI)) (* 1/4 f) 1/4 -4 (neg (* (/ 1 (/ (PI) 4)) (log (/ (+ (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))) (- (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))))))) (* (/ (log (/ -2 (* (* (PI) -1/2) f))) (PI)) -4) (/ (log (/ -2 (* (* (PI) -1/2) f))) (PI)) (log (/ -2 (* (* (PI) -1/2) f))) (/ -2 (* (* (PI) -1/2) f)) -2 (* (* (PI) -1/2) f) (* (PI) -1/2) -1/2 (* (neg (/ 4 (PI))) (log (/ (cosh (* (* -1/4 f) (PI))) (sinh (* (* 1/4 f) (PI)))))) (neg (/ 4 (PI))) (/ 4 (PI)) 4 (neg (log (pow (/ (cosh (* (* -1/4 f) (PI))) (sinh (* (* 1/4 f) (PI)))) (/ 4 (PI))))) (log (pow (/ (cosh (* (* -1/4 f) (PI))) (sinh (* (* 1/4 f) (PI)))) (/ 4 (PI)))) (pow (/ (cosh (* (* -1/4 f) (PI))) (sinh (* (* 1/4 f) (PI)))) (/ 4 (PI))) (neg (* (/ 1 (/ (PI) 4)) (log (/ (+ (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))) (- (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))))))) (+ (* (* -2 (/ (+ (* (+ (* (* (+ (* (/ (* 1/192 (* (* (PI) (PI)) (PI))) (* (* (PI) (PI)) 1/4)) -2) (* (/ (* (PI) (PI)) (PI)) 1/8)) (PI)) 1/2) 0) f) 0) (PI))) f) (* (/ (log (/ -2 (* (* (PI) -1/2) f))) (PI)) -4)) (* -2 (/ (+ (* (+ (* (* (+ (* (/ (* 1/192 (* (* (PI) (PI)) (PI))) (* (* (PI) (PI)) 1/4)) -2) (* (/ (* (PI) (PI)) (PI)) 1/8)) (PI)) 1/2) 0) f) 0) (PI))) (/ (+ (* (+ (* (* (+ (* (/ (* 1/192 (* (* (PI) (PI)) (PI))) (* (* (PI) (PI)) 1/4)) -2) (* (/ (* (PI) (PI)) (PI)) 1/8)) (PI)) 1/2) 0) f) 0) (PI)) (+ (* (+ (* (* (+ (* (/ (* 1/192 (* (* (PI) (PI)) (PI))) (* (* (PI) (PI)) 1/4)) -2) (* (/ (* (PI) (PI)) (PI)) 1/8)) (PI)) 1/2) 0) f) 0) (+ (* (* (+ (* (/ (* 1/192 (* (* (PI) (PI)) (PI))) (* (* (PI) (PI)) 1/4)) -2) (* (/ (* (PI) (PI)) (PI)) 1/8)) (PI)) 1/2) 0) (* (+ (* (/ (* 1/192 (* (* (PI) (PI)) (PI))) (* (* (PI) (PI)) 1/4)) -2) (* (/ (* (PI) (PI)) (PI)) 1/8)) (PI)) (+ (* (/ (* 1/192 (* (* (PI) (PI)) (PI))) (* (* (PI) (PI)) 1/4)) -2) (* (/ (* (PI) (PI)) (PI)) 1/8)) (/ (* 1/192 (* (* (PI) (PI)) (PI))) (* (* (PI) (PI)) 1/4)) (* 1/192 (* (* (PI) (PI)) (PI))) 1/192 (* (* (PI) (PI)) (PI)) (* (PI) (PI)) (* (* (PI) (PI)) 1/4) (* (/ (* (PI) (PI)) (PI)) 1/8) (/ (* (PI) (PI)) (PI)) 1/8 1/2 0) |
| 120.0ms | U | @ | -inf | ((* (* (* (cos (* -1/2 K)) J) -2) (cosh (asinh (/ U (* (cos (* -1/2 K)) (+ J J)))))) (* (* (cos (* -1/2 K)) J) -2) (* (cos (* -1/2 K)) J) (cos (* -1/2 K)) (* -1/2 K) -1/2 K J -2 (cosh (asinh (/ U (* (cos (* -1/2 K)) (+ J J))))) (asinh (/ U (* (cos (* -1/2 K)) (+ J J)))) (/ U (* (cos (* -1/2 K)) (+ J J))) U (* (cos (* -1/2 K)) (+ J J)) (+ J J) (* (* (* -2 J) (cos (/ K 2))) (sqrt (+ 1 (pow (/ U (* (* 2 J) (cos (/ K 2)))) 2)))) (neg U) (* (* (* -2 J) (cos (/ K 2))) (sqrt (+ 1 (pow (/ U (* (* 2 J) (cos (/ K 2)))) 2)))) (* (* -2 J) (cos (/ K 2))) (* -2 J) (cos (/ K 2)) (/ K 2) 2 (sqrt (+ 1 (pow (/ U (* (* 2 J) (cos (/ K 2)))) 2))) 1 (* (* (* -2 J) (cos (/ K 2))) (sqrt (+ 1 (pow (/ U (* (* 2 J) (cos (/ K 2)))) 2)))) (sqrt (+ 1 (pow (/ U (* (* 2 J) (cos (/ K 2)))) 2))) (+ 1 (pow (/ U (* (* 2 J) (cos (/ K 2)))) 2)) (+ (* (/ (* U U) (* J J)) 1/4) 1) (/ (* U U) (* J J)) (* U U) (* J J) 1/4 (* (* (* -2 J) (cos (/ K 2))) (sqrt (+ 1 (pow (/ U (* (* 2 J) (cos (/ K 2)))) 2)))) (sqrt (+ 1 (pow (/ U (* (* 2 J) (cos (/ K 2)))) 2))) (+ 1 (pow (/ U (* (* 2 J) (cos (/ K 2)))) 2)) (pow (/ U (* (* 2 J) (cos (/ K 2)))) 2) (/ U (* (* 2 J) (cos (/ K 2)))) (* (/ U J) 1/2) (/ U J) 1/2) |
| 113.0ms | Om | @ | -inf | ((sqrt (* (/ 1 2) (+ 1 (/ 1 (sqrt (+ 1 (* (pow (/ (* 2 l) Om) 2) (+ (pow (sin kx) 2) (pow (sin ky) 2))))))))) (* (/ 1 2) (+ 1 (/ 1 (sqrt (+ 1 (* (pow (/ (* 2 l) Om) 2) (+ (pow (sin kx) 2) (pow (sin ky) 2)))))))) (/ 1 2) 1 2 (+ 1 (/ 1 (sqrt (+ 1 (* (pow (/ (* 2 l) Om) 2) (+ (pow (sin kx) 2) (pow (sin ky) 2))))))) (/ 1 (sqrt (+ 1 (* (pow (/ (* 2 l) Om) 2) (+ (pow (sin kx) 2) (pow (sin ky) 2)))))) (sqrt (+ 1 (* (pow (/ (* 2 l) Om) 2) (+ (pow (sin kx) 2) (pow (sin ky) 2))))) (+ 1 (* (pow (/ (* 2 l) Om) 2) (+ (pow (sin kx) 2) (pow (sin ky) 2)))) (* (pow (/ (* 2 l) Om) 2) (+ (pow (sin kx) 2) (pow (sin ky) 2))) (pow (/ (* 2 l) Om) 2) (/ (* 2 l) Om) (* 2 l) l Om (+ (pow (sin kx) 2) (pow (sin ky) 2)) (pow (sin kx) 2) (sin kx) kx (pow (sin ky) 2) (sin ky) ky) |
| 113.0ms | K | @ | 0 | ((* (* (* (cos (* -1/2 K)) J) -2) (cosh (asinh (/ U (* (cos (* -1/2 K)) (+ J J)))))) (* (* (cos (* -1/2 K)) J) -2) (* (cos (* -1/2 K)) J) (cos (* -1/2 K)) (* -1/2 K) -1/2 K J -2 (cosh (asinh (/ U (* (cos (* -1/2 K)) (+ J J))))) (asinh (/ U (* (cos (* -1/2 K)) (+ J J)))) (/ U (* (cos (* -1/2 K)) (+ J J))) U (* (cos (* -1/2 K)) (+ J J)) (+ J J) (* (* (* -2 J) (cos (/ K 2))) (sqrt (+ 1 (pow (/ U (* (* 2 J) (cos (/ K 2)))) 2)))) (neg U) (* (* (* -2 J) (cos (/ K 2))) (sqrt (+ 1 (pow (/ U (* (* 2 J) (cos (/ K 2)))) 2)))) (* (* -2 J) (cos (/ K 2))) (* -2 J) (cos (/ K 2)) (/ K 2) 2 (sqrt (+ 1 (pow (/ U (* (* 2 J) (cos (/ K 2)))) 2))) 1 (* (* (* -2 J) (cos (/ K 2))) (sqrt (+ 1 (pow (/ U (* (* 2 J) (cos (/ K 2)))) 2)))) (sqrt (+ 1 (pow (/ U (* (* 2 J) (cos (/ K 2)))) 2))) (+ 1 (pow (/ U (* (* 2 J) (cos (/ K 2)))) 2)) (+ (* (/ (* U U) (* J J)) 1/4) 1) (/ (* U U) (* J J)) (* U U) (* J J) 1/4 (* (* (* -2 J) (cos (/ K 2))) (sqrt (+ 1 (pow (/ U (* (* 2 J) (cos (/ K 2)))) 2)))) (sqrt (+ 1 (pow (/ U (* (* 2 J) (cos (/ K 2)))) 2))) (+ 1 (pow (/ U (* (* 2 J) (cos (/ K 2)))) 2)) (pow (/ U (* (* 2 J) (cos (/ K 2)))) 2) (/ U (* (* 2 J) (cos (/ K 2)))) (* (/ U J) 1/2) (/ U J) 1/2) |
| 29× | fuel |
| 3× | done |
Compiled 6 375 to 3 649 computations (42.8% saved)
| 32× | search |
| Probability | Valid | Unknown | Precondition | Infinite | Domain | Can't | Iter |
|---|---|---|---|---|---|---|---|
| 0% | 0% | 98.2% | 1.8% | 0% | 0% | 0% | 0 |
| 22.2% | 21.8% | 76.4% | 1.8% | 0% | 0% | 0% | 1 |
| 22.6% | 21.8% | 74.8% | 1.8% | 0% | 1.6% | 0% | 2 |
| 28.6% | 26.5% | 66.3% | 1.8% | 0% | 5.5% | 0% | 3 |
| 32.6% | 29.6% | 61.2% | 1.8% | 0% | 7.4% | 0% | 4 |
| 35.8% | 32.3% | 58% | 1.8% | 0% | 8% | 0% | 5 |
| 40.1% | 36.1% | 54% | 1.8% | 0% | 8.1% | 0% | 6 |
| 45.5% | 40.6% | 48.7% | 1.8% | 0% | 8.9% | 0% | 7 |
| 47.9% | 42.1% | 45.8% | 1.8% | 0% | 10.3% | 0% | 8 |
| 51% | 44.6% | 43% | 1.8% | 0% | 10.6% | 0% | 9 |
| 52.1% | 45.5% | 41.8% | 1.8% | 0% | 11% | 0% | 10 |
| 53.9% | 46.7% | 40% | 1.8% | 0% | 11.5% | 0% | 11 |
| 55.6% | 47.9% | 38.2% | 1.8% | 0% | 12.1% | 0% | 12 |
Compiled 798 to 574 computations (28.1% saved)
Compiled 914 207 to 271 036 computations (70.4% saved)
| 32× | node-limit |
Compiled 86 427 to 66 000 computations (23.6% saved)
Compiled 143 963 to 119 729 computations (16.8% saved)
| 182× | binary-search |
| 171× | left-value |
| 176× | narrow-enough |
| 6× | predicate-same |
| 1.4s | 10 914× | 0 | valid |
| 108.0ms | 483× | 1 | valid |
| 52.0ms | 629× | 0 | invalid |
| 16.0ms | 67× | 2 | valid |
| 14.0ms | 40× | 3 | valid |
| 10.0ms | 43× | 1 | invalid |
| 2.0ms | 7× | 2 | invalid |
Compiled 77 627 to 76 066 computations (2% saved)
ival-mult!: 219.0ms (18.3% of total)ival-div!: 144.0ms (12.1% of total)ival-tan: 143.0ms (12% of total)ival-sin: 119.0ms (10% of total)ival-neg: 109.0ms (9.1% of total)ival-pow: 102.0ms (8.5% of total)ival-add!: 89.0ms (7.4% of total)ival-pow2: 46.0ms (3.8% of total)ival-cos: 41.0ms (3.4% of total)adjust: 37.0ms (3.1% of total)ival-tanu: 36.0ms (3% of total)ival-sub!: 34.0ms (2.8% of total)ival-exp: 28.0ms (2.3% of total)ival-sqrt: 24.0ms (2% of total)ival-hypot: 19.0ms (1.6% of total)ival-fabs: 4.0ms (0.3% of total)ival-atan: 0.0ms (0% of total)Loading profile data...