Herbie run

Date:Saturday, March 1st, 2025
Commit:141e80a8 on main
Seed:2025060
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:29 503.3 MB

Time bar (total: 28.5s)

sample10.7s (37.6%)

Memory
360.5MiB live, 10 759.5MiB allocated; 5.1s collecting garbage
Samples
6.3s70 217×0valid
1.1s4 083×2valid
183.0ms1 925×0invalid
0.0ms1valid
Precisions
Click to see histograms. Total time spent on operations: 4.8s
ival-div: 1.3s (27.4% of total)
ival-mult: 1.2s (25.3% of total)
ival-sub: 668.0ms (14% of total)
ival-sqrt: 451.0ms (9.4% of total)
ival-neg: 301.0ms (6.3% of total)
ival-add: 208.0ms (4.4% of total)
adjust: 195.0ms (4.1% of total)
ival-log: 140.0ms (2.9% of total)
ival-fabs: 114.0ms (2.4% of total)
ival-exp: 83.0ms (1.7% of total)
exact: 62.0ms (1.3% of total)
ival-assert: 26.0ms (0.5% of total)
ival-if: 7.0ms (0.1% of total)
ival->=: 3.0ms (0.1% of total)
Bogosity

rewrite5.9s (20.6%)

Memory
30.7MiB live, 5 841.1MiB allocated; 1.2s collecting garbage
Stop Event
73×iter limit
28×node limit
unsound
saturated
Counts
4 340 → 6 820

preprocess2.3s (8.2%)

Memory
89.8MiB live, 2 044.0MiB allocated; 319ms collecting garbage
Stop Event
18×iter limit
16×node limit
saturated
Compiler

Compiled 8 937 to 1 538 computations (82.8% saved)

eval1.8s (6.4%)

Memory
5.6MiB live, 2 367.8MiB allocated; 492ms collecting garbage
Compiler

Compiled 588 646 to 39 882 computations (93.2% saved)

explain1.5s (5.3%)

Memory
-17.9MiB live, 1 814.4MiB allocated; 520ms collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
sqrt.f64#foflow-rescue2640
+.f64#fcancellation1290
-.f64#fcancellation1180
sqrt.f64#fuflow-rescue600
/.f64#fu/n310
/.f64#fn/u220
-.f64#fnan-rescue170
*.f64(*.f64 (/.f64 x y) z)n*o90
*.f64(*.f64 (/.f64 x y) z)n*u60
/.f64(/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 #s(literal 4 binary64) a) c)))) (*.f64 #s(literal 2 binary64) a))n/o10
(*.f64 #s(literal 2 binary64) a)overflow1
exp.f64(exp.f64 (neg.f64 (-.f64 #s(literal 1 binary64) (*.f64 x x))))sensitivity10
Confusion
Predicted +Predicted -
+28912
-2321771
Precision
0.5547024952015355
Recall
0.9601328903654485
Confusion?
Predicted +Predicted MaybePredicted -
+289012
-23201771
Precision?
0.5547024952015355
Recall?
0.9601328903654485
Freqs
test
numberfreq
01783
1389
2127
35
Total Confusion?
Predicted +Predicted MaybePredicted -
+400
-104
Precision?
0.8
Recall?
1.0
Samples
265.0ms3 684×0valid
226.0ms548×2valid
103.0ms322×1valid
31.0ms54×3valid
Compiler

Compiled 1 107 to 300 computations (72.9% saved)

Precisions
Click to see histograms. Total time spent on operations: 428.0ms
ival-sub: 77.0ms (18% of total)
ival-mult: 72.0ms (16.8% of total)
adjust: 65.0ms (15.2% of total)
ival-div: 58.0ms (13.5% of total)
ival-sqrt: 55.0ms (12.8% of total)
ival-add: 52.0ms (12.1% of total)
ival-neg: 11.0ms (2.6% of total)
ival-if: 9.0ms (2.1% of total)
ival-log: 6.0ms (1.4% of total)
ival-fabs: 5.0ms (1.2% of total)
ival-exp: 4.0ms (0.9% of total)
ival-true: 4.0ms (0.9% of total)
exact: 4.0ms (0.9% of total)
ival->=: 3.0ms (0.7% of total)
ival-assert: 2.0ms (0.5% of total)

series1.5s (5.1%)

Memory
-57.5MiB live, 1 727.8MiB allocated; 335ms collecting garbage
Counts
739 → 3 601
Calls

180 calls:

TimeVariablePointExpression
96.0ms
x
@0
((exp (neg (- 1 (* x x)))) (neg (- 1 (* x x))) -1 (exp (neg (- 1 (* x x)))) (neg (- 1 (* x x))) (* x x) x (exp (neg (- 1 (* x x)))) (neg (- 1 (* x x))) (+ (* x x) -1) (/ (- (pow (cosh (+ (* x x) -1)) 3) (pow (sinh (neg (+ (* x x) -1))) 3)) (+ (* (cosh (+ (* x x) -1)) (cosh (+ (* x x) -1))) (+ (* (sinh (neg (+ (* x x) -1))) (sinh (neg (+ (* x x) -1)))) (* (cosh (+ (* x x) -1)) (sinh (neg (+ (* x x) -1))))))) (- (pow (cosh (+ (* x x) -1)) 3) (pow (sinh (neg (+ (* x x) -1))) 3)) (pow (cosh (+ (* x x) -1)) 3) (cosh (+ (* x x) -1)) 3 (pow (sinh (neg (+ (* x x) -1))) 3) (sinh (neg (+ (* x x) -1))) (neg (+ (* x x) -1)) (+ (* (cosh (+ (* x x) -1)) (cosh (+ (* x x) -1))) (+ (* (sinh (neg (+ (* x x) -1))) (sinh (neg (+ (* x x) -1)))) (* (cosh (+ (* x x) -1)) (sinh (neg (+ (* x x) -1)))))) (+ (* (sinh (neg (+ (* x x) -1))) (sinh (neg (+ (* x x) -1)))) (* (cosh (+ (* x x) -1)) (sinh (neg (+ (* x x) -1))))) (* (cosh (+ (* x x) -1)) (sinh (neg (+ (* x x) -1)))))
69.0ms
z
@0
((fabs (- (/ (+ x 4) y) (* (/ x y) z))) (- (/ (+ x 4) y) (* (/ x y) z)) (/ (+ x 4) y) (+ x 4) x 4 y (* (/ x y) z) (/ x y) z)
56.0ms
x
@0
((/ (- (pow (+ (* (cosh (* x x)) (cosh -1)) (* (sinh (* x x)) (sinh -1))) 3) (pow (sinh (neg (+ (* x x) -1))) 3)) (+ (* (cosh (+ (* x x) -1)) (cosh (+ (* x x) -1))) (+ (* (sinh (neg (+ (* x x) -1))) (sinh (neg (+ (* x x) -1)))) (* (cosh (+ (* x x) -1)) (sinh (neg (+ (* x x) -1))))))) (- (pow (+ (* (cosh (* x x)) (cosh -1)) (* (sinh (* x x)) (sinh -1))) 3) (pow (sinh (neg (+ (* x x) -1))) 3)) (pow (+ (* (cosh (* x x)) (cosh -1)) (* (sinh (* x x)) (sinh -1))) 3) (+ (* (cosh (* x x)) (cosh -1)) (* (sinh (* x x)) (sinh -1))) (cosh (* x x)) (* x x) x (cosh -1) -1 (* (sinh (* x x)) (sinh -1)) (sinh (* x x)) (sinh -1) 3 (pow (sinh (neg (+ (* x x) -1))) 3) (sinh (neg (+ (* x x) -1))) (neg (+ (* x x) -1)) (+ (* x x) -1) (+ (* (cosh (+ (* x x) -1)) (cosh (+ (* x x) -1))) (+ (* (sinh (neg (+ (* x x) -1))) (sinh (neg (+ (* x x) -1)))) (* (cosh (+ (* x x) -1)) (sinh (neg (+ (* x x) -1)))))) (cosh (+ (* x x) -1)) (+ (* (sinh (neg (+ (* x x) -1))) (sinh (neg (+ (* x x) -1)))) (* (cosh (+ (* x x) -1)) (sinh (neg (+ (* x x) -1))))) (* (cosh (+ (* x x) -1)) (sinh (neg (+ (* x x) -1)))))
54.0ms
x
@-inf
((neg (log (- (/ 1 x) 1))) (log x) x (neg (log (- (/ 1 x) 1))) (+ (log x) x) (neg (log (- (/ 1 x) 1))) (+ (* (+ (* 1/2 x) 1) x) (log x)) (+ (* 1/2 x) 1) 1/2 1 (neg (log (+ (* (pow x -1/2) (pow x -1/2)) -1))) (log (+ (* (pow x -1/2) (pow x -1/2)) -1)) (+ (* (pow x -1/2) (pow x -1/2)) -1) (pow x -1/2) -1/2 -1)
43.0ms
b
@0
((if (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (>= b 0) b 0 (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (neg b) (sqrt (- (* b b) (* (* 4 a) c))) (- (* b b) (* (* 4 a) c)) (* (+ (* (* a (/ c (* b b))) -4) 1) (* b b)) (+ (* (* a (/ c (* b b))) -4) 1) (* a (/ c (* b b))) a (/ c (* b b)) c (* b b) -4 1 (* 2 a) 2 (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (sqrt (- (* b b) (* (* 4 a) c))) (- (* b b) (* (* 4 a) c)) (* (* 4 a) c) (* 4 a) 4 (if (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (* (sqrt (* (/ c a) -4)) -1/2) (sqrt (* (/ c a) -4)) (* (/ c a) -4) (/ c a) -1/2 (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (neg (sqrt (* (/ c a) -1))) (sqrt (* (/ c a) -1)) (* (/ c a) -1) -1 (if (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (neg (sqrt (* (* a c) -4))) (sqrt (* (* a c) -4)) (* (* a c) -4) (* a c) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (neg (/ (+ (* 1/2 b) (sqrt (* (* c a) -1))) a)) (/ (+ (* 1/2 b) (sqrt (* (* c a) -1))) a) (+ (* 1/2 b) (sqrt (* (* c a) -1))) 1/2 (sqrt (* (* c a) -1)) (* (* c a) -1) (* c a) (if (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (if (>= b 0) (* (/ (+ (sqrt (+ (* (* -4 a) c) (* b b))) b) a) -1/2) (/ (* 2 c) (- (sqrt (+ (* (* -4 a) c) (* b b))) b))) (* (/ (+ (sqrt (+ (* (* -4 a) c) (* b b))) b) a) -1/2) (+ (* -1/2 (/ b a)) (sqrt (* (/ c a) -1))) (/ b a) (/ (* 2 c) (- (sqrt (+ (* (* -4 a) c) (* b b))) b)) (- (sqrt (+ (* (* -4 a) c) (* b b))) b) (sqrt (+ (* (* -4 a) c) (* b b))) (+ (* (* -4 a) c) (* b b)) (* -4 a) (if (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* (- (/ (neg b) c) (sqrt (* (/ a c) -4))) c) (- (/ (neg b) c) (sqrt (* (/ a c) -4))) (/ (neg b) c) (sqrt (* (/ a c) -4)) (* (/ a c) -4) (/ a c))

derivations1.4s (5%)

Memory
-2.8MiB live, 874.3MiB allocated; 121ms collecting garbage
Stop Event
done
fuel
Compiler

Compiled 4 182 to 572 computations (86.3% saved)

prune857.0ms (3%)

Memory
125.3MiB live, 1 231.8MiB allocated; 232ms collecting garbage
Counts
9 983 → 273
Compiler

Compiled 24 317 to 11 824 computations (51.4% saved)

bsearch809.0ms (2.8%)

Memory
40.7MiB live, 792.5MiB allocated; 117ms collecting garbage
Algorithm
55×binary-search
left-value
Stop Event
52×narrow-enough
predicate-same
Samples
397.0ms3 840×0valid
51.0ms435×0invalid
15.0ms96×2valid
Compiler

Compiled 40 828 to 25 472 computations (37.6% saved)

Precisions
Click to see histograms. Total time spent on operations: 307.0ms
ival-mult: 115.0ms (37.4% of total)
ival-div: 55.0ms (17.9% of total)
ival-sub: 36.0ms (11.7% of total)
ival-sqrt: 25.0ms (8.1% of total)
ival-add: 19.0ms (6.2% of total)
ival-neg: 13.0ms (4.2% of total)
ival-if: 12.0ms (3.9% of total)
ival->=: 9.0ms (2.9% of total)
ival-fabs: 7.0ms (2.3% of total)
exact: 5.0ms (1.6% of total)
adjust: 4.0ms (1.3% of total)
ival-true: 3.0ms (1% of total)
ival-assert: 2.0ms (0.7% of total)
ival-exp: 1.0ms (0.3% of total)

analyze617.0ms (2.2%)

Memory
32.0MiB live, 692.3MiB allocated; 165ms collecting garbage
Algorithm
search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%99.9%0.1%0%0%0%0
22.2%22.2%77.7%0.1%0%0%0%1
29.4%27.8%66.6%0.1%0%5.6%0%2
50%44.4%44.4%0.1%0%11.1%0%3
59.7%51.3%34.7%0.1%0%13.9%0%4
66.4%56.2%28.4%0.1%0%15.3%0%5
74%62.1%21.8%0.1%0%16%0%6
77.6%63.8%18.4%0.1%0%17.7%0%7
79.3%65%17%0.1%0%17.9%0%8
85%69.2%12.2%0.1%0%18.5%0%9
86.8%69.7%10.6%0.1%0%19.6%0%10
88.7%71.1%9.1%0.1%0%19.8%0%11
91.6%72.9%6.7%0.1%0%20.3%0%12
Compiler

Compiled 153 to 106 computations (30.7% saved)

regimes600.0ms (2.1%)

Memory
63.4MiB live, 865.4MiB allocated; 98ms collecting garbage
Counts
532 → 114
Calls

26 calls:

108.0ms
b
64.0ms
c
46.0ms
x
42.0ms
a
40.0ms
(exp.f64 (neg.f64 (-.f64 #s(literal 1 binary64) (*.f64 x x))))
Compiler

Compiled 994 to 826 computations (16.9% saved)

simplify475.0ms (1.7%)

Memory
-77.3MiB live, 490.9MiB allocated; 86ms collecting garbage
Stop Event
node limit

start0.0ms (0%)

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

end0.0ms (0%)

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

Profiling

Loading profile data...