Herbie run

Date:Wednesday, March 5th, 2025
Commit:141e80a8 on main
Seed:2025064
Parameters:256 points for 4 iterations
Flags:
reduce:regimesreduce:binary-searchreduce:branch-expressionsreduce:simplifysetup:simplifysetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:simplifygenerate:proofs
default
Memory:85 954.3 MB

Time bar (total: 1.4min)

sample47.5s (55.6%)

Memory
840.1MiB live, 48 285.6MiB allocated; 13.4s collecting garbage
Samples
15.6s16 378×5exit
9.0s39 973×1valid
7.6s108 724×0valid
6.2s16 423×2valid
466.0ms3 973×0invalid
107.0ms1 370×0exit
Precisions
Click to see histograms. Total time spent on operations: 30.9s
ival-pow: 4.6s (14.8% of total)
ival-exp: 4.2s (13.6% of total)
adjust: 3.9s (12.7% of total)
ival-log: 2.8s (8.9% of total)
ival-cos: 2.3s (7.4% of total)
ival-mult: 2.1s (6.9% of total)
ival-sinh: 1.8s (5.9% of total)
ival-tan: 1.5s (4.8% of total)
ival-div: 1.1s (3.5% of total)
ival-sqrt: 1.1s (3.5% of total)
ival-fmod: 918.0ms (3% of total)
ival-sin: 849.0ms (2.7% of total)
ival-sub: 798.0ms (2.6% of total)
ival-add: 771.0ms (2.5% of total)
ival-acos: 601.0ms (1.9% of total)
ival-pow2: 511.0ms (1.7% of total)
const: 362.0ms (1.2% of total)
ival-neg: 351.0ms (1.1% of total)
ival-hypot: 148.0ms (0.5% of total)
ival-assert: 76.0ms (0.2% of total)
ival-<=: 60.0ms (0.2% of total)
ival-atan: 47.0ms (0.2% of total)
exact: 41.0ms (0.1% of total)
ival-and: 39.0ms (0.1% of total)
ival-or: 19.0ms (0.1% of total)
ival->: 4.0ms (0% of total)
ival-==: 2.0ms (0% of total)
ival-<: 2.0ms (0% of total)
Bogosity

rewrite10.2s (12%)

Memory
257.7MiB live, 9 291.8MiB allocated; 2.2s collecting garbage
Stop Event
191×iter limit
49×node limit
18×unsound
4×saturated
Counts
7 828 → 16 706

regimes5.0s (5.8%)

Memory
29.1MiB live, 5 257.8MiB allocated; 1.5s collecting garbage
Counts
3 106 → 177
Calls

53 calls:

673.0ms
x
505.0ms
(+.f64 x (-.f64 (tan.f64 (+.f64 y z)) (tan.f64 a)))
463.0ms
a
252.0ms
b
242.0ms
(-.f64 (tan.f64 (+.f64 y z)) (tan.f64 a))
Compiler

Compiled 1 567 to 1 862 computations (-18.8% saved)

preprocess4.1s (4.8%)

Memory
16.6MiB live, 3 941.2MiB allocated; 804ms collecting garbage
Stop Event
38×iter limit
29×node limit
13×saturated
Compiler

Compiled 8 027 to 2 808 computations (65% saved)

eval3.9s (4.5%)

Memory
-30.4MiB live, 3 846.0MiB allocated; 1.6s collecting garbage
Compiler

Compiled 717 250 to 85 661 computations (88.1% saved)

derivations3.0s (3.5%)

Memory
-7.2MiB live, 1 935.6MiB allocated; 402ms collecting garbage
Stop Event
13×fuel
7×done
Compiler

Compiled 3 328 to 937 computations (71.8% saved)

explain2.9s (3.4%)

Memory
6.8MiB live, 3 034.4MiB allocated; 417ms collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
sqrt.f64#foflow-rescue5750
cos.f64#fsensitivity5200
-.f64#fcancellation3460
sqrt.f64#fuflow-rescue2990
/.f64#fn/o2590
acos.f64(acos.f64 (-.f64 #s(literal 1 binary64) x))sensitivity2560
log.f64(log.f64 (/.f64 (sinh.f64 x) x))sensitivity2540
tan.f64(tan.f64 (+.f64 y z))sensitivity1880
pow.f64(pow.f64 l (exp.f64 w))sensitivity13917
*.f64#fn*u430
*.f64#fn*o380
*.f64(*.f64 (pow.f64 c #s(literal 2 binary64)) (*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x))o*u160
↳(pow.f64 c #s(literal 2 binary64))overflow68
↳(*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x)underflow60
↳(*.f64 x (pow.f64 s #s(literal 2 binary64)))underflow52
↳(pow.f64 s #s(literal 2 binary64))underflow63
*.f64(*.f64 (pow.f64 c #s(literal 2 binary64)) (*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x))u*o150
↳(pow.f64 c #s(literal 2 binary64))underflow57
↳(*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x)overflow65
↳(*.f64 x (pow.f64 s #s(literal 2 binary64)))overflow59
↳(pow.f64 s #s(literal 2 binary64))overflow64
-.f64(-.f64 (*.f64 a a) (*.f64 b b))nan-rescue140
↳(*.f64 a a)overflow104
↳(*.f64 b b)overflow14
log.f64(log.f64 (/.f64 (sinh.f64 x) x))oflow-rescue10
↳(sinh.f64 x)overflow1
↳(/.f64 (sinh.f64 x) x)overflow1
Confusion
Predicted +Predicted -
+2149267
-7381966
Precision
0.7443713197090406
Recall
0.8894867549668874
Confusion?
Predicted +Predicted MaybePredicted -
+21490267
-738171949
Precision?
0.7400137741046832
Recall?
0.8894867549668874
Freqs
test
numberfreq
02233
12815
268
34
Total Confusion?
Predicted +Predicted MaybePredicted -
+1701
-002
Precision?
1.0
Recall?
0.9444444444444444
Samples
525.0ms2 536×1valid
524.0ms90×5exit
410.0ms6 602×0valid
331.0ms1 012×2valid
Compiler

Compiled 1 067 to 440 computations (58.8% saved)

Precisions
Click to see histograms. Total time spent on operations: 1.4s
ival-cos: 534.0ms (38.3% of total)
ival-tan: 131.0ms (9.4% of total)
adjust: 115.0ms (8.2% of total)
ival-mult: 78.0ms (5.6% of total)
ival-sinh: 75.0ms (5.4% of total)
ival-log: 64.0ms (4.6% of total)
ival-sqrt: 58.0ms (4.2% of total)
ival-exp: 57.0ms (4.1% of total)
ival-div: 38.0ms (2.7% of total)
ival-sub: 37.0ms (2.7% of total)
ival-add: 37.0ms (2.7% of total)
ival-fmod: 37.0ms (2.7% of total)
ival-sin: 36.0ms (2.6% of total)
ival-acos: 33.0ms (2.4% of total)
ival-pow2: 22.0ms (1.6% of total)
ival-true: 9.0ms (0.6% of total)
ival-hypot: 9.0ms (0.6% of total)
ival-pow: 8.0ms (0.6% of total)
ival-neg: 6.0ms (0.4% of total)
ival-atan: 4.0ms (0.3% of total)
ival-assert: 4.0ms (0.3% of total)
exact: 2.0ms (0.1% of total)

series2.7s (3.2%)

Memory
-51.7MiB live, 3 249.9MiB allocated; 673ms collecting garbage
Counts
1 455 → 6 373
Calls

387 calls:

TimeVariablePointExpression
128.0ms
a
@inf
((* r (/ (sin b) (+ (* (cos b) (cos a)) (* (neg (sin b)) (sin a))))) r (/ (sin b) (+ (* (cos b) (cos a)) (* (neg (sin b)) (sin a)))) (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)))) (/ (sin b) (cos (+ a b))) (tan b) (* r (/ (sin b) (sin (+ (neg (+ a b)) (/ (PI) 2))))) (/ (sin b) (sin (+ (neg (+ a b)) (/ (PI) 2)))) (sin b) (sin (+ (neg (+ a b)) (/ (PI) 2))) (+ (neg (+ a b)) (/ (PI) 2)) (neg (+ a b)) (+ a b) (/ (PI) 2) (PI) 2 (* r (/ (sin b) (sin (+ (+ a b) (/ (PI) 2))))) (/ (sin b) (sin (+ (+ a b) (/ (PI) 2)))) (sin (+ (+ a b) (/ (PI) 2))) (+ (+ a b) (/ (PI) 2)) (+ a b) (* r (/ (sin b) (- (* (cos b) (cos a)) (* (sin b) (sin a))))) (/ (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)))
59.0ms
x
@-inf
((/ (+ (* (asin (- 1 x)) (asin (+ -1 x))) (pow (/ (PI) 2) 2)) (+ (/ (PI) 2) (asin (- 1 x)))) (+ (* (asin (- 1 x)) (asin (+ -1 x))) (pow (/ (PI) 2) 2)) (asin (- 1 x)) (- 1 x) 1 x (asin (+ -1 x)) (+ -1 x) -1 (pow (/ (PI) 2) 2) (/ (PI) 2) (PI) 2 (+ (/ (PI) 2) (asin (- 1 x))) (asin (- 1 x)) (- 1 x) (* (neg x) (- 1 (pow x -1))) (neg x) (- 1 (pow x -1)) (pow x -1) (acos (- 1 x)) (- 1 x) (* (- (/ 1 x) 1) x) (- (/ 1 x) 1) (/ 1 x) (acos (- 1 x)) (- 1 x) (* (- (exp (neg (log x))) 1) x) (- (exp (neg (log x))) 1) (neg (log x)) (log x) (/ (+ (* (asin (- 1 x)) (asin (+ -1 x))) (pow (/ (PI) 2) 2)) (+ (/ (PI) 2) (asin (- 1 x)))) (/ (+ (* (asin (- x 1)) (asin (- 1 x))) (* 1/4 (* (PI) (PI)))) (+ (* (PI) 1/2) (asin (- 1 x)))) (+ (* (asin (- x 1)) (asin (- 1 x))) (* 1/4 (* (PI) (PI)))) (asin (- x 1)) (- x 1) (* 1/4 (* (PI) (PI))) 1/4 (* (PI) (PI)) (+ (* (PI) 1/2) (asin (- 1 x))) 1/2 (- (/ (PI) 2) (* (pow (asin (- 1 x)) 1/2) (pow (asin (- 1 x)) 1/2))) (* (pow (asin (- 1 x)) 1/2) (pow (asin (- 1 x)) 1/2)) (pow (asin (- 1 x)) 1/2) (pow (asin (- 1 x)) 1/2))
45.0ms
lo
@inf
((/ (- x lo) (- hi lo)) (+ (/ (- (pow (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 2) 1) (- (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 1)) (/ hi lo)) (/ (- (pow (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 2) 1) (- (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 1)) (- (pow (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 2) 1) (pow (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 2) (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) (/ hi lo) hi lo (/ (- x hi) (neg lo)) (- x hi) x (neg lo) (/ (neg x) lo) (neg x) 2 1 (- (+ (* (/ hi lo) (/ (- x hi) (neg lo))) (/ (neg x) lo)) 1) (/ (- 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) (/ (- 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 lo) (- hi lo)) (+ (* (- (/ (+ (* (- (pow lo -1) (/ x (* lo lo))) hi) 1) lo) (/ x (* lo lo))) hi) (neg (/ (- x lo) lo))) (- (/ (+ (* (- (pow lo -1) (/ x (* lo lo))) hi) 1) lo) (/ x (* lo lo))) (/ (+ (* (- (pow lo -1) (/ x (* lo lo))) hi) 1) lo) (+ (* (- (pow lo -1) (/ x (* lo lo))) hi) 1) (- (pow lo -1) (/ x (* lo lo))) (pow lo -1) -1 (/ x (* lo lo)) (* lo lo) (neg (/ (- x lo) lo)) (/ (- x lo) lo) (- x lo) (/ (- x lo) (- hi lo)) (+ (* (- (/ (+ (* (- (pow lo -1) (/ x (* lo lo))) hi) 1) lo) (/ x (* lo lo))) hi) (neg (/ (- x lo) lo))) (- (/ (+ (* (- (pow lo -1) (/ x (* lo lo))) hi) 1) lo) (/ x (* lo lo))) (/ (+ (* (- (pow lo -1) (/ x (* lo lo))) hi) 1) lo) (+ (* (- (pow lo -1) (/ x (* lo lo))) hi) 1) (- (pow lo -1) (/ x (* lo lo))) (* (- (pow (* lo x) -1) (pow lo -2)) x) (- (pow (* lo x) -1) (pow lo -2)) (pow (* lo x) -1) (* lo x) (pow lo -2) -2 (neg (/ (- x lo) lo)) (/ (- x lo) lo) (- x lo))
44.0ms
x
@0
((* (fmod (exp x) (sqrt (cos x))) (exp (neg x))) (fmod (exp x) (sqrt (cos x))) (exp x) x (sqrt (cos x)) (+ (* (* x x) -1/4) 1) (* (* (- (exp (* (log (* x x)) -1)) 1/4) x) x) (* (- (exp (* (log (* x x)) -1)) 1/4) x) (- (exp (* (log (* x x)) -1)) 1/4) (exp (* (log (* x x)) -1)) (* (log (* x x)) -1) (log (* x x)) (* x x) -1 1/4 (exp (neg x)) (neg x) (* (fmod (exp x) (sqrt (cos x))) (exp (neg x))) (fmod (exp x) (sqrt (cos x))) (exp x) (- x -1) (sqrt (cos x)) 1 (exp (neg x)) (* (fmod (exp x) (sqrt (cos x))) (exp (neg x))) (fmod (exp x) (sqrt (cos x))) (exp x) (+ (* (+ (* (+ (* 1/6 x) 1/2) x) 1) x) 1) (+ (* (+ (* 1/6 x) 1/2) x) 1) (+ (* 1/6 x) 1/2) 1/6 1/2 (sqrt (cos x)) (+ (* (* x x) -1/4) 1) -1/4 (exp (neg x)) (+ (* (+ (* 1/2 x) -1) x) 1) (+ (* 1/2 x) -1) (* (fmod (exp x) (sqrt (cos x))) (exp (neg x))) (fmod (exp x) (sqrt (cos x))) (sqrt (cos x)) (+ (* (* x x) -1/4) 1) (* (* (- (pow x -2) 1/4) x) x) (* (- (pow x -2) 1/4) x) (- (pow x -2) 1/4) (* (fmod (exp x) (sqrt (cos x))) (exp (neg x))) (fmod (exp x) (sqrt (cos x))) (sqrt (cos x)) (+ (* (* x x) -1/4) 1) (* (- (pow x -2) 1/4) (* x x)) (- (pow x -2) 1/4) (pow x -2) -2)
44.0ms
b
@inf
((/ (* r (sin b)) (- (* (cos b) (cos a)) (* (sin b) (sin a)))) (* r (sin b)) r (sin b) b (- (* (cos b) (cos a)) (* (sin b) (sin a))) (* (cos b) (cos a)) (cos b) (cos a) a (* (sin b) (sin a)) (sin a) (/ (* r (sin b)) (cos (+ a b))) (* r (tan b)) (tan b) (/ (* r (sin b)) (cos (+ a b))) (cos (+ a b)) (+ a b) (/ (* r (sin b)) (cos (/ (- (* b b) (* a a)) (- b a)))) (cos (/ (- (* b b) (* a a)) (- b a))) (/ (- (* b b) (* a a)) (- b a)) (- (* b b) (* a a)) (* b b) (* a a) (- b a) (/ (* r (exp (* (log (sin b)) 1))) (cos (+ a b))) (* r (exp (* (log (sin b)) 1))) (exp (* (log (sin b)) 1)) (* (log (sin b)) 1) (log (sin b)) 1 (cos (+ a b)) (+ a b))

analyze2.6s (3%)

Memory
14.4MiB live, 2 627.6MiB allocated; 742ms 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)

prune1.9s (2.2%)

Memory
-24.3MiB live, 2 819.7MiB allocated; 360ms collecting garbage
Counts
21 472 → 1 390
Compiler

Compiled 75 060 to 39 251 computations (47.7% saved)

simplify874.0ms (1%)

Memory
-119.3MiB live, 677.1MiB allocated; 94ms collecting garbage
Stop Event
16×node limit
4×saturated

bsearch867.0ms (1%)

Memory
-7.1MiB live, 986.1MiB allocated; 136ms collecting garbage
Algorithm
45×binary-search
11×left-value
Stop Event
44×narrow-enough
1×predicate-same
Samples
414.0ms1 478×1valid
131.0ms1 658×0valid
88.0ms192×2valid
2.0ms26×0exit
Compiler

Compiled 14 572 to 12 275 computations (15.8% saved)

Precisions
Click to see histograms. Total time spent on operations: 508.0ms
ival-sin: 91.0ms (17.9% of total)
ival-tan: 83.0ms (16.4% of total)
ival-exp: 71.0ms (14% of total)
ival-cos: 62.0ms (12.2% of total)
adjust: 61.0ms (12% of total)
ival-mult: 35.0ms (6.9% of total)
ival-fmod: 31.0ms (6.1% of total)
ival-add: 23.0ms (4.5% of total)
ival-div: 13.0ms (2.6% of total)
ival-pow: 10.0ms (2% of total)
ival-sqrt: 9.0ms (1.8% of total)
ival-sub: 6.0ms (1.2% of total)
ival-pow2: 5.0ms (1% of total)
ival-neg: 4.0ms (0.8% of total)
ival-true: 3.0ms (0.6% of total)
ival-assert: 1.0ms (0.2% of total)
exact: 0.0ms (0% of total)

start1.0ms (0%)

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

end0.0ms (0%)

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

Profiling

Loading profile data...