Herbie run

Date:Saturday, April 26th, 2025
Commit:af246fab on time-nightly
Seed:2025116
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:24 247.3 MB

Time bar (total: 22.0s)

sample9.0s (41%)

Memory
274.1MiB live, 9 193.9MiB allocated; 4.8s collecting garbage
Samples
5.2s70 154×0valid
978.0ms4 141×2valid
136.0ms1 916×0invalid
1.0ms9×1valid
Precisions
Click to see histograms. Total time spent on operations: 3.7s
ival-mult!: 1.2s (32.8% of total)
ival-div!: 559.0ms (15.2% of total)
ival-sqrt: 457.0ms (12.4% of total)
ival-exp: 342.0ms (9.3% of total)
ival-neg: 319.0ms (8.7% of total)
ival-sub!: 306.0ms (8.3% of total)
ival-add!: 165.0ms (4.5% of total)
adjust: 120.0ms (3.3% of total)
ival-log: 104.0ms (2.8% of total)
ival-fabs: 92.0ms (2.5% of total)
ival-if: 4.0ms (0.1% of total)
ival->=: 3.0ms (0.1% of total)
Bogosity

rewrite5.2s (23.8%)

Memory
199.1MiB live, 5 688.4MiB allocated; 1.2s collecting garbage
Stop Event
74×iter-limit
28×node-limit
2×saturated
2×unsound
Counts
4 384 → 7 078

derivations1.7s (7.9%)

Memory
-72.9MiB live, 1 600.0MiB allocated; 311ms collecting garbage
Stop Event
6×done
3×fuel
Compiler

Compiled 1 024 to 606 computations (40.8% saved)

preprocess1.2s (5.6%)

Memory
-95.3MiB live, 1 255.3MiB allocated; 255ms collecting garbage
Stop Event
8×node-limit
1×saturated
Compiler

Compiled 2 141 to 1 620 computations (24.3% saved)

eval1.1s (5%)

Memory
-78.2MiB live, 1 659.8MiB allocated; 404ms collecting garbage
Compiler

Compiled 120 509 to 34 666 computations (71.2% saved)

series979.0ms (4.4%)

Memory
251.9MiB live, 1 345.9MiB allocated; 242ms collecting garbage
Counts
659 → 3 725
Calls

183 calls:

TimeVariablePointExpression
75.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)) (* (neg z) (/ x y)) (neg z) (/ x y) (fabs (+ (* (/ (- 1 z) y) x) (/ 4 y))) (+ (* (/ (- 1 z) y) x) (/ 4 y)) (/ (- 1 z) y) (- 1 z) 1 (fabs (- (/ (+ x 4) y) (* (/ x y) z))) (- (/ (+ x 4) y) (* (/ x y) z)) (* (- (/ (- 1 z) y) (/ -4 (* y x))) x) (- (/ (- 1 z) y) (/ -4 (* y x))) (/ -4 (* y x)) (* y x))
68.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))) (>= b 0) b 0 (/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (* 2 c) 2 c (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (neg b) (sqrt (- (* b b) (* (* 4 a) c))) (- (* b b) (* (* 4 a) c)) (* b b) (* (* 4 a) c) (* 4 a) 4 a (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (* (neg b) (+ (/ (neg c) (* b b)) (/ 1 a))) (+ (/ (neg c) (* b b)) (/ 1 a)) (/ (neg c) (* b b)) (neg c) (/ 1 a) 1 (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))) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (+ (neg b) (sqrt (- (* 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)) (+ (sqrt (+ (* (* -4 a) c) (* b b))) b) (sqrt (+ (* (* -4 a) c) (* b b))) (+ (* (* -4 a) c) (* b b)) (* -4 a) -4 -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))))) (* (- (neg (* a (/ c (* (* b b) b)))) (/ 1 b)) c) (- (neg (* a (/ c (* (* b b) b)))) (/ 1 b)) (neg (* a (/ c (* (* b b) b)))) (* a (/ c (* (* b b) b))) (/ c (* (* b b) b)) (* (* b b) b) (/ 1 b) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (+ (neg b) (sqrt (- (* b b) (* (* 4 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))) (/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (- (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))
52.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 (* (/ c a) -1)) (* (/ c a) -1) (/ c a) (* (/ (- (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 c) 2 (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (neg b) (sqrt (- (* b b) (* (* 4 a) c))) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (* 1/2 (sqrt (* (/ c a) -4))) (sqrt (* (/ c a) -4)) (* (/ c a) -4) -4 (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 (/ (+ (* -1 (sqrt (* (* a c) -1))) (* 1/2 b)) a)) (/ (+ (* -1 (sqrt (* (* a c) -1))) (* 1/2 b)) a) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (* (neg b) (+ (/ (neg c) (* b b)) (/ 1 a))) (+ (/ (neg c) (* b b)) (/ 1 a)) (/ (neg c) (* b b)) (neg c) (* b b) (/ 1 a) 1 (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) (+ (* -2 (/ (* a c) b)) (* 2 b)) (/ (* a c) b) (* a c) (* 2 b))
27.0ms
x
@0
((neg (log (- (/ 1 x) 1))) (log x) x (neg (log (- (/ 1 x) 1))) (+ (log x) x))
21.0ms
x
@-inf
((neg (log (- (/ 1 x) 1))) (log x) x (neg (log (- (/ 1 x) 1))) (+ (log x) x))

regimes864.0ms (3.9%)

Memory
-1.1MiB live, 1 184.6MiB allocated; 273ms collecting garbage
Counts
618 → 126
Calls

26 calls:

190.0ms
b
85.0ms
x
63.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))))))
58.0ms
a
50.0ms
(neg.f64 (-.f64 #s(literal 1 binary64) (*.f64 x x)))
Compiler

Compiled 746 to 786 computations (-5.4% saved)

bsearch830.0ms (3.8%)

Memory
41.1MiB live, 1 079.3MiB allocated; 208ms collecting garbage
Algorithm
63×binary-search
6×left-value
Stop Event
60×narrow-enough
3×predicate-same
Samples
381.0ms3 840×0valid
54.0ms583×0invalid
7.0ms64×2valid
Compiler

Compiled 32 960 to 28 551 computations (13.4% saved)

Precisions
Click to see histograms. Total time spent on operations: 333.0ms
ival-div!: 81.0ms (24.3% of total)
ival-mult!: 72.0ms (21.6% of total)
ival-if: 68.0ms (20.4% of total)
ival-neg: 35.0ms (10.5% of total)
ival-sqrt: 33.0ms (9.9% of total)
ival-sub!: 15.0ms (4.5% of total)
ival-add!: 10.0ms (3% of total)
ival->=: 8.0ms (2.4% of total)
ival-fabs: 7.0ms (2.1% of total)
adjust: 2.0ms (0.6% of total)
ival-exp: 1.0ms (0.3% of total)

prune531.0ms (2.4%)

Memory
-98.9MiB live, 750.8MiB allocated; 147ms collecting garbage
Counts
6 906 → 293
Compiler

Compiled 14 173 to 11 502 computations (18.8% saved)

analyze471.0ms (2.1%)

Memory
24.3MiB live, 488.4MiB allocated; 498ms 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.8MiB live, 0.8MiB allocated; 0ms collecting garbage

end0.0ms (0%)

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

Profiling

Loading profile data...