Herbie run

Date:Tuesday, May 27th, 2025
Commit:3faf5b03 on fighting-unsoundness
Seed:2025147
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:38 758.8 MB

Time bar (total: 31.6s)

sample9.6s (30.4%)

Memory
180.4MiB live, 10 459.9MiB allocated; 5.7s collecting garbage
Samples
5.3s70 183×0valid
812.0ms4 119×2valid
143.0ms1 860×0invalid
0.0ms2×1valid
Precisions
Click to see histograms. Total time spent on operations: 3.6s
ival-mult!: 1.0s (28.2% of total)
ival-neg: 561.0ms (15.4% of total)
ival-div!: 560.0ms (15.4% of total)
ival-sqrt: 519.0ms (14.3% of total)
ival-sub!: 308.0ms (8.5% of total)
adjust: 192.0ms (5.3% of total)
ival-fabs: 159.0ms (4.4% of total)
ival-add!: 138.0ms (3.8% of total)
ival-log: 92.0ms (2.5% of total)
ival-exp: 71.0ms (2% of total)
ival-if: 4.0ms (0.1% of total)
ival->=: 3.0ms (0.1% of total)
Bogosity

rewrite8.8s (27.8%)

Memory
-1.5MiB live, 10 341.5MiB allocated; 2.0s collecting garbage
Stop Event
33×saturated
32×iter-limit
32×node-limit
Counts
729 → 31 755

eval5.0s (15.7%)

Memory
379.9MiB live, 7 851.6MiB allocated; 1.6s collecting garbage
Compiler

Compiled 410 673 to 119 682 computations (70.9% saved)

series1.7s (5.3%)

Memory
-19.3MiB live, 2 555.6MiB allocated; 345ms collecting garbage
Stop Event
32×iter-limit
Counts
729 → 2 982
Calls

189 calls:

TimeVariablePointExpression
60.0ms
c
@0
((if (>= b 0) (/ (* (+ (sqrt (+ (* (* a c) -4) (* b b))) b) -1/2) a) (/ (+ c c) (- (sqrt (+ (* (* c -4) a) (* b b))) b))) (>= b 0) b 0 (/ (* (+ (sqrt (+ (* (* a c) -4) (* b b))) b) -1/2) a) (* (+ (sqrt (+ (* (* a c) -4) (* b b))) b) -1/2) (+ (sqrt (+ (* (* a c) -4) (* b b))) b) (sqrt (+ (* (* a c) -4) (* b b))) (+ (* (* a c) -4) (* b b)) (* a c) a c -4 (* b b) -1/2 (/ (+ c c) (- (sqrt (+ (* (* c -4) a) (* b b))) b)) (+ c c) (- (sqrt (+ (* (* c -4) a) (* b b))) b) (sqrt (+ (* (* c -4) a) (* b b))) (+ (* (* c -4) a) (* b b)) (* c -4) (if (>= b 0) (* (+ (sqrt (- (* b b) (* (* 4 a) c))) b) (/ -1/2 a)) (/ (+ c c) (- (sqrt (- (* b b) (* (* 4 a) c))) b))) (* (+ (sqrt (- (* b b) (* (* 4 a) c))) b) (/ -1/2 a)) (+ (sqrt (- (* b b) (* (* 4 a) c))) b) (sqrt (- (* b b) (* (* 4 a) c))) (- (* b b) (* (* 4 a) c)) (* (* a c) -4) (/ -1/2 a) (/ (+ c c) (- (sqrt (- (* b b) (* (* 4 a) c))) b)) (- (sqrt (- (* b b) (* (* 4 a) c))) b) (if (>= b 0) (/ (- (neg b) (sqrt (fabs (- (* b b) (* (* 4 a) c))))) (* 2 a)) (/ (* 2 c) (+ (neg b) (sqrt (fabs (- (* b b) (* (* 4 a) c))))))) (/ (- (neg b) (sqrt (fabs (- (* b b) (* (* 4 a) c))))) (* 2 a)) (- (neg b) (sqrt (fabs (- (* b b) (* (* 4 a) c))))) (neg b) (sqrt (fabs (- (* b b) (* (* 4 a) c)))) (fabs (- (* b b) (* (* 4 a) c))) (* 2 a) 2 (/ (* 2 c) (+ (neg b) (sqrt (fabs (- (* b b) (* (* 4 a) c)))))) (* 2 c) (+ (neg b) (sqrt (fabs (- (* b b) (* (* 4 a) c))))) (if (>= b 0) (* (+ b (sqrt (+ (* (* c -4) a) (* b b)))) (/ -1/2 a)) (/ (+ c c) (- (sqrt (+ (* (* c -4) a) (* b b))) b))) (* (+ b (sqrt (+ (* (* c -4) a) (* b b)))) (/ -1/2 a)) (+ (* -1/2 (/ b a)) (* 1/2 (sqrt (* -4 (/ c a))))) (/ b a) (* 1/2 (sqrt (* -4 (/ c a)))) 1/2 (sqrt (* -4 (/ c a))) (* -4 (/ c a)) (/ c a) (if (>= b 0) (* (+ b (sqrt (+ (* (* c -4) a) (* b b)))) (/ -1/2 a)) (/ (+ c c) (- (sqrt (+ (* (* c -4) a) (* b b))) b))) (* (+ b (sqrt (+ (* (* c -4) a) (* b b)))) (/ -1/2 a)) (+ b (sqrt (+ (* (* c -4) a) (* b b)))) (/ (+ c c) (- (sqrt (+ (* (* c -4) a) (* b b))) b)) (/ 2 (sqrt (* -4 (/ a c)))) (sqrt (* -4 (/ a c))) (* -4 (/ a c)) (/ a c))
56.0ms
x
@-inf
((neg (log (- (/ 1 x) 1))) (log x) x (neg (log (- (/ 1 x) 1))) (- x (* -1 (log x))) (* -1 (log x)) -1 (neg (log (- (/ 1 x) 1))) (/ -1 x) (log (/ x (- 1 x))) (/ x (- 1 x)) (- 1 x) 1)
53.0ms
b
@0
((if (>= b 0) (* (+ b (sqrt (+ (* b b) (* (* a c) -4)))) (/ -1/2 a)) (/ (+ c c) (- (sqrt (+ (* b b) (* (* a c) -4))) b))) (>= b 0) b 0 (* (+ b (sqrt (+ (* b b) (* (* a c) -4)))) (/ -1/2 a)) (+ b (sqrt (+ (* b b) (* (* a c) -4)))) (sqrt (+ (* b b) (* (* a c) -4))) (+ (* b b) (* (* a c) -4)) (* (* a c) -4) (* a c) a c -4 (/ -1/2 a) -1/2 (/ (+ c c) (- (sqrt (+ (* b b) (* (* a c) -4))) b)) (+ c c) (- (sqrt (+ (* b b) (* (* a c) -4))) b) (if (>= b 0) (* (+ (sqrt (- (* b b) (* (* 4 a) c))) b) (/ -1/2 a)) (/ (+ c c) (- (sqrt (- (* b b) (* (* 4 a) c))) b))) (* (+ (sqrt (- (* b b) (* (* 4 a) c))) b) (/ -1/2 a)) (* -1/2 (/ (sqrt (neg (* 4 (* a c)))) a)) (/ (sqrt (neg (* 4 (* a c)))) a) (sqrt (neg (* 4 (* a c)))) (neg (* 4 (* a c))) (* 4 (* a c)) 4 (/ (+ c c) (- (sqrt (- (* b b) (* (* 4 a) c))) b)) (- (sqrt (- (* b b) (* (* 4 a) c))) b) (sqrt (- (* b b) (* (* 4 a) c))) (- (* b b) (* (* 4 a) c)) (if (>= b 0) (/ (+ (sqrt (- (* b b) (* (* 4 a) c))) b) (* -2 a)) (/ (+ c c) (- (sqrt (- (* b b) (* (* 4 a) c))) b))) (/ (+ (sqrt (- (* b b) (* (* 4 a) c))) b) (* -2 a)) (+ (sqrt (- (* b b) (* (* 4 a) c))) b) (sqrt (- (* b b) (* (* 4 a) c))) (- (* b b) (* (* 4 a) c)) (* (* -4 c) a) (* -4 c) (* -2 a) -2 (if (>= b 0) (* (+ b (sqrt (+ (* (* c -4) a) (* b b)))) (/ -1/2 a)) (/ (+ c c) (- (sqrt (+ (* (* c -4) a) (* b b))) b))) (* (+ b (sqrt (+ (* (* c -4) a) (* b b)))) (/ -1/2 a)) (+ (* -1/2 (/ b a)) (* 1/2 (sqrt (* -4 (/ c a))))) (/ b a) (* 1/2 (sqrt (* -4 (/ c a)))) 1/2 (sqrt (* -4 (/ c a))) (* -4 (/ c a)) (/ c a) (/ (+ c c) (- (sqrt (+ (* (* c -4) a) (* b b))) b)) (* -2 (/ c (* a (sqrt (* -4 (/ c a)))))) (/ c (* a (sqrt (* -4 (/ c a))))) (* a (sqrt (* -4 (/ 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)))))) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* -1 (* a (sqrt (* -4 (/ c a))))) -1 (* 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) (sqrt (- (* b b) (* (* 4 a) c))) (- (* b b) (* (* 4 a) c)) (* -4 (* a c)))
51.0ms
x
@0
((neg (log (- (/ 1 x) 1))) (log x) x (neg (log (- (/ 1 x) 1))) (- x (* -1 (log x))) (* -1 (log x)) -1 (neg (log (- (/ 1 x) 1))) (/ -1 x) (log (/ x (- 1 x))) (/ x (- 1 x)) (- 1 x) 1)
40.0ms
a
@-inf
((if (>= b 0) (/ (* (+ (sqrt (+ (* (* a c) -4) (* b b))) b) -1/2) a) (/ (+ c c) (- (sqrt (+ (* (* c -4) a) (* b b))) b))) (>= b 0) b 0 (/ (* (+ (sqrt (+ (* (* a c) -4) (* b b))) b) -1/2) a) (* (+ (sqrt (+ (* (* a c) -4) (* b b))) b) -1/2) (+ (sqrt (+ (* (* a c) -4) (* b b))) b) (sqrt (+ (* (* a c) -4) (* b b))) (+ (* (* a c) -4) (* b b)) (* a c) a c -4 (* b b) -1/2 (/ (+ c c) (- (sqrt (+ (* (* c -4) a) (* b b))) b)) (+ c c) (- (sqrt (+ (* (* c -4) a) (* b b))) b) (sqrt (+ (* (* c -4) a) (* b b))) (+ (* (* c -4) a) (* b b)) (* c -4) (if (>= b 0) (* (+ (sqrt (- (* b b) (* (* 4 a) c))) b) (/ -1/2 a)) (/ (+ c c) (- (sqrt (- (* b b) (* (* 4 a) c))) b))) (* (+ (sqrt (- (* b b) (* (* 4 a) c))) b) (/ -1/2 a)) (+ (sqrt (- (* b b) (* (* 4 a) c))) b) (sqrt (- (* b b) (* (* 4 a) c))) (- (* b b) (* (* 4 a) c)) (* (* a c) -4) (/ -1/2 a) (/ (+ c c) (- (sqrt (- (* b b) (* (* 4 a) c))) b)) (- (sqrt (- (* b b) (* (* 4 a) c))) b) (if (>= b 0) (/ (- (neg b) (sqrt (fabs (- (* b b) (* (* 4 a) c))))) (* 2 a)) (/ (* 2 c) (+ (neg b) (sqrt (fabs (- (* b b) (* (* 4 a) c))))))) (/ (- (neg b) (sqrt (fabs (- (* b b) (* (* 4 a) c))))) (* 2 a)) (- (neg b) (sqrt (fabs (- (* b b) (* (* 4 a) c))))) (neg b) (sqrt (fabs (- (* b b) (* (* 4 a) c)))) (fabs (- (* b b) (* (* 4 a) c))) (* 2 a) 2 (/ (* 2 c) (+ (neg b) (sqrt (fabs (- (* b b) (* (* 4 a) c)))))) (* 2 c) (+ (neg b) (sqrt (fabs (- (* b b) (* (* 4 a) c))))) (if (>= b 0) (* (+ b (sqrt (+ (* (* c -4) a) (* b b)))) (/ -1/2 a)) (/ (+ c c) (- (sqrt (+ (* (* c -4) a) (* b b))) b))) (* (+ b (sqrt (+ (* (* c -4) a) (* b b)))) (/ -1/2 a)) (+ (* -1/2 (/ b a)) (* 1/2 (sqrt (* -4 (/ c a))))) (/ b a) (* 1/2 (sqrt (* -4 (/ c a)))) 1/2 (sqrt (* -4 (/ c a))) (* -4 (/ c a)) (/ c a) (if (>= b 0) (* (+ b (sqrt (+ (* (* c -4) a) (* b b)))) (/ -1/2 a)) (/ (+ c c) (- (sqrt (+ (* (* c -4) a) (* b b))) b))) (* (+ b (sqrt (+ (* (* c -4) a) (* b b)))) (/ -1/2 a)) (+ b (sqrt (+ (* (* c -4) a) (* b b)))) (/ (+ c c) (- (sqrt (+ (* (* c -4) a) (* b b))) b)) (/ 2 (sqrt (* -4 (/ a c)))) (sqrt (* -4 (/ a c))) (* -4 (/ a c)) (/ a c))

derivations1.6s (5%)

Memory
-207.9MiB live, 1 000.8MiB allocated; 272ms collecting garbage
Stop Event
6×done
3×fuel
Compiler

Compiled 1 158 to 674 computations (41.8% saved)

preprocess1.3s (4.1%)

Memory
57.9MiB live, 1 669.9MiB allocated; 386ms collecting garbage
Stop Event
9×node-limit
1×iter-limit
Compiler

Compiled 1 931 to 1 382 computations (28.4% saved)

regimes1.3s (4%)

Memory
109.7MiB live, 1 674.9MiB allocated; 213ms collecting garbage
Counts
1 037 → 134
Calls

26 calls:

287.0ms
b
132.0ms
c
120.0ms
a
103.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))))))
98.0ms
x
Compiler

Compiled 1 267 to 1 214 computations (4.2% saved)

prune1.2s (3.8%)

Memory
35.3MiB live, 1 990.3MiB allocated; 342ms collecting garbage
Counts
33 461 → 328
Compiler

Compiled 15 542 to 12 780 computations (17.8% saved)

bsearch665.0ms (2.1%)

Memory
5.8MiB live, 726.7MiB allocated; 75ms collecting garbage
Algorithm
52×binary-search
14×left-value
Stop Event
49×narrow-enough
3×predicate-same
Samples
283.0ms2 880×0valid
63.0ms453×0invalid
10.0ms80×2valid
Compiler

Compiled 26 685 to 23 587 computations (11.6% saved)

Precisions
Click to see histograms. Total time spent on operations: 218.0ms
ival-mult!: 83.0ms (38.1% of total)
ival-sqrt: 52.0ms (23.9% of total)
ival-div!: 31.0ms (14.2% of total)
ival-sub!: 12.0ms (5.5% of total)
ival-neg: 11.0ms (5% of total)
ival-if: 10.0ms (4.6% of total)
ival->=: 7.0ms (3.2% of total)
ival-add!: 7.0ms (3.2% of total)
adjust: 3.0ms (1.4% of total)
ival-fabs: 3.0ms (1.4% of total)

analyze611.0ms (1.9%)

Memory
-87.1MiB live, 486.3MiB allocated; 605ms 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
1.2MiB live, 1.2MiB allocated; 0ms collecting garbage

end0.0ms (0%)

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

Profiling

Loading profile data...