Herbie run

Date:Thursday, April 3rd, 2025
Commit:f7a7cb35 on main
Seed:2025093
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:32 206.9 MB

Time bar (total: 25.1s)

sample9.4s (37.3%)

Memory
261.9MiB live, 11 498.7MiB allocated; 5.2s collecting garbage
Samples
4.4s70 141×0valid
600.0ms4 158×2valid
143.0ms1 855×0invalid
0.0ms1valid
Precisions
Click to see histograms. Total time spent on operations: 2.9s
ival-mult!: 679.0ms (23.2% of total)
ival-div!: 500.0ms (17.1% of total)
ival-sqrt: 478.0ms (16.3% of total)
ival-sub!: 388.0ms (13.2% of total)
ival-neg: 311.0ms (10.6% of total)
ival-fabs: 140.0ms (4.8% of total)
adjust: 128.0ms (4.4% of total)
ival-log: 121.0ms (4.1% of total)
ival-exp: 95.0ms (3.2% of total)
ival-add!: 82.0ms (2.8% of total)
ival-if: 4.0ms (0.1% of total)
ival->=: 3.0ms (0.1% of total)
Bogosity

rewrite6.1s (24.2%)

Memory
166.5MiB live, 6 487.2MiB allocated; 1.7s collecting garbage
Stop Event
71×iter-limit
28×node-limit
unsound
saturated
Counts
4 110 → 7 263

derivations1.9s (7.8%)

Memory
37.0MiB live, 2 181.8MiB allocated; 324ms collecting garbage
Stop Event
done
fuel
Compiler

Compiled 5 022 to 666 computations (86.7% saved)

eval1.5s (6%)

Memory
21.0MiB live, 2 481.7MiB allocated; 407ms collecting garbage
Compiler

Compiled 462 103 to 37 613 computations (91.9% saved)

explain1.3s (5.2%)

Memory
33.7MiB live, 2 143.3MiB allocated; 316ms collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
sqrt.f64#foflow-rescue2540
-.f64#fcancellation1270
+.f64#fcancellation980
sqrt.f64#fuflow-rescue670
/.f64#fn/u330
/.f64#fu/n280
*.f64(*.f64 (/.f64 x y) z)n*o140
-.f64#fnan-rescue130
*.f64(*.f64 (/.f64 x y) z)n*u30
exp.f64(exp.f64 (neg.f64 (-.f64 #s(literal 1 binary64) (*.f64 x x))))sensitivity10
Confusion
Predicted +Predicted -
+27911
-2331781
Precision
0.544921875
Recall
0.9620689655172414
Confusion?
Predicted +Predicted MaybePredicted -
+279011
-23301781
Precision?
0.544921875
Recall?
0.9620689655172414
Freqs
test
numberfreq
01792
1390
2118
34
Total Confusion?
Predicted +Predicted MaybePredicted -
+500
-004
Precision?
1.0
Recall?
1.0
Samples
203.0ms606×2valid
202.0ms3 662×0valid
93.0ms284×1valid
20.0ms56×3valid
Compiler

Compiled 1 107 to 300 computations (72.9% saved)

Precisions
Click to see histograms. Total time spent on operations: 327.0ms
adjust: 72.0ms (22% of total)
ival-sqrt: 67.0ms (20.5% of total)
ival-mult!: 61.0ms (18.7% of total)
ival-div!: 50.0ms (15.3% of total)
ival-sub!: 23.0ms (7% of total)
ival-neg: 12.0ms (3.7% of total)
ival-if: 10.0ms (3.1% of total)
ival-log: 9.0ms (2.8% of total)
ival-add!: 8.0ms (2.4% of total)
ival-fabs: 6.0ms (1.8% of total)
ival-exp: 4.0ms (1.2% of total)
ival->=: 3.0ms (0.9% of total)

regimes1.0s (4%)

Memory
-35.6MiB live, 1 802.6MiB allocated; 246ms collecting garbage
Counts
712 → 135
Calls

26 calls:

188.0ms
(*.f64 x x)
158.0ms
b
95.0ms
x
54.0ms
(exp.f64 (neg.f64 (-.f64 #s(literal 1 binary64) (*.f64 x x))))
51.0ms
a
Compiler

Compiled 1 266 to 1 049 computations (17.1% saved)

bsearch1.0s (4%)

Memory
21.8MiB live, 1 283.7MiB allocated; 184ms collecting garbage
Algorithm
61×binary-search
left-value
Stop Event
57×narrow-enough
predicate-same
Samples
370.0ms4 304×0valid
124.0ms860×0invalid
14.0ms112×2valid
1.0ms16×1valid
Compiler

Compiled 46 682 to 28 285 computations (39.4% saved)

Precisions
Click to see histograms. Total time spent on operations: 278.0ms
ival-mult!: 108.0ms (38.8% of total)
ival-div!: 47.0ms (16.9% of total)
ival-sqrt: 31.0ms (11.1% of total)
ival-sub!: 19.0ms (6.8% of total)
ival-neg: 18.0ms (6.5% of total)
ival-if: 16.0ms (5.8% of total)
ival-add!: 14.0ms (5% of total)
ival->=: 12.0ms (4.3% of total)
ival-fabs: 7.0ms (2.5% of total)
adjust: 4.0ms (1.4% of total)
ival-exp: 1.0ms (0.4% of total)

series988.0ms (3.9%)

Memory
-144.2MiB live, 1 687.6MiB allocated; 342ms collecting garbage
Counts
700 → 3 410
Calls

183 calls:

TimeVariablePointExpression
39.0ms
x
@-inf
((neg (log (- (/ 1 x) 1))) (+ (log x) x) x (neg (log (- (/ 1 x) 1))) (+ (* (+ (* 1/2 x) 1) x) (log x)) (* (* x x) 1/2) (* x x) 1/2 (neg (log (- (/ 1 x) 1))) (+ x (+ (* (* x x) 1/2) (log x))) (+ (* (* x x) 1/2) (log x)) (log x))
32.0ms
c
@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 (- (* a (/ c b)) b)) (- (* a (/ c b)) b) (* a (/ c b)) a (/ c b) (/ (+ (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))))) (/ (neg 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))) (/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (neg (sqrt (* (* a c) -4))) (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))) (if (>= b 0) (/ (* -2 c) (+ (sqrt (+ (* (* -4 a) c) (* b b))) b)) (* (/ (- (sqrt (+ (* (* -4 a) c) (* b b))) b) a) 1/2)) (/ (* -2 c) (+ (sqrt (+ (* (* -4 a) c) (* b b))) b)) (* -2 c) -2 (+ (sqrt (+ (* (* -4 a) c) (* b b))) b) (sqrt (+ (* (* -4 a) c) (* b b))) (+ (* (* -4 a) c) (* b b)) (* -4 a) (* b b) (* (/ (- (sqrt (+ (* (* -4 a) c) (* b b))) b) a) 1/2) (/ (- (sqrt (+ (* (* -4 a) c) (* b b))) b) a) (sqrt (* (/ c a) -4)) (* (/ c a) -4) (/ c 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))) (/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (+ (* (/ b a) -1/2) (sqrt (* (/ c a) -1))) (/ b a) -1/2 (sqrt (* (/ c a) -1)) (neg (sqrt (* (/ c a) -1))) (sqrt (* (/ c a) -1)) (* (/ c a) -1) -1 (/ (+ (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)
30.0ms
c
@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) (/ (* 2 c) (- (sqrt (+ (* (* -4 a) c) (* b b))) b))) (>= b 0) b 0 (* (/ (+ (sqrt (+ (* (* -4 a) c) (* b b))) b) a) -1/2) (/ (+ (* a (/ c b)) (neg b)) a) (+ (* a (/ c b)) (neg b)) a (/ c b) c (neg b) (/ (* 2 c) (- (sqrt (+ (* (* -4 a) c) (* b b))) b)) (* 2 c) 2 (- (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)) (* (sqrt (* (/ c a) -4)) -1/2) (sqrt (* (/ c a) -4)) (* (/ c a) -4) (/ c a) -1/2 (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (neg (sqrt (* (/ c a) -1))) (sqrt (* (/ c a) -1)) (* (/ c a) -1) -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 b) (sqrt (- (* b b) (* (* 4 a) c)))) (* -2 b) -2 (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) (* 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)) (+ (* (/ b a) -1/2) (sqrt (* (/ c a) -1))) (/ b a) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* -2 (/ (* a c) b)) (/ (* a c) b))
27.0ms
z
@-inf
((fabs (+ (* (/ (- 1 z) y) x) (/ 4 y))) (+ (* (/ (- 1 z) y) x) (/ 4 y)) (/ (- 1 z) y) (- 1 z) 1 z y x (/ 4 y) 4 (fabs (- (/ (+ x 4) y) (* (/ x y) z))) (- (/ (+ x 4) y) (* (/ x y) z)) (fabs (- (/ (+ x 4) y) (* (/ x y) z))) (- (/ (+ x 4) y) (* (/ x y) z)) (* (neg z) (/ x y)) (neg z) (/ x y) (fabs (/ (+ (* z x) (- -4 x)) y)) (/ (+ (* z x) (- -4 x)) y) (+ (* z x) (- -4 x)) (- -4 x) -4 (fabs (+ (* (* z x) (/ -1 y)) (/ (- x -4) y))) (+ (* (* z x) (/ -1 y)) (/ (- x -4) y)) (* z x) (/ -1 y) -1 (/ (- x -4) y) (- x -4))
27.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/2 x) 1) x) (log x)) (+ (* 1/2 x) 1) 1/2 1 (neg (log (- (/ 1 x) 1))) (log (- (/ 1 x) 1)) (- (/ 1 x) 1) (/ (- 1 x) x) (- 1 x))

preprocess988.0ms (3.9%)

Memory
-153.1MiB live, 1 050.3MiB allocated; 255ms collecting garbage
Stop Event
node-limit
saturated
Compiler

Compiled 11 962 to 2 508 computations (79% saved)

prune572.0ms (2.3%)

Memory
129.4MiB live, 1 132.1MiB allocated; 134ms collecting garbage
Counts
9 774 → 273
Compiler

Compiled 19 468 to 9 569 computations (50.8% saved)

analyze339.0ms (1.4%)

Memory
39.8MiB live, 457.0MiB allocated; 60ms collecting garbage
Algorithm
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.7MiB live, 0.7MiB allocated; 0ms collecting garbage

end0.0ms (0%)

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

Profiling

Loading profile data...