Herbie run

Date:Thursday, April 17th, 2025
Commit:5565a39e on main
Seed:2025107
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:90 083.3 MB

Time bar (total: 1.4min)

sample46.3s (56.1%)

Memory
659.2MiB live, 49 358.6MiB allocated; 12.6s collecting garbage
Samples
19.7s21 431×5exit
7.0s109 842×0valid
6.6s39 046×1valid
4.4s16 232×2valid
635.0ms5 852×0invalid
151.0ms1 115×1exit
144.0ms1 322×0exit
Precisions
Click to see histograms. Total time spent on operations: 31.6s
ival-exp: 6.6s (20.8% of total)
ival-cos: 5.1s (16.2% of total)
ival-pow: 3.6s (11.3% of total)
adjust: 3.5s (11.2% of total)
ival-log: 1.9s (5.9% of total)
ival-mult!: 1.7s (5.2% of total)
ival-tan: 1.6s (5% of total)
ival-fmod: 1.4s (4.4% of total)
ival-sqrt: 1.4s (4.4% of total)
ival-sinh: 1.1s (3.4% of total)
ival-sin: 767.0ms (2.4% of total)
ival-div!: 675.0ms (2.1% of total)
ival-acos: 552.0ms (1.7% of total)
ival-pow2: 505.0ms (1.6% of total)
ival-sub!: 409.0ms (1.3% of total)
ival-add!: 344.0ms (1.1% of total)
ival-neg: 238.0ms (0.8% of total)
ival-hypot: 175.0ms (0.6% of total)
ival-<=: 54.0ms (0.2% of total)
ival-atan: 51.0ms (0.2% of total)
ival-and: 33.0ms (0.1% of total)
ival-or: 15.0ms (0% of total)
ival-assert: 3.0ms (0% of total)
ival->: 2.0ms (0% of total)
ival-<: 2.0ms (0% of total)
Bogosity

rewrite10.1s (12.2%)

Memory
360.7MiB live, 10 326.7MiB allocated; 1.6s collecting garbage
Stop Event
189×iter-limit
53×node-limit
15×unsound
saturated
Counts
8 818 → 18 725

regimes7.3s (8.8%)

Memory
97.5MiB live, 8 899.8MiB allocated; 1.9s collecting garbage
Counts
4 111 → 210
Calls

53 calls:

809.0ms
y
780.0ms
x
684.0ms
a
466.0ms
z
400.0ms
(-.f64 (tan.f64 (+.f64 y z)) (tan.f64 a))
Compiler

Compiled 1 847 to 2 221 computations (-20.2% saved)

derivations3.6s (4.3%)

Memory
-164.6MiB live, 2 448.4MiB allocated; 1.3s collecting garbage
Stop Event
13×fuel
done
Compiler

Compiled 4 185 to 998 computations (76.2% saved)

eval3.4s (4.1%)

Memory
-92.5MiB live, 4 332.2MiB allocated; 1.3s collecting garbage
Compiler

Compiled 733 794 to 93 510 computations (87.3% saved)

explain2.8s (3.3%)

Memory
-126.2MiB live, 2 601.7MiB allocated; 1.4s collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
sqrt.f64#foflow-rescue5510
cos.f64#fsensitivity4880
sqrt.f64#fuflow-rescue3540
-.f64#fcancellation3290
/.f64#fn/o2600
acos.f64(acos.f64 (-.f64 #s(literal 1 binary64) x))sensitivity2560
log.f64(log.f64 (/.f64 (sinh.f64 x) x))sensitivity2500
tan.f64(tan.f64 (+.f64 y z))sensitivity1971
pow.f64(pow.f64 l (exp.f64 w))sensitivity13810
*.f64#fn*o380
*.f64#fn*u250
*.f64#fu*o170
-.f64(-.f64 (*.f64 a a) (*.f64 b b))nan-rescue160
(*.f64 a a)overflow118
(*.f64 b b)overflow16
*.f64(*.f64 (pow.f64 c #s(literal 2 binary64)) (*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x))o*u110
(pow.f64 c #s(literal 2 binary64))overflow51
(*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x)underflow63
(*.f64 x (pow.f64 s #s(literal 2 binary64)))underflow54
(pow.f64 s #s(literal 2 binary64))underflow47
log.f64(log.f64 (/.f64 (sinh.f64 x) x))oflow-rescue30
(sinh.f64 x)overflow3
(/.f64 (sinh.f64 x) x)overflow3
Confusion
Predicted +Predicted -
+2155263
-7161986
Precision
0.7506095437129919
Recall
0.891232423490488
Confusion?
Predicted +Predicted MaybePredicted -
+21550263
-716111975
Precision?
0.7477446217904233
Recall?
0.891232423490488
Freqs
test
numberfreq
02249
12811
258
32
Total Confusion?
Predicted +Predicted MaybePredicted -
+1800
-002
Precision?
1.0
Recall?
1.0
Samples
834.0ms1 006×2valid
468.0ms6 656×0valid
418.0ms2 390×1valid
23.0ms188×1exit
Compiler

Compiled 1 067 to 440 computations (58.8% saved)

Precisions
Click to see histograms. Total time spent on operations: 1.3s
ival-cos: 658.0ms (49% of total)
ival-sqrt: 92.0ms (6.9% of total)
ival-tan: 84.0ms (6.3% of total)
adjust: 80.0ms (6% of total)
ival-sub!: 66.0ms (4.9% of total)
ival-log: 66.0ms (4.9% of total)
ival-mult!: 51.0ms (3.8% of total)
ival-sin: 40.0ms (3% of total)
ival-sinh: 34.0ms (2.5% of total)
ival-acos: 30.0ms (2.2% of total)
ival-exp: 25.0ms (1.9% of total)
ival-div!: 24.0ms (1.8% of total)
ival-add!: 21.0ms (1.6% of total)
ival-pow2: 21.0ms (1.6% of total)
ival-fmod: 20.0ms (1.5% of total)
ival-hypot: 14.0ms (1% of total)
ival-pow: 8.0ms (0.6% of total)
ival-neg: 8.0ms (0.6% of total)
ival-atan: 3.0ms (0.2% of total)

series2.4s (2.9%)

Memory
273.7MiB live, 3 580.9MiB allocated; 392ms collecting garbage
Counts
1 615 → 7 203
Calls

393 calls:

TimeVariablePointExpression
47.0ms
a
@0
((/ (* r (sin b)) (+ (* (cos b) (cos a)) (* (neg (sin b)) (sin a)))) (* r (sin b)) r (sin b) b (+ (* (cos b) (cos a)) (* (neg (sin b)) (sin a))) (cos b) (cos a) a (* (neg (sin b)) (sin a)) (neg (sin b)) (sin a) (/ (* r (sin b)) (cos (+ a b))) (* r (tan b)) (tan b) (/ (* r (sin b)) (cos (/ (+ (pow b 3) (pow a 3)) (+ (* b b) (- (* a a) (* b a)))))) (cos (/ (+ (pow b 3) (pow a 3)) (+ (* b b) (- (* a a) (* b a))))) (/ (+ (pow b 3) (pow a 3)) (+ (* b b) (- (* a a) (* b a)))) (/ (* r (sin b)) (- (* (cos b) (cos a)) (* (sin b) (sin a)))) (- (* (cos b) (cos a)) (* (sin b) (sin a))) (* (cos b) (cos a)) (* (sin b) (sin a)) (/ (* r (sin b)) (cos (/ (+ (pow b 3) (pow a 3)) (+ (* b b) (- (* a a) (* b a)))))) (cos (/ (+ (pow b 3) (pow a 3)) (+ (* b b) (- (* a a) (* b a))))) (/ (+ (pow b 3) (pow a 3)) (+ (* b b) (- (* a a) (* b a)))) (+ (pow b 3) (pow a 3)) (pow b 3) 3 (pow a 3) (+ (* b b) (- (* a a) (* b a))) (* (+ (* (/ b a) -1) 1) (* a a)) (+ (* (/ b a) -1) 1) (/ b a) -1 1 (* a a))
43.0ms
x
@-inf
((/ (- x lo) (- hi lo)) (+ (+ (/ (- (pow (* (/ hi lo) (/ (- x hi) (neg lo))) 2) (pow (/ (neg x) lo) 2)) (- (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo))) 1) (/ hi lo)) (+ (/ (- (pow (* (/ hi lo) (/ (- x hi) (neg lo))) 2) (pow (/ (neg x) lo) 2)) (- (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo))) 1) (/ (- (pow (* (/ hi lo) (/ (- x hi) (neg lo))) 2) (pow (/ (neg x) lo) 2)) (- (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo))) (- (pow (* (/ hi lo) (/ (- x hi) (neg lo))) 2) (pow (/ (neg x) lo) 2)) (pow (* (/ hi lo) (/ (- x hi) (neg lo))) 2) (* (/ hi lo) (/ (- x hi) (neg lo))) (/ hi lo) hi lo (/ (- x hi) (neg lo)) (- x hi) x (neg lo) 2 (pow (/ (neg x) lo) 2) (/ (neg x) lo) (neg x) (- (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (- x hi) (neg lo)) (* hi (+ (* -1 (/ x (* hi lo))) (pow lo -1))) (+ (* -1 (/ x (* hi lo))) (pow lo -1)) -1 (/ x (* hi lo)) (* hi lo) (pow lo -1) 1 (/ (- x lo) (- hi lo)) (- x lo) (- hi lo) (/ (- x lo) (- hi lo)) (+ (+ (+ (* (neg (/ (- x hi) lo)) (/ hi lo)) (/ (neg x) lo)) 1) (/ hi lo)) (+ (+ (* (neg (/ (- x hi) lo)) (/ hi lo)) (/ (neg x) lo)) 1) (+ (* (neg (/ (- x hi) lo)) (/ hi lo)) (/ (neg x) lo)) (neg (/ (- x hi) lo)) (/ (- x hi) lo) (* (- (/ (/ x hi) lo) (pow lo -1)) hi) (- (/ (/ x hi) lo) (pow lo -1)) (/ -1 lo) (/ (- x lo) (- hi lo)) (/ (- (* (* (/ (- (+ (* hi (/ (- x hi) lo)) x) hi) lo) -1) (* (/ (- (+ (* hi (/ (- x hi) lo)) x) hi) lo) -1)) 1) (- (* (/ (- (+ (* hi (/ (- x hi) lo)) x) hi) lo) -1) 1)) (- (* (* (/ (- (+ (* hi (/ (- x hi) lo)) x) hi) lo) -1) (* (/ (- (+ (* hi (/ (- x hi) lo)) x) hi) lo) -1)) 1) (* (* (/ (- (+ (* hi (/ (- x hi) lo)) x) hi) lo) -1) (* (/ (- (+ (* hi (/ (- x hi) lo)) x) hi) lo) -1)) (* (/ (- (+ (* hi (/ (- x hi) lo)) x) hi) lo) -1) (/ (- (+ (* hi (/ (- x hi) lo)) x) hi) lo) (- (+ (* hi (/ (- x hi) lo)) x) hi) (+ (* hi (/ (- x hi) lo)) x) (/ (- x hi) lo) (- x hi) (* (neg x) (- (/ hi x) 1)) (- (/ hi x) 1) (/ hi x) (- (* (/ (- (+ (* hi (/ (- x hi) lo)) x) hi) lo) -1) 1) (/ (- x lo) (- hi lo)) (/ (- (pow (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (+ (* (/ x lo) -1) 1)) 2) (pow (/ hi lo) 2)) (- (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (+ (* (/ x lo) -1) 1)) (/ hi lo))) (- (pow (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (+ (* (/ x lo) -1) 1)) 2) (pow (/ hi lo) 2)) (pow (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (+ (* (/ x lo) -1) 1)) 2) (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (+ (* (/ x lo) -1) 1)) (+ (* (/ x lo) -1) 1) (/ x lo) (pow (/ hi lo) 2) (- (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (+ (* (/ x lo) -1) 1)) (/ hi lo)))
42.0ms
x
@-inf
((- (sqrt (+ 1 x)) (sqrt (- 1 x))) (+ (* (* (* x x) 1/8) x) x) (* (* x x) 1/8) (* x x) x 1/8 (/ (- (pow (sqrt (+ x 1)) 3) (pow (sqrt (- 1 x)) 3)) (+ (+ (+ x 1) (- 1 x)) (sqrt (* (+ x 1) (- 1 x))))) (+ (* (* (* (+ (* (+ (* (* x x) 33/1024) 7/128) (* x x)) 1/8) x) x) x) x) (* (* (+ (* (+ (* (* x x) 33/1024) 7/128) (* x x)) 1/8) x) x) (* (+ (* (+ (* (* x x) 33/1024) 7/128) (* x x)) 1/8) x) (+ (* (+ (* (* x x) 33/1024) 7/128) (* x x)) 1/8) (+ (* (* x x) 33/1024) 7/128) 33/1024 7/128 (/ (- (pow (sqrt (+ x 1)) 3) (* (* (sqrt (- 1 x)) (sqrt (- 1 x))) (sqrt (- 1 x)))) (+ (+ (+ x 1) (- 1 x)) (sqrt (* (+ x 1) (- 1 x))))) (- (pow (sqrt (+ x 1)) 3) (* (* (sqrt (- 1 x)) (sqrt (- 1 x))) (sqrt (- 1 x)))) (pow (sqrt (+ x 1)) 3) (sqrt (+ x 1)) (+ x 1) 1 3 (* (* (sqrt (- 1 x)) (sqrt (- 1 x))) (sqrt (- 1 x))) (* (sqrt (- 1 x)) (sqrt (- 1 x))) (sqrt (- 1 x)) (- 1 x) (+ (+ (+ x 1) (- 1 x)) (sqrt (* (+ x 1) (- 1 x)))) (+ (+ x 1) (- 1 x)) (sqrt (* (+ x 1) (- 1 x))) (* (+ x 1) (- 1 x)))
35.0ms
l
@0
((* (/ 1 (exp w)) (pow l (exp w))) (/ 1 (exp w)) 1 (exp w) w (pow l (exp w)) l (* (exp (neg w)) (pow l (exp w))) (* (exp (neg w)) (pow l (exp w))) (exp (neg w)) (- 1 w) (* (exp (neg w)) (pow l (exp w))) (pow (exp -1) (+ (* (neg (log l)) (exp w)) w)) (exp -1) -1 (+ (* (neg (log l)) (exp w)) w) (neg (log l)) (log l) (* (exp (neg w)) (pow (exp (log l)) (exp w))) (exp (neg w)) (neg w) (pow (exp (log l)) (exp w)) (exp (log l)))
32.0ms
s
@0
((/ (/ (cos (* -2 x)) (* (* s x) c)) (* (* s x) c)) (/ (cos (* -2 x)) (* (* s x) c)) (cos (* -2 x)) (* -2 x) -2 x (* (* s x) c) (* s x) s c (/ (cos (* 2 x)) (* (* (* c c) (* x x)) (* s s))) (cos (* 2 x)) 1 (* (* (* c c) (* x x)) (* s s)) (* (* c c) (* x x)) (* c c) (* x x) (* s s) (/ (/ (/ (cos (* -2 x)) (* c c)) (* s s)) (* x x)) (/ (/ (cos (* -2 x)) (* c c)) (* s s)) (pow (* c s) -2) (* c s) (/ (cos (* 2 x)) (* (* (* (* c x) c) x) (* s s))) (cos (* 2 x)) (* 2 x) 2 (* (* (* (* c x) c) x) (* s s)) (* (* (* c x) c) x) (* (* c x) c) (* c x) (/ (sin (+ (* x 2) (/ (PI) 2))) (* (* (* c c) (* x x)) (* s s))) (sin (+ (* x 2) (/ (PI) 2))) (+ (* x 2) (/ (PI) 2)) (/ (PI) 2) (PI))

analyze2.1s (2.6%)

Memory
30.1MiB live, 2 992.9MiB allocated; 581ms collecting garbage
Algorithm
20×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%73.7%26.3%0%0%0%0
28.8%21.3%52.5%26.3%0%0%0%1
44.1%32.5%41.2%26.3%0%0%0%2
52.6%38.7%35%26.3%0%0%0%3
61.9%45.6%28.1%26.3%0%0%0%4
65.2%47.5%25.3%26.3%0%0.9%0%5
66.8%48.4%24%26.3%0%1.2%0%6
71.1%51.1%20.8%26.3%0%1.9%0%7
72.1%51.6%20%26.3%0%2.1%0%8
74.4%53%18.2%26.3%0%2.5%0%9
75.8%53.9%17.2%26.3%0%2.6%0%10
76.6%54.3%16.6%26.3%0%2.8%0%11
77.3%54.8%16.1%26.3%0%2.9%0%12
Compiler

Compiled 279 to 216 computations (22.6% saved)

preprocess2.0s (2.5%)

Memory
-93.8MiB live, 2 168.3MiB allocated; 292ms collecting garbage
Stop Event
15×node-limit
saturated
Compiler

Compiled 19 688 to 8 938 computations (54.6% saved)

prune1.9s (2.3%)

Memory
-95.9MiB live, 2 749.1MiB allocated; 429ms collecting garbage
Counts
20 890 → 1 616
Compiler

Compiled 86 793 to 45 977 computations (47% saved)

bsearch696.0ms (0.8%)

Memory
16.9MiB live, 623.3MiB allocated; 95ms collecting garbage
Algorithm
54×binary-search
14×left-value
Stop Event
54×narrow-enough
Samples
221.0ms1 076×1valid
213.0ms1 532×0valid
8.0ms72×0exit
Compiler

Compiled 13 702 to 11 422 computations (16.6% saved)

Precisions
Click to see histograms. Total time spent on operations: 319.0ms
ival-tan: 93.0ms (29.1% of total)
ival-sin: 89.0ms (27.9% of total)
ival-cos: 30.0ms (9.4% of total)
adjust: 28.0ms (8.8% of total)
ival-exp: 17.0ms (5.3% of total)
ival-pow: 17.0ms (5.3% of total)
ival-mult!: 12.0ms (3.8% of total)
ival-add!: 10.0ms (3.1% of total)
ival-acos: 6.0ms (1.9% of total)
ival-div!: 5.0ms (1.6% of total)
ival-neg: 5.0ms (1.6% of total)
ival-pow2: 4.0ms (1.3% of total)
ival-sub!: 4.0ms (1.3% of total)

start1.0ms (0%)

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

end0.0ms (0%)

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

Profiling

Loading profile data...