Herbie run

Date:Sunday, May 18th, 2025
Commit:599f26b5 on main
Seed:2025138
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:26 978.8 MB

Time bar (total: 23.6s)

sample9.0s (38.3%)

Memory
127.3MiB live, 9 439.4MiB allocated; 5.5s collecting garbage
Samples
5.3s70 204×0valid
871.0ms4 086×2valid
160.0ms1 936×0invalid
1.0ms14×1valid
Precisions
Click to see histograms. Total time spent on operations: 4.0s
ival-mult!: 1.2s (30.3% of total)
ival-div!: 868.0ms (21.9% of total)
ival-neg: 513.0ms (13% of total)
ival-sqrt: 461.0ms (11.6% of total)
ival-sub!: 262.0ms (6.6% of total)
adjust: 188.0ms (4.7% of total)
ival-log: 165.0ms (4.2% of total)
ival-add!: 120.0ms (3% of total)
ival-fabs: 113.0ms (2.9% of total)
ival-exp: 67.0ms (1.7% of total)
ival-if: 4.0ms (0.1% of total)
ival->=: 3.0ms (0.1% of total)
Bogosity

rewrite5.8s (24.6%)

Memory
91.8MiB live, 6 171.9MiB allocated; 1.4s collecting garbage
Stop Event
79×iter-limit
30×node-limit
2×unsound
1×saturated
Counts
3 957 → 8 438

derivations1.9s (8.1%)

Memory
41.3MiB live, 1 862.4MiB allocated; 510ms collecting garbage
Stop Event
5×done
4×fuel
Compiler

Compiled 1 174 to 721 computations (38.6% saved)

eval1.4s (5.7%)

Memory
74.8MiB live, 2 295.2MiB allocated; 513ms collecting garbage
Compiler

Compiled 130 513 to 41 295 computations (68.4% saved)

preprocess1.3s (5.3%)

Memory
-134.7MiB live, 1 475.8MiB allocated; 307ms collecting garbage
Stop Event
9×node-limit
Compiler

Compiled 2 243 to 1 677 computations (25.2% saved)

regimes1.2s (5%)

Memory
-161.5MiB live, 1 363.8MiB allocated; 362ms collecting garbage
Counts
872 → 134
Calls

26 calls:

393.0ms
b
143.0ms
x
63.0ms
a
59.0ms
(exp.f64 (neg.f64 (-.f64 #s(literal 1 binary64) (*.f64 x x))))
54.0ms
c
Compiler

Compiled 814 to 855 computations (-5% saved)

series1.0s (4.4%)

Memory
256.6MiB live, 1 648.1MiB allocated; 228ms collecting garbage
Counts
788 → 3 169
Calls

189 calls:

TimeVariablePointExpression
47.0ms
c
@-inf
((if (>= b 0) (/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a))) (if (>= b 0) (* (/ c (+ (sqrt (+ (* (* -4 a) c) (* b b))) b)) -2) (* (/ (- (sqrt (+ (* (* -4 a) c) (* b b))) b) a) 1/2)) (>= b 0) b 0 (* (/ c (+ (sqrt (+ (* (* -4 a) c) (* b b))) b)) -2) (/ c (+ (sqrt (+ (* (* -4 a) c) (* b b))) b)) c (+ (sqrt (+ (* (* -4 a) c) (* b b))) b) (sqrt (+ (* (* -4 a) c) (* b b))) (+ (* (* -4 a) c) (* b b)) (* -4 a) -4 a (* b b) -2 (* (/ (- (sqrt (+ (* (* -4 a) c) (* b b))) b) a) 1/2) (/ (- (sqrt (+ (* (* -4 a) c) (* b b))) b) a) (* -2 (/ b a)) (/ b a) 1/2 (if (>= b 0) (/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a))) (if (>= b 0) (* (/ c (+ (sqrt (+ (* (* -4 a) c) (* b b))) b)) -2) (* (/ (- (sqrt (+ (* (* -4 a) c) (* b b))) b) a) 1/2)) (* (/ c (+ (sqrt (+ (* (* -4 a) c) (* b b))) b)) -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)) (* (/ (- (sqrt (+ (* (* -4 a) c) (* b b))) b) a) 1/2) (/ (- (sqrt (+ (* (* -4 a) c) (* b b))) b) a) (- (sqrt (+ (* (* -4 a) c) (* b b))) b) (if (>= b 0) (/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a))) (/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (* 2 c) 2 (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* -1 (* c (sqrt (* -4 (/ a c))))) -1 (* c (sqrt (* -4 (/ a c)))) (sqrt (* -4 (/ a c))) (* -4 (/ a c)) (/ a c) (/ (+ (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)) (* 2 a) (if (>= b 0) (/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a))) (if (>= b 0) (* (/ c (+ (sqrt (+ (* (* -4 a) c) (* b b))) b)) -2) (* (/ (- (sqrt (+ (* (* -4 a) c) (* b b))) b) a) 1/2)) (* (/ c (+ (sqrt (+ (* (* -4 a) c) (* b b))) b)) -2) (/ c (+ (sqrt (+ (* (* -4 a) c) (* b b))) b)) (/ -1 (sqrt (* -4 (/ a c)))) (* (/ (- (sqrt (+ (* (* -4 a) c) (* b b))) b) a) 1/2) (/ (- (sqrt (+ (* (* -4 a) c) (* b b))) b) a) (- (sqrt (+ (* (* -4 a) c) (* b b))) b) (if (>= b 0) (/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (/ (+ (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)))) (sqrt (- (* b b) (* (* 4 a) c))) (- (* b b) (* (* 4 a) c)) (* (* 4 a) c) (* 4 a) 4 (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (* -1/2 (+ (/ b a) (sqrt (* (/ c a) -4)))) -1/2 (+ (/ b a) (sqrt (* (/ c a) -4))) (* c (+ (sqrt (/ -4 (* a c))) (/ b (* a c)))) (+ (sqrt (/ -4 (* a c))) (/ b (* a c))) (sqrt (/ -4 (* a c))) (/ -4 (* a c)) (* a c) (/ b (* a c)))
35.0ms
a
@-inf
((if (>= b 0) (/ (- (neg b) (exp (* (log (+ (* (* -4 a) c) (* b b))) 1/2))) (* 2 a)) (/ (* 2 c) (+ (neg b) (exp (* (log (+ (* (* -4 a) c) (* b b))) 1/2))))) (>= b 0) b 0 (/ (- (neg b) (exp (* (log (+ (* (* -4 a) c) (* b b))) 1/2))) (* 2 a)) (- (neg b) (exp (* (log (+ (* (* -4 a) c) (* b b))) 1/2))) (neg b) (exp (* (log (+ (* (* -4 a) c) (* b b))) 1/2)) (* (log (+ (* (* -4 a) c) (* b b))) 1/2) (log (+ (* (* -4 a) c) (* b b))) (+ (* (* -4 a) c) (* b b)) (* -4 a) -4 a c (* b b) 1/2 (* 2 a) 2 (/ (* 2 c) (+ (neg b) (exp (* (log (+ (* (* -4 a) c) (* b b))) 1/2)))) (* 2 c) (+ (neg b) (exp (* (log (+ (* (* -4 a) c) (* b b))) 1/2))) (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) (/ (+ c c) (- (sqrt (+ (* (* -4 a) c) (* b b))) b))) (* (/ (+ (sqrt (+ (* (* -4 a) c) (* b b))) b) a) -1/2) (/ (+ (sqrt (+ (* (* -4 a) c) (* b b))) b) a) (neg (sqrt (* -4 (/ c a)))) (sqrt (* -4 (/ c a))) (* -4 (/ c a)) (/ c a) -1/2 (/ (+ c c) (- (sqrt (+ (* (* -4 a) c) (* b b))) b)) (+ c c) (- (sqrt (+ (* (* -4 a) c) (* b b))) b) (sqrt (+ (* (* -4 a) c) (* b b))) (+ (* (* -4 a) c) (* b b)) (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)) (* -1/2 (/ (sqrt (* (* -4 a) c)) a)) (/ (sqrt (* (* -4 a) c)) a) (sqrt (* (* -4 a) c)) (* (* -4 a) c) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (sqrt (- (* b b) (* (* 4 a) c))) (- (* b b) (* (* 4 a) c)) (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 (* c (sqrt (* -4 (/ a c))))) (* c (sqrt (* -4 (/ a c)))) (sqrt (* -4 (/ a c))) (* -4 (/ a c)) (/ a c) (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) (/ (+ c c) (- (sqrt (+ (* (* -4 a) c) (* b b))) b))) (* (/ (+ (sqrt (+ (* (* -4 a) c) (* b b))) b) a) -1/2) (/ (+ (sqrt (+ (* (* -4 a) c) (* b b))) b) a) (neg (/ (* c (sqrt (* -4 (/ a c)))) a)) (/ (* c (sqrt (* -4 (/ a c)))) a) (* c (sqrt (* -4 (/ a c)))) (* a (* c (sqrt (/ -4 (* a c))))) (* c (sqrt (/ -4 (* a c)))) (sqrt (/ -4 (* a c))) (/ -4 (* a c)) (* a c) (/ (+ c c) (- (sqrt (+ (* (* -4 a) c) (* b b))) b)) (- (sqrt (+ (* (* -4 a) c) (* b b))) b) (sqrt (+ (* (* -4 a) c) (* b b))))
34.0ms
x
@0
((neg (log (- (/ 1 x) 1))) (log x) x (neg (log (- (/ 1 x) 1))) (+ (log x) x) (neg (log (- (/ 1 x) 1))) (/ -1 x) -1 (log (/ 1 (- (/ 1 x) 1))) (/ 1 (- (/ 1 x) 1)) 1 (- (/ 1 x) 1) (/ 1 x))
30.0ms
y
@inf
((fabs (/ (+ (* z x) (- -4 x)) y)) (/ (+ (* z x) (- -4 x)) y) (+ (* z x) (- -4 x)) z x (- -4 x) -4 y (fabs (- (/ (+ x 4) y) (* (/ x y) z))) (- (/ (+ x 4) y) (* (/ x y) z)) (/ 4 y) 4 (fabs (- (/ (+ x 4) y) (* (/ x y) z))) (- (/ (+ x 4) y) (* (/ x y) z)) (* (/ (- 1 z) y) x) (/ (- 1 z) y) (- 1 z) 1 (fabs (+ (* (/ x y) (+ z -1)) (/ 4 y))) (+ (* (/ x y) (+ z -1)) (/ 4 y)) (/ x y) (+ z -1) -1 (fabs (- (/ (/ 16 (* y y)) (/ (- (- x -4) (* z x)) y)) (/ (* (* (* (/ (- 1 z) y) x) (/ (- 1 z) y)) x) (/ (- (- x -4) (* z x)) y)))) (- (/ (/ 16 (* y y)) (/ (- (- x -4) (* z x)) y)) (/ (* (* (* (/ (- 1 z) y) x) (/ (- 1 z) y)) x) (/ (- (- x -4) (* z x)) y))) (/ (/ 16 (* y y)) (/ (- (- x -4) (* z x)) y)) (/ 16 (* y y)) 16 (* y y) (/ (- (- x -4) (* z x)) y) (- (- x -4) (* z x)) (- x -4) (* z x) (/ (* (* (* (/ (- 1 z) y) x) (/ (- 1 z) y)) x) (/ (- (- x -4) (* z x)) y)) (* (* (* (/ (- 1 z) y) x) (/ (- 1 z) y)) x) (* (* (/ (- 1 z) y) x) (/ (- 1 z) y)))
29.0ms
x
@inf
((fabs (/ (+ (* z x) (- -4 x)) y)) (/ (+ (* z x) (- -4 x)) y) (+ (* z x) (- -4 x)) z x (- -4 x) -4 y (fabs (- (/ (+ x 4) y) (* (/ x y) z))) (- (/ (+ x 4) y) (* (/ x y) z)) (/ 4 y) 4 (fabs (- (/ (+ x 4) y) (* (/ x y) z))) (- (/ (+ x 4) y) (* (/ x y) z)) (* (/ (- 1 z) y) x) (/ (- 1 z) y) (- 1 z) 1 (fabs (+ (* (/ x y) (+ z -1)) (/ 4 y))) (+ (* (/ x y) (+ z -1)) (/ 4 y)) (/ x y) (+ z -1) -1 (fabs (- (/ (/ 16 (* y y)) (/ (- (- x -4) (* z x)) y)) (/ (* (* (* (/ (- 1 z) y) x) (/ (- 1 z) y)) x) (/ (- (- x -4) (* z x)) y)))) (- (/ (/ 16 (* y y)) (/ (- (- x -4) (* z x)) y)) (/ (* (* (* (/ (- 1 z) y) x) (/ (- 1 z) y)) x) (/ (- (- x -4) (* z x)) y))) (/ (/ 16 (* y y)) (/ (- (- x -4) (* z x)) y)) (/ 16 (* y y)) 16 (* y y) (/ (- (- x -4) (* z x)) y) (- (- x -4) (* z x)) (- x -4) (* z x) (/ (* (* (* (/ (- 1 z) y) x) (/ (- 1 z) y)) x) (/ (- (- x -4) (* z x)) y)) (* (* (* (/ (- 1 z) y) x) (/ (- 1 z) y)) x) (* (* (/ (- 1 z) y) x) (/ (- 1 z) y)))

bsearch875.0ms (3.7%)

Memory
-20.0MiB live, 1 246.3MiB allocated; 244ms collecting garbage
Algorithm
66×binary-search
6×left-value
Stop Event
56×narrow-enough
10×predicate-same
Samples
338.0ms3 904×0valid
92.0ms677×0invalid
12.0ms96×2valid
Compiler

Compiled 44 768 to 38 007 computations (15.1% saved)

Precisions
Click to see histograms. Total time spent on operations: 288.0ms
ival-mult!: 108.0ms (37.5% of total)
ival-div!: 42.0ms (14.6% of total)
ival-neg: 41.0ms (14.2% of total)
ival-sqrt: 26.0ms (9% of total)
ival-if: 18.0ms (6.3% of total)
ival->=: 18.0ms (6.3% of total)
ival-sub!: 17.0ms (5.9% of total)
ival-add!: 9.0ms (3.1% of total)
ival-fabs: 5.0ms (1.7% of total)
adjust: 3.0ms (1% of total)
ival-exp: 1.0ms (0.3% of total)

prune627.0ms (2.7%)

Memory
-42.8MiB live, 1 013.5MiB allocated; 276ms collecting garbage
Counts
7 489 → 327
Compiler

Compiled 18 182 to 14 458 computations (20.5% saved)

analyze510.0ms (2.2%)

Memory
19.1MiB live, 461.8MiB allocated; 136ms collecting garbage
Algorithm
9×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)

start0.0ms (0%)

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

end0.0ms (0%)

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

Profiling

Loading profile data...