Herbie run

Date:Wednesday, May 14th, 2025
Commit:79007786 on artem-rules-updates
Seed:2025134
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:457 690.8 MB

Time bar (total: 5.9min)

sample3.6min (60.9%)

Memory
6 010.6MiB live, 283 815.5MiB allocated; 1.7min collecting garbage
Samples
2.1min14 866×3exit
41.5s268 065×0valid
7.2s28 855×1valid
1.2s10 957×0invalid
799.0ms2 548×2valid
169.0ms1 543×1exit
138.0ms693×1invalid
85.0ms6×5exit
24.0ms2×4exit
0.0ms1×3valid
Precisions
Click to see histograms. Total time spent on operations: 2.6min
ival-mult!: 26.7s (16.9% of total)
adjust: 21.0s (13.3% of total)
ival-exp: 20.5s (13% of total)
ival-pow2: 20.1s (12.7% of total)
ival-log: 16.5s (10.5% of total)
ival-sub!: 9.5s (6% of total)
ival-div!: 9.0s (5.7% of total)
ival-add!: 7.9s (5% of total)
ival-neg: 7.4s (4.7% of total)
ival-sqrt: 6.0s (3.8% of total)
ival-fmax: 2.2s (1.4% of total)
ival-sin: 1.7s (1.1% of total)
ival-fabs: 1.4s (0.9% of total)
ival-fmin: 1.1s (0.7% of total)
ival-cos: 911.0ms (0.6% of total)
ival-tan: 807.0ms (0.5% of total)
ival-cosu: 770.0ms (0.5% of total)
ival-floor: 713.0ms (0.5% of total)
ival-sinu: 611.0ms (0.4% of total)
ival-<=: 511.0ms (0.3% of total)
ival-expm1: 494.0ms (0.3% of total)
ival-sinh: 417.0ms (0.3% of total)
ival-and: 290.0ms (0.2% of total)
ival-log2: 222.0ms (0.1% of total)
ival-if: 216.0ms (0.1% of total)
ival-log1p: 130.0ms (0.1% of total)
ival-atan: 127.0ms (0.1% of total)
ival-asin: 123.0ms (0.1% of total)
ival->=: 70.0ms (0% of total)
ival->: 48.0ms (0% of total)
ival-assert: 27.0ms (0% of total)
ival-<: 26.0ms (0% of total)
const: 1.0ms (0% of total)
ival-pi: 0.0ms (0% of total)
Bogosity

rewrite32.1s (9.1%)

Memory
497.9MiB live, 33 469.3MiB allocated; 9.1s collecting garbage
Stop Event
171×iter-limit
141×saturated
120×node-limit
21×unsound
Counts
25 464 → 51 209

analyze30.1s (8.5%)

Memory
494.4MiB live, 40 096.9MiB allocated; 12.0s collecting garbage
Algorithm
37×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%21%79%0%0%0%0
25.7%5.4%15.6%79%0%0%0%1
26.5%5.6%15.5%79%0%0%0%2
26.5%5.6%15.4%79%0%0%0%3
28.6%6%15%79%0%0%0%4
40.9%8.6%12.4%79%0%0%0%5
46.2%9.7%11.3%79%0%0%0%6
53.2%11%9.7%79%0%0.4%0%7
55.6%11.5%9.2%79%0%0.4%0%8
60.6%12.5%8.1%79%0%0.4%0%9
63.8%13.1%7.4%79%0%0.5%0%10
66.1%13.6%7%79%0%0.5%0%11
67.5%13.9%6.7%79%0%0.5%0%12
Compiler

Compiled 20 293 to 1 873 computations (90.8% saved)

regimes19.5s (5.5%)

Memory
423.5MiB live, 29 160.3MiB allocated; 6.9s collecting garbage
Counts
7 362 → 422
Calls

167 calls:

570.0ms
x
547.0ms
(+.f32 (+.f32 (*.f32 (*.f32 (cos.f32 (*.f32 (*.f32 uy #s(literal 2 binary32)) (PI.f32))) (sqrt.f32 (-.f32 #s(literal 1 binary32) (*.f32 (*.f32 (*.f32 (-.f32 #s(literal 1 binary32) ux) maxCos) ux) (*.f32 (*.f32 (-.f32 #s(literal 1 binary32) ux) maxCos) ux))))) xi) (*.f32 (*.f32 (sin.f32 (*.f32 (*.f32 uy #s(literal 2 binary32)) (PI.f32))) (sqrt.f32 (-.f32 #s(literal 1 binary32) (*.f32 (*.f32 (*.f32 (-.f32 #s(literal 1 binary32) ux) maxCos) ux) (*.f32 (*.f32 (-.f32 #s(literal 1 binary32) ux) maxCos) ux))))) yi)) (*.f32 (*.f32 (*.f32 (-.f32 #s(literal 1 binary32) ux) maxCos) ux) zi))
510.0ms
s
502.0ms
(*.f32 (*.f32 uy #s(literal 2 binary32)) (PI.f32))
416.0ms
maxCos
Compiler

Compiled 20 235 to 18 565 computations (8.3% saved)

series18.2s (5.2%)

Memory
630.5MiB live, 25 494.2MiB allocated; 7.5s collecting garbage
Counts
5 883 → 19 581
Calls

1512 calls:

TimeVariablePointExpression
929.0ms
x
@0
((* (/ (sin (* x (* (PI) tau))) (* x (* (PI) tau))) (/ (sin (* x (PI))) (* x (PI)))) (/ (sin (* x (* (PI) tau))) (* x (* (PI) tau))) (sin (* x (* (PI) tau))) (* x (* (PI) tau)) x (* (PI) tau) (PI) tau (/ (sin (* x (PI))) (* x (PI))) (sin (* x (PI))) (* x (PI)) (* (/ (sin (* (* x (PI)) tau)) (* (* x (PI)) tau)) (/ (sin (* x (PI))) (* x (PI)))) 1 (* (/ (sin (* (* x (PI)) tau)) (* (* x (PI)) tau)) (/ (sin (* x (PI))) (* x (PI)))) (/ (sin (* (* x (PI)) tau)) (* (* x (PI)) tau)) (sin (* (* x (PI)) tau)) (* (* x (PI)) tau) (/ (sin (* x (PI))) (* x (PI))) (+ (* (* -1/6 (* x x)) (* (PI) (PI))) 1) (* -1/6 (* x x)) -1/6 (* x x) (* (PI) (PI)) (* (/ (sin (* (* x (PI)) tau)) (* (* x (PI)) tau)) (/ (sin (* x (PI))) (* x (PI)))) (* (sin (* (* tau x) (PI))) (/ (sin (* (PI) x)) (* (* (* (PI) (PI)) (* x x)) tau))) (sin (* (* tau x) (PI))) (* (* tau x) (PI)) (* tau x) (/ (sin (* (PI) x)) (* (* (* (PI) (PI)) (* x x)) tau)) (sin (* (PI) x)) (* (PI) x) (* (* (* (PI) (PI)) (* x x)) tau) (* (* (PI) (PI)) (* x x)) (/ (* (/ (sin (* (PI) x)) x) (sin (* (* tau x) (PI)))) (* (PI) (* (* tau x) (PI)))) (* (/ (sin (* (PI) x)) x) (sin (* (* tau x) (PI)))) (/ (sin (* (PI) x)) x) (* (PI) (* (* tau x) (PI))))
304.0ms
tau
@0
((* (/ (sin (* x (* (PI) tau))) (* x (* (PI) tau))) (/ (sin (* x (PI))) (* x (PI)))) (/ (sin (* x (* (PI) tau))) (* x (* (PI) tau))) (sin (* x (* (PI) tau))) (* x (* (PI) tau)) x (* (PI) tau) (PI) tau (/ (sin (* x (PI))) (* x (PI))) (sin (* x (PI))) (* x (PI)) (* (/ (sin (* (* x (PI)) tau)) (* (* x (PI)) tau)) (/ (sin (* x (PI))) (* x (PI)))) 1 (* (/ (sin (* (* x (PI)) tau)) (* (* x (PI)) tau)) (/ (sin (* x (PI))) (* x (PI)))) (/ (sin (* (* x (PI)) tau)) (* (* x (PI)) tau)) (sin (* (* x (PI)) tau)) (* (* x (PI)) tau) (/ (sin (* x (PI))) (* x (PI))) (+ (* (* -1/6 (* x x)) (* (PI) (PI))) 1) (* -1/6 (* x x)) -1/6 (* x x) (* (PI) (PI)) (* (/ (sin (* (* x (PI)) tau)) (* (* x (PI)) tau)) (/ (sin (* x (PI))) (* x (PI)))) (* (sin (* (* tau x) (PI))) (/ (sin (* (PI) x)) (* (* (* (PI) (PI)) (* x x)) tau))) (sin (* (* tau x) (PI))) (* (* tau x) (PI)) (* tau x) (/ (sin (* (PI) x)) (* (* (* (PI) (PI)) (* x x)) tau)) (sin (* (PI) x)) (* (PI) x) (* (* (* (PI) (PI)) (* x x)) tau) (* (* (PI) (PI)) (* x x)) (/ (* (/ (sin (* (PI) x)) x) (sin (* (* tau x) (PI)))) (* (PI) (* (* tau x) (PI)))) (* (/ (sin (* (PI) x)) x) (sin (* (* tau x) (PI)))) (/ (sin (* (PI) x)) x) (* (PI) (* (* tau x) (PI))))
301.0ms
maxCos
@0
((+ (* (- maxCos 1) ux) 1) (- maxCos 1) maxCos 1 ux (+ (- 1 ux) (* ux maxCos)) (+ (- 1 ux) (* ux maxCos)) (- 1 ux) (+ (* ux maxCos) (- 1 ux)) (* (- (- maxCos (/ -1 ux)) 1) ux) (- (- maxCos (/ -1 ux)) 1) (- maxCos (/ -1 ux)) (/ -1 ux) -1)
141.0ms
u
@inf
((- (log (pow (+ (* (- 1 u) (exp (/ -2 v))) u) v)) -1) (log (pow (+ (* (- 1 u) (exp (/ -2 v))) u) v)) (pow (+ (* (- 1 u) (exp (/ -2 v))) u) v) (+ (* (- 1 u) (exp (/ -2 v))) u) (- 1 u) 1 u (exp (/ -2 v)) (/ -2 v) -2 v -1 (+ (* v (log (+ (* (- 1 u) (exp (/ -2 v))) u))) 1) (+ (* (- 1 u) -2) 1) (+ 1 (* v (log (+ u (* (- 1 u) (exp (/ -2 v))))))) (+ (* (* (- (exp (neg (/ -2 v))) 1) v) u) -1) (* (- (exp (neg (/ -2 v))) 1) v) (+ (- 2 (/ -2 v)) (/ 4/3 (* v v))) (- 2 (/ -2 v)) 2 (/ 4/3 (* v v)) 4/3 (* v v) (+ (* (log (+ (* (- 1 u) (exp (/ -2 v))) u)) v) 1) (log (+ (* (- 1 u) (exp (/ -2 v))) u)) (+ (* (- (exp (/ 2 v)) 1) u) (/ -2 v)) (- (exp (/ 2 v)) 1) (/ 2 v) (+ (* v (log (+ (* (- 1 u) (exp (/ -2 v))) u))) 1) (log (+ (* (- 1 u) (exp (/ -2 v))) u)) (+ (* (- (exp (/ 2 v)) 1) u) (/ -2 v)) (/ (+ (* (* (- (exp (/ 2 v)) 1) v) u) -2) v) (+ (* (* (- (exp (/ 2 v)) 1) v) u) -2) (* (- (exp (/ 2 v)) 1) v))
119.0ms
s
@0
((* (* s 3) (neg (log (+ 1 (/ (* -2 (- u 1/4)) 3/2))))) (* s 3) s 3 (neg (log (+ 1 (/ (* -2 (- u 1/4)) 3/2)))) (log (+ 1 (/ (* -2 (- u 1/4)) 3/2))) (/ (* -2 (- u 1/4)) 3/2) (* -2 (- u 1/4)) -2 (- u 1/4) u 1/4 3/2 (* (* 3 s) (log (/ 1 (- 1 (/ (- u 1/4) 3/4))))) (* (* (log 3/4) s) 3) (* (log 3/4) s) (log 3/4) 3/4 (* 3 (* s (neg (log (- 1 (/ (- u 1/4) 3/4)))))) (* s (neg (log (- 1 (/ (- u 1/4) 3/4))))) (neg (log (- 1 (/ (- u 1/4) 3/4)))) (log (- 1 (/ (- u 1/4) 3/4))) (- 1 (/ (- u 1/4) 3/4)) (+ (* -4/3 u) 4/3) -4/3 4/3 (* s (* 3 (neg (log (- 1 (* 4/3 (- u 1/4))))))) (* 3 (neg (log (- 1 (* 4/3 (- u 1/4)))))) (neg (log (- 1 (* 4/3 (- u 1/4))))) (log (- 1 (* 4/3 (- u 1/4)))) (- 1 (* 4/3 (- u 1/4))) 1 (* 4/3 (- u 1/4)) (* (* s 3) (neg (log (/ (- (* 2 (- u 1/4)) 3/2) -3/2)))) (neg (log (/ (- (* 2 (- u 1/4)) 3/2) -3/2))) (log (/ (- (* 2 (- u 1/4)) 3/2) -3/2)) (/ (- (* 2 (- u 1/4)) 3/2) -3/2) (- (* 2 (- u 1/4)) 3/2) (* 2 (- u 1/4)) 2 -3/2)

eval11.8s (3.4%)

Memory
166.3MiB live, 15 619.0MiB allocated; 7.4s collecting garbage
Compiler

Compiled 1 881 785 to 361 389 computations (80.8% saved)

derivations10.8s (3%)

Memory
248.8MiB live, 9 392.1MiB allocated; 1.5s collecting garbage
Stop Event
33×fuel
3×done
Compiler

Compiled 8 878 to 3 599 computations (59.5% saved)

prune7.2s (2%)

Memory
-277.2MiB live, 10 044.8MiB allocated; 5.2s collecting garbage
Counts
58 842 → 3 095
Compiler

Compiled 243 106 to 165 971 computations (31.7% saved)

preprocess7.1s (2%)

Memory
-213.0MiB live, 9 148.3MiB allocated; 3.4s collecting garbage
Stop Event
36×node-limit
Compiler

Compiled 57 771 to 36 297 computations (37.2% saved)

bsearch1.0s (0.3%)

Memory
8.9MiB live, 1 394.7MiB allocated; 228ms collecting garbage
Algorithm
74×binary-search
30×left-value
Stop Event
72×narrow-enough
2×predicate-same
Samples
423.0ms2 488×0valid
197.0ms1 113×1valid
35.0ms70×1invalid
25.0ms111×2valid
5.0ms93×0invalid
Compiler

Compiled 23 036 to 19 666 computations (14.6% saved)

Precisions
Click to see histograms. Total time spent on operations: 572.0ms
ival-mult!: 116.0ms (20.3% of total)
ival-exp: 115.0ms (20.1% of total)
ival-pow2: 80.0ms (14% of total)
ival-fmax: 51.0ms (8.9% of total)
ival-sub!: 42.0ms (7.3% of total)
adjust: 32.0ms (5.6% of total)
ival-fabs: 26.0ms (4.5% of total)
ival-sqrt: 24.0ms (4.2% of total)
ival-cos: 18.0ms (3.1% of total)
ival-sin: 18.0ms (3.1% of total)
ival-log1p: 17.0ms (3% of total)
ival-add!: 15.0ms (2.6% of total)
ival-fmin: 13.0ms (2.3% of total)
ival-neg: 6.0ms (1% of total)

start55.0ms (0%)

Memory
-49.8MiB live, 55.1MiB allocated; 37ms collecting garbage

end0.0ms (0%)

Memory
0.6MiB live, 0.6MiB allocated; 0ms collecting garbage

Profiling

Loading profile data...