Herbie run

Date:Wednesday, May 7th, 2025
Commit:efe40450 on artem-rules-updates
Seed:2025127
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:206 154.6 MB

Time bar (total: 2.8min)

sample1.2min (40.6%)

Memory
1 301.3MiB live, 79 736.5MiB allocated; 28.1s collecting garbage
Samples
28.8s224 529×0valid
6.8s64 664×0invalid
6.4s23 457×1valid
3.7s14 501×1invalid
2.9s9 802×2valid
2.4s6 396×3valid
288.0ms592×2invalid
38.0ms242×0exit
3.0ms8×4valid
Precisions
Click to see histograms. Total time spent on operations: 34.9s
ival-mult!: 8.6s (24.7% of total)
ival-div!: 4.5s (12.8% of total)
ival-pow2: 2.6s (7.6% of total)
adjust: 2.6s (7.3% of total)
ival-sin: 2.5s (7% of total)
ival-pow: 2.4s (6.7% of total)
ival-sqrt: 2.1s (6.1% of total)
ival-exp: 2.1s (6% of total)
ival-sub!: 1.5s (4.4% of total)
ival-cos: 1.3s (3.7% of total)
ival-add!: 1.2s (3.4% of total)
ival-tan: 828.0ms (2.4% of total)
ival-acos: 688.0ms (2% of total)
ival-neg: 659.0ms (1.9% of total)
ival-log: 414.0ms (1.2% of total)
ival-hypot: 323.0ms (0.9% of total)
ival-asin: 268.0ms (0.8% of total)
ival-tanu: 259.0ms (0.7% of total)
ival-atan: 81.0ms (0.2% of total)
ival-fabs: 48.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)
Bogosity

rewrite29.1s (17.1%)

Memory
128.1MiB live, 30 464.0MiB allocated; 11.1s collecting garbage
Stop Event
294×iter-limit
124×node-limit
4×unsound
Counts
28 166 → 49 920

regimes15.9s (9.3%)

Memory
-58.5MiB live, 23 044.3MiB allocated; 4.7s collecting garbage
Counts
9 394 → 752
Calls

156 calls:

762.0ms
l
537.0ms
x
440.0ms
k
433.0ms
M
379.0ms
t
Compiler

Compiled 10 773 to 12 597 computations (-16.9% saved)

series12.0s (7%)

Memory
468.9MiB live, 17 171.1MiB allocated; 2.8s collecting garbage
Counts
4 444 → 23 722
Calls

1200 calls:

TimeVariablePointExpression
251.0ms
f
@-inf
((neg (* (/ 1 (/ (PI) 4)) (log (/ (+ (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))) (- (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))))))) (* (/ (neg (log (tanh (* (* (PI) f) 1/4)))) (PI)) -4) (/ (neg (log (tanh (* (* (PI) f) 1/4)))) (PI)) (neg (log (tanh (* (* (PI) f) 1/4)))) (log (tanh (* (* (PI) f) 1/4))) (tanh (* (* (PI) f) 1/4)) (* (* (PI) f) 1/4) (* (PI) f) (PI) 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 (sqrt (PI))) (/ (neg (log (tanh (* (* (PI) f) 1/4)))) (sqrt (PI))))) (* (/ 4 (sqrt (PI))) (/ (neg (log (tanh (* (* (PI) f) 1/4)))) (sqrt (PI)))) (/ 4 (sqrt (PI))) 4 (sqrt (PI)) (/ (neg (log (tanh (* (* (PI) f) 1/4)))) (sqrt (PI))) (log (/ 1 (exp (* (/ (neg (log (tanh (* (* (PI) f) 1/4)))) (PI)) 4)))) (/ 1 (exp (* (/ (neg (log (tanh (* (* (PI) f) 1/4)))) (PI)) 4))) 1 (exp (* (/ (neg (log (tanh (* (* (PI) f) 1/4)))) (PI)) 4)) (* (/ (neg (log (tanh (* (* (PI) f) 1/4)))) (PI)) 4) (neg (* (/ 1 (/ (PI) 4)) (log (/ (* (- (exp (* (* (* (PI) f) 1/4) 2)) (exp (* (* (* (PI) f) -1/4) 2))) 1) (* (* 2 (sinh (* (* (PI) f) 1/4))) (* 2 (sinh (* (* (PI) f) 1/4)))))))) (* (/ 1 (/ (PI) 4)) (log (/ (* (- (exp (* (* (* (PI) f) 1/4) 2)) (exp (* (* (* (PI) f) -1/4) 2))) 1) (* (* 2 (sinh (* (* (PI) f) 1/4))) (* 2 (sinh (* (* (PI) f) 1/4))))))) (/ 1 (/ (PI) 4)) (/ (PI) 4) (log (/ (* (- (exp (* (* (* (PI) f) 1/4) 2)) (exp (* (* (* (PI) f) -1/4) 2))) 1) (* (* 2 (sinh (* (* (PI) f) 1/4))) (* 2 (sinh (* (* (PI) f) 1/4)))))) (/ (* (- (exp (* (* (* (PI) f) 1/4) 2)) (exp (* (* (* (PI) f) -1/4) 2))) 1) (* (* 2 (sinh (* (* (PI) f) 1/4))) (* 2 (sinh (* (* (PI) f) 1/4))))) (* (- (exp (* (* (* (PI) f) 1/4) 2)) (exp (* (* (* (PI) f) -1/4) 2))) 1) (- (exp (* (* (* (PI) f) 1/4) 2)) (exp (* (* (* (PI) f) -1/4) 2))) (exp (* (* (* (PI) f) 1/4) 2)) (* (* (* (PI) f) 1/4) 2) (exp (* (* (* (PI) f) -1/4) 2)) (* (* (* (PI) f) -1/4) 2) (* (* (PI) f) -1/4) -1/4 (* (* 2 (sinh (* (* (PI) f) 1/4))) (* 2 (sinh (* (* (PI) f) 1/4)))) (* 2 (sinh (* (* (PI) f) 1/4))) (sinh (* (* (PI) f) 1/4)))
150.0ms
f
@inf
((neg (* (/ 1 (/ (PI) 4)) (log (/ (+ (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))) (- (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))))))) (* (/ (neg (log (tanh (* (* (PI) f) 1/4)))) (PI)) -4) (/ (neg (log (tanh (* (* (PI) f) 1/4)))) (PI)) (neg (log (tanh (* (* (PI) f) 1/4)))) (log (tanh (* (* (PI) f) 1/4))) (tanh (* (* (PI) f) 1/4)) (* (* (PI) f) 1/4) (* (PI) f) (PI) 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 (sqrt (PI))) (/ (neg (log (tanh (* (* (PI) f) 1/4)))) (sqrt (PI))))) (* (/ 4 (sqrt (PI))) (/ (neg (log (tanh (* (* (PI) f) 1/4)))) (sqrt (PI)))) (/ 4 (sqrt (PI))) 4 (sqrt (PI)) (/ (neg (log (tanh (* (* (PI) f) 1/4)))) (sqrt (PI))) (log (/ 1 (exp (* (/ (neg (log (tanh (* (* (PI) f) 1/4)))) (PI)) 4)))) (/ 1 (exp (* (/ (neg (log (tanh (* (* (PI) f) 1/4)))) (PI)) 4))) 1 (exp (* (/ (neg (log (tanh (* (* (PI) f) 1/4)))) (PI)) 4)) (* (/ (neg (log (tanh (* (* (PI) f) 1/4)))) (PI)) 4) (neg (* (/ 1 (/ (PI) 4)) (log (/ (* (- (exp (* (* (* (PI) f) 1/4) 2)) (exp (* (* (* (PI) f) -1/4) 2))) 1) (* (* 2 (sinh (* (* (PI) f) 1/4))) (* 2 (sinh (* (* (PI) f) 1/4)))))))) (* (/ 1 (/ (PI) 4)) (log (/ (* (- (exp (* (* (* (PI) f) 1/4) 2)) (exp (* (* (* (PI) f) -1/4) 2))) 1) (* (* 2 (sinh (* (* (PI) f) 1/4))) (* 2 (sinh (* (* (PI) f) 1/4))))))) (/ 1 (/ (PI) 4)) (/ (PI) 4) (log (/ (* (- (exp (* (* (* (PI) f) 1/4) 2)) (exp (* (* (* (PI) f) -1/4) 2))) 1) (* (* 2 (sinh (* (* (PI) f) 1/4))) (* 2 (sinh (* (* (PI) f) 1/4)))))) (/ (* (- (exp (* (* (* (PI) f) 1/4) 2)) (exp (* (* (* (PI) f) -1/4) 2))) 1) (* (* 2 (sinh (* (* (PI) f) 1/4))) (* 2 (sinh (* (* (PI) f) 1/4))))) (* (- (exp (* (* (* (PI) f) 1/4) 2)) (exp (* (* (* (PI) f) -1/4) 2))) 1) (- (exp (* (* (* (PI) f) 1/4) 2)) (exp (* (* (* (PI) f) -1/4) 2))) (exp (* (* (* (PI) f) 1/4) 2)) (* (* (* (PI) f) 1/4) 2) (exp (* (* (* (PI) f) -1/4) 2)) (* (* (* (PI) f) -1/4) 2) (* (* (PI) f) -1/4) -1/4 (* (* 2 (sinh (* (* (PI) f) 1/4))) (* 2 (sinh (* (* (PI) f) 1/4)))) (* 2 (sinh (* (* (PI) f) 1/4))) (sinh (* (* (PI) f) 1/4)))
89.0ms
f
@-inf
((neg (* (/ 4 (sqrt (PI))) (* (neg (log (tanh (* (* 1/4 f) (PI))))) (/ 1 (sqrt (PI)))))) (* (/ 4 (sqrt (PI))) (* (neg (log (tanh (* (* 1/4 f) (PI))))) (/ 1 (sqrt (PI))))) (/ 4 (sqrt (PI))) 4 (sqrt (PI)) (PI) (* (neg (log (tanh (* (* 1/4 f) (PI))))) (/ 1 (sqrt (PI)))) (neg (log (tanh (* (* 1/4 f) (PI))))) (log (tanh (* (* 1/4 f) (PI)))) (tanh (* (* 1/4 f) (PI))) (* (* 1/4 f) (PI)) (* 1/4 f) 1/4 f (/ 1 (sqrt (PI))) 1 (* (/ 4 (PI)) (log (tanh (* (* 1/4 f) (PI))))) (/ 4 (PI)) (log (tanh (* (* 1/4 f) (PI)))) (tanh (* (* 1/4 f) (PI))) (* (* f (PI)) 1/4) (* f (PI)) (neg (* (/ 4 (sqrt (PI))) (/ (neg (log (tanh (* (* (PI) f) 1/4)))) (sqrt (PI))))) (* (/ (+ (log (* 1/4 (PI))) (log f)) (PI)) 4) (/ (+ (log (* 1/4 (PI))) (log f)) (PI)) (+ (log (* 1/4 (PI))) (log f)) (log (* 1/4 (PI))) (* 1/4 (PI)) (log f) (neg (* (/ 4 (sqrt (PI))) (/ (neg (log (tanh (* (* (PI) f) 1/4)))) (sqrt (PI))))) (* (+ (/ (log (* 1/4 (PI))) (PI)) (/ (log f) (PI))) 4) (+ (/ (log (* 1/4 (PI))) (PI)) (/ (log f) (PI))) (/ (log (* 1/4 (PI))) (PI)) (/ (log f) (PI)) (neg (* (/ 1 (/ (PI) 4)) (log (/ (+ (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))) (- (exp (* (/ (PI) 4) f)) (exp (neg (* (/ (PI) 4) f)))))))) (* (exp (* (log (/ (neg (PI)) (log (tanh (* (* f (PI)) 1/4))))) -1)) -4) (exp (* (log (/ (neg (PI)) (log (tanh (* (* f (PI)) 1/4))))) -1)) (* (log (/ (neg (PI)) (log (tanh (* (* f (PI)) 1/4))))) -1) (log (/ (neg (PI)) (log (tanh (* (* f (PI)) 1/4))))) (/ (neg (PI)) (log (tanh (* (* f (PI)) 1/4)))) (neg (PI)) (log (tanh (* (* f (PI)) 1/4))) (tanh (* (* f (PI)) 1/4)) -1 -4)
82.0ms
t
@0
((/ 2 (* (* (* (exp (- (* (log t) 3) (* (log l) 2))) (sin k)) (tan k)) (+ (+ 1 (pow (/ k t) 2)) 1))) 2 (* (* (* (exp (- (* (log t) 3) (* (log l) 2))) (sin k)) (tan k)) (+ (+ 1 (pow (/ k t) 2)) 1)) (* (* (exp (- (* (log t) 3) (* (log l) 2))) (sin k)) (tan k)) (* (exp (- (* (log t) 3) (* (log l) 2))) (sin k)) (exp (- (* (log t) 3) (* (log l) 2))) (- (* (log t) 3) (* (log l) 2)) (* (log t) 3) (log t) t 3 (* (log l) 2) (log l) l (sin k) k (tan k) (+ (+ 1 (pow (/ k t) 2)) 1) (+ 1 (pow (/ k t) 2)) 1 (pow (/ k t) 2) (/ k t) (/ 2 (* (* (* (/ (pow t 3) (* l l)) (sin k)) (tan k)) (+ (+ 1 (pow (/ k t) 2)) 1))) (/ (* l l) (* (* k k) (* (* t t) t))) (* l l) (* (* k k) (* (* t t) t)) (* k k) (* (* t t) t) (* t t) (/ 2 (* (* (* (/ (pow t 3) (* l l)) (sin k)) (tan k)) (+ (+ 1 (pow (/ k t) 2)) 1))) (/ (+ (* (/ (* (* (+ (/ 1 (* t t)) 1/3) (* l l)) (* k k)) (* (* t t) t)) -1/2) (/ (* l l) (* (* t t) t))) (* k k)) (+ (* (/ (* (* (+ (/ 1 (* t t)) 1/3) (* l l)) (* k k)) (* (* t t) t)) -1/2) (/ (* l l) (* (* t t) t))) (/ (* (* (+ (/ 1 (* t t)) 1/3) (* l l)) (* k k)) (* (* t t) t)) (* (* (+ (/ 1 (* t t)) 1/3) (* l l)) (* k k)) (* (+ (/ 1 (* t t)) 1/3) (* l l)) (+ (/ 1 (* t t)) 1/3) (/ 1 (* t t)) 1/3 -1/2 (/ (* l l) (* (* t t) t)) (/ 2 (* (* (* (/ (pow t 3) (* l l)) (sin k)) (tan k)) (+ (+ 1 (pow (/ k t) 2)) 1))) (* (* (* (/ (pow t 3) (* l l)) (sin k)) (tan k)) (+ (+ 1 (pow (/ k t) 2)) 1)) (* (* (/ (pow t 3) (* l l)) (sin k)) (tan k)) (* (/ (pow t 3) (* l l)) (sin k)) (/ (pow t 3) (* l l)) (pow t 3) (tan k) (/ 2 (* (* (* (/ (pow t 3) (* l l)) (sin k)) (tan k)) (+ (+ 1 (pow (/ k t) 2)) 1))) (* (/ (* (cos k) (* l l)) (* (* (+ (* (/ k t) (/ k t)) 2) (- 1/2 (* 1/2 (cos (* 2 k))))) (* (* t t) t))) 2) (/ (* (cos k) (* l l)) (* (* (+ (* (/ k t) (/ k t)) 2) (- 1/2 (* 1/2 (cos (* 2 k))))) (* (* t t) t))) (* (cos k) (* l l)) (cos k) (* (* (+ (* (/ k t) (/ k t)) 2) (- 1/2 (* 1/2 (cos (* 2 k))))) (* (* t t) t)) (* (+ (* (/ k t) (/ k t)) 2) (- 1/2 (* 1/2 (cos (* 2 k))))) (+ (* (/ k t) (/ k t)) 2) (- 1/2 (* 1/2 (cos (* 2 k)))) 1/2 (* 1/2 (cos (* 2 k))) (cos (* 2 k)) (* 2 k))
72.0ms
k
@inf
((/ 1 (/ (+ (* (+ 10 k) k) 1) (* (pow k m) a))) 1 (/ (+ (* (+ 10 k) k) 1) (* (pow k m) a)) (+ (* (+ (/ 10 (* (pow k m) a)) (/ k (* (pow k m) a))) k) (/ 1 (* (pow k m) a))) (+ (/ 10 (* (pow k m) a)) (/ k (* (pow k m) a))) (/ 10 (* (pow k m) a)) 10 (* (pow k m) a) (pow k m) k m a (/ k (* (pow k m) a)) (/ 1 (* (pow k m) a)) (/ (* a (pow k m)) (+ (+ 1 (* 10 k)) (* k k))) (/ a (+ (* (+ 10 k) k) 1)) (+ (* (* k a) -10) a) (* (* a k) -10) (* a k) -10 (/ (* a (pow k m)) (+ (+ 1 (* 10 k)) (* k k))) (/ a (+ (* (+ 10 k) k) 1)) (+ (* (+ 10 k) k) 1) (+ 10 k) (/ (* a (pow k m)) (+ (+ 1 (* 10 k)) (* k k))) (/ 1 (/ (+ (* (+ 10 k) k) 1) a)) (/ (+ (* (+ 10 k) k) 1) a) (+ (* (+ 10 k) k) 1) (+ 10 k) (* (* (pow k m) a) (/ 1 (+ (* (+ 10 k) k) 1))) (* (pow k m) a) (/ 1 (+ (* (+ 10 k) k) 1)) (/ (- 1 (/ 10 k)) (* k k)) (- 1 (/ 10 k)) (/ 10 k) (* k k))

derivations9.6s (5.6%)

Memory
-34.0MiB live, 9 160.3MiB allocated; 2.2s collecting garbage
Stop Event
32×fuel
Compiler

Compiled 6 918 to 3 933 computations (43.1% saved)

preprocess9.5s (5.6%)

Memory
-245.2MiB live, 11 789.3MiB allocated; 3.8s collecting garbage
Stop Event
32×node-limit
Compiler

Compiled 102 172 to 77 980 computations (23.7% saved)

analyze8.5s (5%)

Memory
125.6MiB live, 10 888.6MiB allocated; 3.2s collecting garbage
Algorithm
32×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
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
Compiler

Compiled 798 to 574 computations (28.1% saved)

eval8.4s (4.9%)

Memory
-157.6MiB live, 11 805.4MiB allocated; 3.6s collecting garbage
Compiler

Compiled 1 049 752 to 263 726 computations (74.9% saved)

prune4.5s (2.6%)

Memory
272.2MiB live, 7 050.6MiB allocated; 1.2s collecting garbage
Counts
49 416 → 2 882
Compiler

Compiled 163 897 to 131 952 computations (19.5% saved)

bsearch3.8s (2.2%)

Memory
160.3MiB live, 5 039.7MiB allocated; 630ms collecting garbage
Algorithm
218×binary-search
194×left-value
Stop Event
208×narrow-enough
10×predicate-same
Samples
1.9s14 146×0valid
224.0ms2 165×0invalid
128.0ms755×1valid
47.0ms194×2valid
21.0ms57×3valid
3.0ms19×1invalid
1.0ms3×2invalid
Compiler

Compiled 104 726 to 99 311 computations (5.2% saved)

Precisions
Click to see histograms. Total time spent on operations: 1.6s
ival-mult!: 373.0ms (23.7% of total)
ival-div!: 219.0ms (13.9% of total)
ival-sin: 186.0ms (11.8% of total)
ival-pow: 129.0ms (8.2% of total)
ival-tan: 120.0ms (7.6% of total)
ival-add!: 93.0ms (5.9% of total)
ival-neg: 88.0ms (5.6% of total)
ival-pow2: 79.0ms (5% of total)
ival-exp: 77.0ms (4.9% of total)
ival-sub!: 62.0ms (3.9% of total)
ival-sqrt: 50.0ms (3.2% of total)
adjust: 38.0ms (2.4% of total)
ival-cos: 35.0ms (2.2% of total)
ival-hypot: 16.0ms (1% of total)
ival-tanu: 6.0ms (0.4% of total)
ival-fabs: 4.0ms (0.3% of total)
ival-atan: 1.0ms (0.1% of total)

start2.0ms (0%)

Memory
4.4MiB live, 4.3MiB allocated; 0ms collecting garbage

end0.0ms (0%)

Memory
0.4MiB live, 0.5MiB allocated; 0ms collecting garbage

Profiling

Loading profile data...