Herbie run

Date:Sunday, May 11th, 2025
Commit:32d50127 on autofix-28-1
Seed:2025131
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 806.5 MB

Time bar (total: 22.3s)

sample9.1s (40.8%)

Memory
229.5MiB live, 9 699.4MiB allocated; 5.2s collecting garbage
Samples
5.1s70 165×0valid
743.0ms4 124×2valid
155.0ms1 929×0invalid
1.0ms15×1valid
Precisions
Click to see histograms. Total time spent on operations: 3.7s
ival-mult!: 1.2s (31.8% of total)
ival-div!: 758.0ms (20.4% of total)
ival-sub!: 444.0ms (12% of total)
ival-sqrt: 443.0ms (11.9% of total)
ival-neg: 286.0ms (7.7% of total)
adjust: 146.0ms (3.9% of total)
ival-log: 128.0ms (3.4% of total)
ival-fabs: 117.0ms (3.1% of total)
ival-add!: 89.0ms (2.4% of total)
ival-exp: 70.0ms (1.9% of total)
ival->=: 47.0ms (1.3% of total)
ival-if: 4.0ms (0.1% of total)
Bogosity

rewrite5.4s (24.4%)

Memory
-23.3MiB live, 5 619.9MiB allocated; 1.3s collecting garbage
Stop Event
76×iter-limit
29×node-limit
2×unsound
1×saturated
Counts
3 536 → 7 002

derivations1.7s (7.4%)

Memory
9.4MiB live, 1 377.3MiB allocated; 241ms collecting garbage
Stop Event
5×done
4×fuel
Compiler

Compiled 920 to 579 computations (37.1% saved)

preprocess1.4s (6.2%)

Memory
-90.3MiB live, 1 408.1MiB allocated; 362ms collecting garbage
Stop Event
9×node-limit
Compiler

Compiled 1 963 to 1 537 computations (21.7% saved)

eval1.1s (5%)

Memory
235.9MiB live, 1 742.6MiB allocated; 283ms collecting garbage
Compiler

Compiled 124 095 to 39 165 computations (68.4% saved)

series1.1s (4.9%)

Memory
110.0MiB live, 1 376.5MiB allocated; 235ms collecting garbage
Counts
801 → 2 735
Calls

186 calls:

TimeVariablePointExpression
53.0ms
c
@-inf
((if (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (>= b 0) b 0 (/ (- (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)) (* b b) (* (* 4 a) c) (* 4 a) 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)))) (* (neg b) (+ (* (* a (/ c (* b b))) -2) 2)) (* (+ (* (/ b c) -2) (/ (+ a a) b)) c) (+ (* (/ b c) -2) (/ (+ a a) b)) (/ b c) -2 (/ (+ a a) b) (+ a a) (if (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (+ a a)) (/ (+ c c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (+ a a)) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (sqrt (- (* b b) (* (* 4 a) c))) (/ (+ c c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (+ c 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)))) (neg (sqrt (* (* -4 a) c))) (sqrt (* (* -4 a) c)) (* (* -4 a) c) (* -4 a) -4 (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* -2 (/ (* c a) b)) (/ (* c a) b) (* c a) (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 (sqrt (* (/ c a) -1))) (* 1/2 (/ b a))) (neg (sqrt (* (/ c a) -1))) (sqrt (* (/ c a) -1)) (* (/ c a) -1) (/ c a) -1 (* 1/2 (/ b a)) 1/2 (/ b a) (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 (* c a)) 1/2) (neg (sqrt (* (/ 1 (* c a)) -1)))) c)) (* (+ (* (/ b (* c a)) 1/2) (neg (sqrt (* (/ 1 (* c a)) -1)))) c) (+ (* (/ b (* c a)) 1/2) (neg (sqrt (* (/ 1 (* c a)) -1)))) (/ b (* c a)) (neg (sqrt (* (/ 1 (* c a)) -1))) (sqrt (* (/ 1 (* c a)) -1)) (* (/ 1 (* c a)) -1) (/ 1 (* c a)) 1 (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))
50.0ms
z
@0
((fabs (/ (+ (* (- 1 z) x) 4) y)) (/ (+ (* (- 1 z) x) 4) y) (+ (* (- 1 z) x) 4) (- 1 z) 1 z x 4 y (fabs (- (/ (+ x 4) y) (* (/ x y) z))) (- (/ (+ x 4) y) (* (/ x y) z)) (* (/ (- 1 z) y) x) (/ (- 1 z) y) (- 1 z) (fabs (- (/ (+ x 4) y) (* (/ x y) z))) (- (/ (+ x 4) y) (* (/ x y) z)) (* (/ (- 1 z) y) x) (/ (- 1 z) y) (- 1 z) (neg z) (fabs (/ (- (* x z) (+ x 4)) y)) (/ (- (* x z) (+ x 4)) y) (- (* x z) (+ x 4)) (* x z) (+ x 4) (fabs (- (/ (+ x 4) y) (* (/ x y) z))) (- (/ (+ x 4) y) (* (/ x y) z)) (* (/ (- 1 z) y) x) (/ (- 1 z) y) (- 1 z) (* (- (/ 1 z) 1) z) (- (/ 1 z) 1) (/ 1 z))
38.0ms
b
@-inf
((if (>= b 0) (/ (- (neg b) (sqrt (+ (* (* -4 a) c) (* b b)))) (+ a a)) (/ (+ c c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (>= b 0) b 0 (/ (- (neg b) (sqrt (+ (* (* -4 a) c) (* b b)))) (+ a a)) (- (neg b) (sqrt (+ (* (* -4 a) c) (* b b)))) (neg b) (sqrt (+ (* (* -4 a) c) (* b b))) (+ (* (* -4 a) c) (* b b)) (* -4 a) -4 a c (* b b) (+ a a) (/ (+ c c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (+ c c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* (neg b) (+ (* (* a (/ c (* b b))) -2) 2)) (* (+ (* (/ b c) -2) (/ (+ a a) b)) c) (+ (* (/ b c) -2) (/ (+ a a) b)) (/ b c) -2 (/ (+ a a) 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))) (- (* 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)))) (neg (sqrt (* (* -4 a) c))) (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)))) (* -2 (* c (/ a b))) (* c (/ a b)) (/ a b) (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) (+ (* (/ (* c a) b) -2) (+ b b)) (/ (* c a) b) (* c a) (+ b b) -1/2 (/ (+ 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 (* c a)) 1/2) (neg (sqrt (* (/ 1 (* c a)) -1)))) c)) (* (+ (* (/ b (* c a)) -1/2) (sqrt (/ -1 (* c a)))) c) (+ (* (/ b (* c a)) -1/2) (sqrt (/ -1 (* c a)))) (/ b (* c a)) (sqrt (/ -1 (* c a))) (/ -1 (* c a)) -1 (/ (* 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)
38.0ms
x
@0
((fabs (- (/ (+ x 4) y) (* (/ x y) z))) (- (/ (+ x 4) y) (* (/ x y) z)) (/ (+ x 4) y) (+ x 4) x 4 y (* (/ x y) z) (/ x y) z)
27.0ms
a
@inf
((if (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (>= b 0) b 0 (/ (- (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)) (* b b) (* (* 4 a) c) (* 4 a) 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)))) (* (neg b) (+ (* (* a (/ c (* b b))) -2) 2)) (* (+ (* (/ b c) -2) (/ (+ a a) b)) c) (+ (* (/ b c) -2) (/ (+ a a) b)) (/ b c) -2 (/ (+ a a) b) (+ a a) (if (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (+ a a)) (/ (+ c c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (+ a a)) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (sqrt (- (* b b) (* (* 4 a) c))) (/ (+ c c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (+ c 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)))) (neg (sqrt (* (* -4 a) c))) (sqrt (* (* -4 a) c)) (* (* -4 a) c) (* -4 a) -4 (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* -2 (/ (* c a) b)) (/ (* c a) b) (* c a) (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 (sqrt (* (/ c a) -1))) (* 1/2 (/ b a))) (neg (sqrt (* (/ c a) -1))) (sqrt (* (/ c a) -1)) (* (/ c a) -1) (/ c a) -1 (* 1/2 (/ b a)) 1/2 (/ b a) (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 (* c a)) 1/2) (neg (sqrt (* (/ 1 (* c a)) -1)))) c)) (* (+ (* (/ b (* c a)) 1/2) (neg (sqrt (* (/ 1 (* c a)) -1)))) c) (+ (* (/ b (* c a)) 1/2) (neg (sqrt (* (/ 1 (* c a)) -1)))) (/ b (* c a)) (neg (sqrt (* (/ 1 (* c a)) -1))) (sqrt (* (/ 1 (* c a)) -1)) (* (/ 1 (* c a)) -1) (/ 1 (* c a)) 1 (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))

regimes888.0ms (4%)

Memory
21.1MiB live, 1 286.7MiB allocated; 196ms collecting garbage
Counts
685 → 114
Calls

26 calls:

141.0ms
x
138.0ms
b
67.0ms
a
65.0ms
c
62.0ms
y
Compiler

Compiled 810 to 853 computations (-5.3% saved)

bsearch629.0ms (2.8%)

Memory
9.2MiB live, 891.5MiB allocated; 149ms collecting garbage
Algorithm
51×binary-search
5×left-value
Stop Event
48×narrow-enough
3×predicate-same
Samples
291.0ms3 328×0valid
56.0ms488×0invalid
9.0ms80×2valid
1.0ms16×1valid
Compiler

Compiled 25 938 to 21 984 computations (15.2% saved)

Precisions
Click to see histograms. Total time spent on operations: 257.0ms
ival-mult!: 67.0ms (26.1% of total)
ival-sqrt: 63.0ms (24.5% of total)
ival-div!: 55.0ms (21.4% of total)
ival-if: 17.0ms (6.6% of total)
ival-sub!: 14.0ms (5.5% of total)
ival-add!: 11.0ms (4.3% of total)
ival-neg: 11.0ms (4.3% of total)
ival->=: 7.0ms (2.7% of total)
ival-fabs: 7.0ms (2.7% of total)
adjust: 3.0ms (1.2% of total)
ival-exp: 2.0ms (0.8% of total)

prune528.0ms (2.4%)

Memory
-77.4MiB live, 706.6MiB allocated; 125ms collecting garbage
Counts
7 539 → 329
Compiler

Compiled 16 237 to 13 368 computations (17.7% saved)

analyze473.0ms (2.1%)

Memory
8.5MiB live, 696.8MiB allocated; 357ms 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.9MiB live, 0.8MiB allocated; 0ms collecting garbage

end0.0ms (0%)

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

Profiling

Loading profile data...