Herbie run

Date:Thursday, May 22nd, 2025
Commit:9e1ea048 on batch-critical-subexpressions
Seed:2025142
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:29 022.8 MB

Time bar (total: 23.9s)

sample8.9s (37.4%)

Memory
225.6MiB live, 10 498.5MiB allocated; 5.3s collecting garbage
Samples
5.0s70 174×0valid
845.0ms4 118×2valid
212.0ms1 991×0invalid
1.0ms12×1valid
Precisions
Click to see histograms. Total time spent on operations: 3.7s
ival-mult!: 880.0ms (23.7% of total)
ival-div!: 840.0ms (22.6% of total)
ival-sub!: 492.0ms (13.2% of total)
ival-sqrt: 435.0ms (11.7% of total)
ival-neg: 373.0ms (10% of total)
ival-add!: 216.0ms (5.8% of total)
adjust: 161.0ms (4.3% of total)
ival-log: 110.0ms (3% of total)
ival-exp: 106.0ms (2.9% of total)
ival-fabs: 100.0ms (2.7% of total)
ival-if: 4.0ms (0.1% of total)
ival->=: 3.0ms (0.1% of total)
Bogosity

rewrite6.0s (25.1%)

Memory
105.1MiB live, 6 622.9MiB allocated; 1.6s collecting garbage
Stop Event
78×iter-limit
29×node-limit
2×unsound
1×saturated
Counts
3 851 → 8 473

derivations1.6s (6.7%)

Memory
-113.1MiB live, 2 076.3MiB allocated; 363ms collecting garbage
Stop Event
5×done
4×fuel
Compiler

Compiled 7 147 to 644 computations (91% saved)

eval1.5s (6.1%)

Memory
-216.4MiB live, 2 203.2MiB allocated; 549ms collecting garbage
Compiler

Compiled 414 681 to 41 273 computations (90% saved)

preprocess1.4s (5.7%)

Memory
-122.0MiB live, 1 628.1MiB allocated; 465ms collecting garbage
Stop Event
9×node-limit
Compiler

Compiled 8 454 to 1 442 computations (82.9% saved)

regimes1.1s (4.7%)

Memory
-38.9MiB live, 2 054.7MiB allocated; 260ms collecting garbage
Counts
766 → 128
Calls

26 calls:

170.0ms
b
56.0ms
x
53.0ms
a
50.0ms
c
34.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))))))
Compiler

Compiled 9 449 to 1 982 computations (79% saved)

series1.1s (4.7%)

Memory
188.3MiB live, 1 388.2MiB allocated; 208ms collecting garbage
Counts
774 → 3 077
Calls

186 calls:

TimeVariablePointExpression
72.0ms
a
@-inf
((if (>= b 0) (/ (* 2 c) (- (neg b) (exp (* (log (+ (* (* -4 a) c) (* b b))) 1/2)))) (/ (+ (neg b) (exp (* (log (+ (* (* -4 a) c) (* b b))) 1/2))) (* 2 a))) (>= b 0) b 0 (/ (* 2 c) (- (neg b) (exp (* (log (+ (* (* -4 a) c) (* b b))) 1/2)))) (* 2 c) 2 c (- (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 (* b b) 1/2 (/ (+ (neg b) (exp (* (log (+ (* (* -4 a) c) (* b b))) 1/2))) (* 2 a)) (+ (neg b) (exp (* (log (+ (* (* -4 a) c) (* b b))) 1/2))) (* 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)))) -1 (sqrt (* -4 (/ a c))) (* -4 (/ a c)) (/ a c) -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) (sqrt (+ (* (* -4 a) c) (* b b))) (sqrt (* 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))) (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) (* -2 (/ (* a c) b)) (/ (* a c) b) (* a c) (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))) (* a (sqrt (/ -4 (* a c)))) (sqrt (/ -4 (* a c))) (/ -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) (sqrt (+ (* (* -4 a) c) (* 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)) (+ (* b b) (* -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 c) (+ (/ b c) (sqrt (* (/ a c) -4)))) (* -1 (+ b (* c (sqrt (* -4 (/ a c)))))) (+ b (* c (sqrt (* -4 (/ a c))))) (* c (sqrt (* -4 (/ a c)))))
68.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)
51.0ms
c
@inf
((if (>= b 0) (/ (* 2 c) (- (neg b) (exp (* (log (+ (* (* -4 a) c) (* b b))) 1/2)))) (/ (+ (neg b) (exp (* (log (+ (* (* -4 a) c) (* b b))) 1/2))) (* 2 a))) (>= b 0) b 0 (/ (* 2 c) (- (neg b) (exp (* (log (+ (* (* -4 a) c) (* b b))) 1/2)))) (* 2 c) 2 c (- (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 (* b b) 1/2 (/ (+ (neg b) (exp (* (log (+ (* (* -4 a) c) (* b b))) 1/2))) (* 2 a)) (+ (neg b) (exp (* (log (+ (* (* -4 a) c) (* b b))) 1/2))) (* 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)))) -1 (sqrt (* -4 (/ a c))) (* -4 (/ a c)) (/ a c) -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) (sqrt (+ (* (* -4 a) c) (* b b))) (sqrt (* 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))) (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) (* -2 (/ (* a c) b)) (/ (* a c) b) (* a c) (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))) (* a (sqrt (/ -4 (* a c)))) (sqrt (/ -4 (* a c))) (/ -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) (sqrt (+ (* (* -4 a) c) (* 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)) (+ (* b b) (* -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 c) (+ (/ b c) (sqrt (* (/ a c) -4)))) (* -1 (+ b (* c (sqrt (* -4 (/ a c)))))) (+ b (* c (sqrt (* -4 (/ a c))))) (* c (sqrt (* -4 (/ a c)))))
41.0ms
y
@0
((fabs (+ (* (/ (- 1 z) y) x) (/ 4 y))) (+ (* (/ (- 1 z) y) x) (/ 4 y)) (+ (/ x y) (/ 4 y)) (/ x y) x y (/ 4 y) 4 (fabs (- (/ (+ x 4) y) (* (/ x y) z))) (- (/ (+ x 4) y) (* (/ x y) z)) (* (/ (- 1 z) y) x) (/ (- 1 z) y) (* (- (/ 1 (* y z)) (/ 1 y)) z) (- (/ 1 (* y z)) (/ 1 y)) (/ 1 (* y z)) 1 (* y z) z (/ 1 y) (fabs (- (/ (+ x 4) y) (* (/ x y) z))) (- (/ (+ x 4) y) (* (/ x y) z)) (* (/ (- (/ 1 (* y y)) (/ (* z z) (* y y))) (/ (+ 1 z) y)) x) (/ (- (/ 1 (* y y)) (/ (* z z) (* y y))) (/ (+ 1 z) y)) (- (/ 1 (* y y)) (/ (* z z) (* y y))) (/ 1 (* y y)) (* y y) (/ (* z z) (* y y)) (* z z) (/ (+ 1 z) y) (+ 1 z) (fabs (/ (+ (* z x) (- -4 x)) y)) (/ (+ (* z x) (- -4 x)) y) (* x (/ z y)) (/ z y))
33.0ms
a
@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))) a) (/ 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))) a) (/ b a)) 1/2) (- (/ (sqrt (+ (* (* -4 a) c) (* b b))) a) (/ b a)) (/ (sqrt (+ (* (* -4 a) c) (* b 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))) (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)) (* -4 (* a c)) (* 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))) (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)))) -1 (sqrt (* -4 (/ a c))) (* -4 (/ a c)) (/ 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))))) (* 2 c) 2 (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (neg b) (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)) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* (neg c) (+ (/ b c) (sqrt (* (/ a c) -4)))) (* -1 (+ b (* c (sqrt (* -4 (/ a c)))))) (+ b (* c (sqrt (* -4 (/ a c))))) (* c (sqrt (* -4 (/ a c)))) (* 2 a))

analyze969.0ms (4.1%)

Memory
42.0MiB live, 496.1MiB allocated; 1.6s 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)

bsearch859.0ms (3.6%)

Memory
105.1MiB live, 1 247.8MiB allocated; 123ms collecting garbage
Algorithm
62×binary-search
8×left-value
Stop Event
46×narrow-enough
16×predicate-same
Samples
312.0ms3 552×0valid
113.0ms817×0invalid
11.0ms96×2valid
Compiler

Compiled 70 684 to 39 147 computations (44.6% saved)

Precisions
Click to see histograms. Total time spent on operations: 291.0ms
ival-mult!: 85.0ms (29.2% of total)
ival-div!: 74.0ms (25.4% of total)
ival-sub!: 34.0ms (11.7% of total)
ival-neg: 31.0ms (10.7% of total)
ival-sqrt: 24.0ms (8.3% of total)
ival-if: 15.0ms (5.2% of total)
ival->=: 11.0ms (3.8% of total)
ival-add!: 9.0ms (3.1% of total)
adjust: 3.0ms (1% of total)
ival-fabs: 3.0ms (1% of total)
ival-exp: 1.0ms (0.3% of total)

prune474.0ms (2%)

Memory
150.0MiB live, 806.4MiB allocated; 85ms collecting garbage
Counts
7 838 → 296
Compiler

Compiled 20 257 to 11 697 computations (42.3% saved)

start0.0ms (0%)

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

end0.0ms (0%)

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

Profiling

Loading profile data...