Herbie run

Date:Thursday, April 24th, 2025
Commit:d5acc5eb on main
Seed:2025114
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:27 083.4 MB

Time bar (total: 21.7s)

sample8.3s (38.5%)

Memory
267.7MiB live, 9 856.7MiB allocated; 4.3s collecting garbage
Samples
4.6s70 219×0valid
696.0ms4 076×2valid
422.0ms2 066×0invalid
1.0ms9×1valid
Precisions
Click to see histograms. Total time spent on operations: 3.0s
ival-mult!: 782.0ms (26.4% of total)
ival-div!: 669.0ms (22.6% of total)
ival-sqrt: 371.0ms (12.5% of total)
ival-sub!: 290.0ms (9.8% of total)
ival-neg: 221.0ms (7.5% of total)
ival-log: 168.0ms (5.7% of total)
adjust: 160.0ms (5.4% of total)
ival-add!: 111.0ms (3.7% of total)
ival-fabs: 98.0ms (3.3% of total)
ival-exp: 85.0ms (2.9% of total)
ival-if: 4.0ms (0.1% of total)
ival->=: 3.0ms (0.1% of total)
Bogosity

rewrite5.3s (24.7%)

Memory
239.4MiB live, 5 908.1MiB allocated; 1.1s collecting garbage
Stop Event
77×iter-limit
29×node-limit
2×saturated
2×unsound
Counts
4 629 → 7 355

derivations1.7s (7.8%)

Memory
32.1MiB live, 2 031.4MiB allocated; 284ms collecting garbage
Stop Event
5×done
4×fuel
Compiler

Compiled 1 224 to 675 computations (44.9% saved)

eval1.3s (6.1%)

Memory
-163.8MiB live, 2 104.9MiB allocated; 421ms collecting garbage
Compiler

Compiled 142 343 to 39 867 computations (72% saved)

preprocess1.1s (5.3%)

Memory
-301.1MiB live, 1 558.4MiB allocated; 314ms collecting garbage
Stop Event
8×node-limit
1×saturated
Compiler

Compiled 2 307 to 1 659 computations (28.1% saved)

bsearch1.0s (4.7%)

Memory
-40.0MiB live, 1 155.5MiB allocated; 144ms collecting garbage
Algorithm
77×binary-search
7×left-value
Stop Event
70×narrow-enough
7×predicate-same
Samples
329.0ms4 112×0valid
68.0ms639×0invalid
13.0ms80×2valid
Compiler

Compiled 39 491 to 34 619 computations (12.3% saved)

Precisions
Click to see histograms. Total time spent on operations: 263.0ms
ival-mult!: 75.0ms (28.5% of total)
ival-add!: 46.0ms (17.5% of total)
ival-div!: 42.0ms (16% of total)
ival-sqrt: 26.0ms (9.9% of total)
ival-if: 19.0ms (7.2% of total)
ival-sub!: 18.0ms (6.8% of total)
ival-neg: 14.0ms (5.3% of total)
ival->=: 9.0ms (3.4% of total)
ival-fabs: 9.0ms (3.4% of total)
adjust: 3.0ms (1.1% of total)
ival-exp: 2.0ms (0.8% of total)

series997.0ms (4.6%)

Memory
192.6MiB live, 1 567.4MiB allocated; 246ms collecting garbage
Counts
709 → 3 920
Calls

186 calls:

TimeVariablePointExpression
44.0ms
b
@0
((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)))) (* -2 b) -2 (/ (+ (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) 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))))) (sqrt (* (/ c a) -1)) (* (/ c a) -1) (/ c a) -1 (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (neg (/ b a)) (/ b a) (if (>= b 0) (/ (* 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)))) (* 2 a)) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (sqrt (* (* a c) -4)) (* (* a c) -4) (* a c) -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))))) (- (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)))) (sqrt (- (* b b) (* (* 4 a) c))) (- (* b b) (* (* 4 a) c)) (* -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))) (* 2 (sqrt (* (/ a c) -1))) (sqrt (* (/ a c) -1)) (* (/ a c) -1) (/ 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))) (- (* b b) (* (* 4 a) c)) (* b b))
42.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))) (- b (* 2 (/ (* a c) b))) (* 2 (/ (* a c) b)) 2 (/ (* a c) b) (* a c) a -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))) (+ (* (* -4 a) c) (* b b)) (* -4 a) -4 (* 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))))) (sqrt (* (/ c a) -1)) (* (/ c a) -1) (/ c a) -1 (/ (+ (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) (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)))) (* -1 (sqrt (* (* a c) -4))) (sqrt (* (* a c) -4)) (* (* a c) -4) (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))) b) a) 1/2) (/ (- (sqrt (+ (* (* -4 a) c) (* b b))) b) a) (* -2 (sqrt (* (/ c 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)))) (* (- (/ (neg b) c) (sqrt (* (/ a c) -4))) c) (- (/ (neg b) c) (sqrt (* (/ a c) -4))) (* 2 (sqrt (* (/ a c) -1))) (sqrt (* (/ a c) -1)) (* (/ a c) -1) (/ 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))) (- (* b b) (* (* 4 a) c)) (* (* 4 a) c) (* 4 a) 4)
37.0ms
x
@0
((neg (log (- (/ 1 x) 1))) (log x) x (neg (log (- (/ 1 x) 1))) (+ (log x) x))
29.0ms
x
@0
((* (sqrt (- x 1)) (sqrt x)) x (* (sqrt (- x 1)) (sqrt x)) (* (- (+ (neg (/ (+ (/ 1/16 x) 1/8) (* x x))) 1) (/ 1/2 x)) x) (- (+ (neg (/ (+ (/ 1/16 x) 1/8) (* x x))) 1) (/ 1/2 x)) (+ (neg (/ (+ (/ 1/16 x) 1/8) (* x x))) 1) (neg (/ (+ (/ 1/16 x) 1/8) (* x x))) (/ (+ (/ 1/16 x) 1/8) (* x x)) (+ (/ 1/16 x) 1/8) (/ 1/16 x) 1/16 1/8 (* x x) 1 (/ 1/2 x) 1/2 (sqrt (* (- x 1) x)) (* (- x 1) x) (- x 1) (* (sqrt (- x 1)) (sqrt x)) (sqrt (- x 1)) (- x 1) (sqrt x))
26.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) (+ (* -2 (/ (* a c) b)) (+ b b)) -2 (/ (* a c) b) (* a c) a c (+ b b) -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)) (* -4 a) -4 (* 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))))) (neg (sqrt (* (/ c a) -1))) (sqrt (* (/ c a) -1)) (* (/ c a) -1) (/ c a) -1 (if (>= b 0) (/ (- (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))))) (neg (/ (+ (* 1/2 b) (sqrt (* (* a c) -1))) a)) (/ (+ (* 1/2 b) (sqrt (* (* a c) -1))) a) (+ (* 1/2 b) (sqrt (* (* a c) -1))) 1/2 (sqrt (* (* a c) -1)) (* (* a c) -1) (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) (+ (* -2 (sqrt (* (/ c a) -1))) (/ b a)) (/ b a) (if (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (/ (/ (+ (* (* c c) c) (* (* c c) c)) (+ (* c c) (- (* c c) (* c c)))) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (/ (/ (+ (* (* c c) c) (* (* c c) c)) (+ (* c c) (- (* c c) (* c c)))) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (/ (+ (* (* c c) c) (* (* c c) c)) (+ (* c c) (- (* c c) (* c c)))) (+ (* (* c c) c) (* (* c c) c)) (* c c) (* (* c c) c) (+ (* c c) (- (* c c) (* c c))) (- (* c c) (* c 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)

regimes801.0ms (3.7%)

Memory
62.2MiB live, 1 535.5MiB allocated; 134ms collecting garbage
Counts
803 → 150
Calls

26 calls:

161.0ms
b
74.0ms
a
59.0ms
x
55.0ms
c
47.0ms
y
Compiler

Compiled 905 to 943 computations (-4.2% saved)

analyze558.0ms (2.6%)

Memory
18.7MiB live, 479.1MiB allocated; 717ms 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)

prune441.0ms (2%)

Memory
15.9MiB live, 885.5MiB allocated; 55ms collecting garbage
Counts
8 629 → 312
Compiler

Compiled 14 626 to 12 094 computations (17.3% saved)

start0.0ms (0%)

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

end0.0ms (0%)

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

Profiling

Loading profile data...