Herbie run

Date:Wednesday, May 14th, 2025
Commit:0476ec29 on no-reduce-sqrt
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:26 000.3 MB

Time bar (total: 23.4s)

sample8.9s (38.1%)

Memory
262.3MiB live, 9 055.1MiB allocated; 4.7s collecting garbage
Samples
5.5s70 221×0valid
757.0ms4 076×2valid
138.0ms1 862×0invalid
1.0ms1valid
Precisions
Click to see histograms. Total time spent on operations: 3.7s
ival-sqrt: 876.0ms (24% of total)
ival-mult!: 768.0ms (21% of total)
ival-sub!: 606.0ms (16.6% of total)
ival-div!: 588.0ms (16.1% of total)
ival-neg: 296.0ms (8.1% of total)
adjust: 123.0ms (3.4% of total)
ival-fabs: 114.0ms (3.1% of total)
ival-exp: 93.0ms (2.5% of total)
ival-add!: 93.0ms (2.5% of total)
ival-log: 90.0ms (2.5% of total)
ival-if: 4.0ms (0.1% of total)
ival->=: 3.0ms (0.1% of total)
Bogosity

rewrite5.6s (24%)

Memory
27.5MiB live, 5 795.2MiB allocated; 1.2s collecting garbage
Stop Event
79×iter-limit
30×node-limit
saturated
unsound
Counts
4 939 → 8 097

derivations1.8s (7.7%)

Memory
37.2MiB live, 1 597.7MiB allocated; 312ms collecting garbage
Stop Event
done
fuel
Compiler

Compiled 1 088 to 632 computations (41.9% saved)

preprocess1.5s (6.2%)

Memory
-210.2MiB live, 1 701.9MiB allocated; 391ms collecting garbage
Stop Event
node-limit
Compiler

Compiled 2 061 to 1 514 computations (26.5% saved)

regimes1.2s (5.3%)

Memory
-16.9MiB live, 1 679.0MiB allocated; 333ms collecting garbage
Counts
836 → 132
Calls

26 calls:

355.0ms
b
118.0ms
a
94.0ms
(if (>=.f64 b #s(literal 0 binary64)) (/.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)) (/.f64 (*.f64 #s(literal 2 binary64) c) (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 #s(literal 4 binary64) a) c))))))
87.0ms
(log.f64 (-.f64 (/.f64 #s(literal 1 binary64) x) #s(literal 1 binary64)))
74.0ms
x
Compiler

Compiled 955 to 960 computations (-0.5% saved)

eval1.2s (5%)

Memory
267.0MiB live, 2 060.3MiB allocated; 382ms collecting garbage
Compiler

Compiled 143 874 to 39 842 computations (72.3% saved)

series1.1s (4.6%)

Memory
172.1MiB live, 1 398.4MiB allocated; 183ms collecting garbage
Counts
698 → 4 241
Calls

189 calls:

TimeVariablePointExpression
65.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))) -2 (* (/ (- (sqrt (+ (* (* -4 a) c) (* b b))) b) a) 1/2) (* -1 (/ b a)) -1 (/ b a) 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) (* (/ (- (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) 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))) (/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (/ -2 (sqrt (* -4 (/ a c)))) (sqrt (* -4 (/ a c))) (* -4 (/ a c)) -4 (/ 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))) (* 2 a) 2 (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) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (sqrt (- (* b b) (* (* 4 a) c))) (- (* b b) (* (* 4 a) c)) (* b b) (/ (+ (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))) (sqrt (* (/ c a) -4)) (* (/ c a) -4) (/ c a) (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))))) (/ (* -1 (+ c (/ (* a (* c c)) (* b b)))) b) (* -1 (+ c (/ (* a (* c c)) (* b b)))) (+ c (/ (* a (* c c)) (* b b))) (/ (* a (* c c)) (* b b)) (* a (* c c)) (* c c) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* -2 b))
56.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 x) -1 (neg (log (- (/ 1 x) 1))) (log (- (/ 1 x) 1)) (- (/ 1 x) 1) (/ (- 1 x) x) (- 1 x) 1)
42.0ms
a
@0
((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))) (>= b 0) b 0 (* (/ (+ (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) (sqrt (+ (* (* -4 a) c) (* b b))) (+ (* (* -4 a) c) (* b b)) (* -4 a) -4 a c (* b b) -1/2 (/ (+ c c) (- (sqrt (+ (* (* -4 a) c) (* b b))) b)) (+ c c) (- (sqrt (+ (* (* -4 a) c) (* b 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)) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (neg b) (sqrt (- (* b b) (* (* 4 a) c))) (* 2 a) 2 (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (* 2 c) (+ (neg b) (sqrt (- (* 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)))) (sqrt (- (* b b) (* (* 4 a) c))) (* (sqrt (* (/ c a) -4)) a) (sqrt (* (/ c a) -4)) (* (/ c a) -4) (/ c a) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (+ (neg b) (sqrt (- (* 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)) (* (sqrt (* (/ c a) -4)) -1/2) (/ (* 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 (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 (+ (/ b (* c a)) (/ (sqrt (* (/ a c) -4)) a))) c) (* -1/2 (+ (/ b (* c a)) (/ (sqrt (* (/ a c) -4)) a))) (+ (/ b (* c a)) (/ (sqrt (* (/ a c) -4)) a)) (/ b (* c a)) (* c a) (/ (sqrt (* (/ a c) -4)) a) (sqrt (* (/ a c) -4)) (* (/ a c) -4) (/ a c))
35.0ms
z
@0
((fabs (/ (+ (* z x) (- -4 x)) y)) (/ (+ (* z x) (- -4 x)) y) (+ (* z x) (- -4 x)) (* (- (- z 1) (/ 4 x)) x) (- (- z 1) (/ 4 x)) (- z 1) z 1 (/ 4 x) 4 x y (fabs (- (/ (+ x 4) y) (* (/ x y) z))) (- (/ (+ x 4) y) (* (/ x y) z)) (/ (- x -4) y) (- x -4) -4 (fabs (/ (+ (* z x) (- -4 x)) y)) (/ (+ (* z x) (- -4 x)) y) (+ (* z x) (- -4 x)) (- -4 x) (fabs (+ (* (/ (- 1 z) y) x) (/ 4 y))) (+ (* (/ (- 1 z) y) x) (/ 4 y)) (/ (- 1 z) y) (- 1 z) (/ 4 y) (fabs (/ (+ (* (* (- 1 z) x) y) (* y 4)) (* y y))) (/ (+ (* (* (- 1 z) x) y) (* y 4)) (* y y)) (+ (* (* (- 1 z) x) y) (* y 4)) (* (- 1 z) x) (- 1 z) (* y 4) (* y y))
29.0ms
b
@inf
((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))) (>= b 0) b 0 (* (/ (+ (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) (sqrt (+ (* (* -4 a) c) (* b b))) a -1/2 (/ (+ c c) (- (sqrt (+ (* (* -4 a) c) (* b b))) b)) (+ c c) c (- (sqrt (+ (* (* -4 a) c) (* b b))) b) (* -2 b) -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) (/ (neg b) a) (neg b) (/ (+ c c) (- (sqrt (+ (* (* -4 a) c) (* b b))) b)) (- (sqrt (+ (* (* -4 a) c) (* b 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)) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (sqrt (- (* b b) (* (* 4 a) c))) (* 2 a) 2 (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (/ 2 (sqrt (* (/ a c) -4))) (sqrt (* (/ a c) -4)) (* (/ a c) -4) (/ a c) -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)) (* (- (/ c (* b b)) (/ 1 a)) b) (- (/ c (* b b)) (/ 1 a)) (/ c (* b b)) (* b b) (/ 1 a) 1 (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (* 2 c) (+ (neg b) (sqrt (- (* 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)))))) (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) (+ (sqrt (+ (* (* -4 a) c) (* b b))) b) (sqrt (+ (* (* -4 a) c) (* b b))) (* (sqrt (* (/ c a) -4)) a) (sqrt (* (/ c a) -4)) (* (/ c a) -4) (/ c a) (/ (+ c c) (- (sqrt (+ (* (* -4 a) c) (* b b))) b)) (- (sqrt (+ (* (* -4 a) c) (* b b))) b))

bsearch861.0ms (3.7%)

Memory
-15.3MiB live, 1 139.1MiB allocated; 265ms collecting garbage
Algorithm
60×binary-search
10×left-value
Stop Event
52×narrow-enough
predicate-same
Samples
309.0ms3 744×0valid
63.0ms112×2valid
37.0ms450×0invalid
1.0ms16×1valid
Compiler

Compiled 30 042 to 25 585 computations (14.8% saved)

Precisions
Click to see histograms. Total time spent on operations: 292.0ms
ival-div!: 75.0ms (25.7% of total)
ival-mult!: 65.0ms (22.3% of total)
adjust: 54.0ms (18.5% of total)
ival-sub!: 28.0ms (9.6% of total)
ival-sqrt: 18.0ms (6.2% of total)
ival-neg: 12.0ms (4.1% of total)
ival-if: 11.0ms (3.8% of total)
ival-add!: 9.0ms (3.1% of total)
ival->=: 8.0ms (2.7% of total)
ival-fabs: 8.0ms (2.7% of total)
ival-exp: 2.0ms (0.7% of total)

prune702.0ms (3%)

Memory
-223.8MiB live, 1 056.3MiB allocated; 252ms collecting garbage
Counts
7 929 → 357
Compiler

Compiled 18 672 to 14 334 computations (23.2% saved)

analyze557.0ms (2.4%)

Memory
39.1MiB live, 516.5MiB allocated; 564ms 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)

start0.0ms (0%)

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

end0.0ms (0%)

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

Profiling

Loading profile data...