Herbie run

Date:Monday, December 2nd, 2024
Commit:a3fa83c3 on main
Hostname:nightly with Racket 8.10
Seed:2024337
Parameters:256 points for 4 iterations
Flags:
localize:costslocalize:errorsreduce:regimesreduce:binary-searchreduce:branch-expressionssetup:simplifysetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:simplifygenerate:proofs
default
Memory:49 373.8 MB

Time bar (total: 59.2s)

sample13.1s (22.2%)

Memory
221.0MiB live, 11 551.8MiB allocated
Samples
8.0s70 166×0valid
1.2s4 133×2valid
251.0ms2 006×0invalid
0.0ms1valid
Precisions
Click to see histograms. Total time spent on operations: 6.2s
ival-mult: 1.6s (25.3% of total)
ival-div: 1.4s (23% of total)
ival-sub: 792.0ms (12.8% of total)
ival-sqrt: 640.0ms (10.4% of total)
ival-if: 416.0ms (6.7% of total)
ival-add: 309.0ms (5% of total)
ival-neg: 287.0ms (4.6% of total)
ival-fabs: 183.0ms (3% of total)
ival-log: 123.0ms (2% of total)
ival->=: 109.0ms (1.8% of total)
adjust: 105.0ms (1.7% of total)
ival-exp: 81.0ms (1.3% of total)
exact: 62.0ms (1% of total)
ival-true: 58.0ms (0.9% of total)
ival-assert: 32.0ms (0.5% of total)
Bogosity

simplify11.6s (19.6%)

Memory
179.9MiB live, 9 641.1MiB allocated
Algorithm
73×egg-herbie
Stop Event
94×iter limit
53×node limit
22×saturated
Counts
2 586 → 2 559

soundness9.5s (16%)

Memory
148.1MiB live, 4 407.0MiB allocated
Stop Event
59×iter limit
39×node limit
fuel
done
saturated
Compiler

Compiled 7 627 to 3 198 computations (58.1% saved)

rewrite7.3s (12.3%)

Memory
103.4MiB live, 6 817.2MiB allocated
Stop Event
68×iter limit
30×node limit
unsound
saturated
Counts
404 → 13 775

localize4.8s (8.1%)

Memory
-74.1MiB live, 4 345.5MiB allocated
Samples
1.3s6 519×0valid
1.0s897×2valid
674.0ms649×1valid
223.0ms126×3valid
1.0ms5exit
Compiler

Compiled 7 184 to 787 computations (89% saved)

Precisions
Click to see histograms. Total time spent on operations: 2.3s
ival-div: 464.0ms (20.5% of total)
ival-mult: 424.0ms (18.7% of total)
ival-add: 294.0ms (13% of total)
adjust: 221.0ms (9.8% of total)
ival-sub: 193.0ms (8.5% of total)
ival-sqrt: 193.0ms (8.5% of total)
ival-fabs: 179.0ms (7.9% of total)
ival-neg: 120.0ms (5.3% of total)
ival-if: 98.0ms (4.3% of total)
ival-log: 28.0ms (1.2% of total)
exact: 13.0ms (0.6% of total)
ival->=: 11.0ms (0.5% of total)
ival-exp: 9.0ms (0.4% of total)
ival-true: 7.0ms (0.3% of total)
ival-pow2: 5.0ms (0.2% of total)
ival-assert: 4.0ms (0.2% of total)

eval3.8s (6.4%)

Memory
162.4MiB live, 4 441.9MiB allocated
Compiler

Compiled 841 974 to 67 283 computations (92% saved)

preprocess2.1s (3.6%)

Memory
-139.8MiB live, 1 401.3MiB allocated
Algorithm
egg-herbie
Stop Event
18×iter limit
14×saturated
node limit
Compiler

Compiled 8 193 to 1 454 computations (82.3% saved)

explain2.0s (3.5%)

Memory
89.1MiB live, 1 883.5MiB allocated
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
sqrt.f64#foflow-rescue2780
+.f64#fcancellation1390
-.f64#fcancellation1090
sqrt.f64#fuflow-rescue690
/.f64#fn/u280
/.f64#fu/n260
-.f64#fnan-rescue230
*.f64(*.f64 (/.f64 x y) z)n*o110
*.f64(*.f64 (/.f64 x y) z)n*u70
Confusion
Predicted +Predicted -
+30413
-2361751
Precision
0.562962962962963
Recall
0.9589905362776026
Confusion?
Predicted +Predicted MaybePredicted -
+304013
-23601751
Precision?
0.562962962962963
Recall?
0.9589905362776026
Freqs
test
numberfreq
01764
1402
2126
312
Total Confusion?
Predicted +Predicted MaybePredicted -
+400
-005
Precision?
1.0
Recall?
1.0
Samples
539.0ms3 640×0valid
228.0ms582×2valid
123.0ms324×1valid
26.0ms62×3valid
Compiler

Compiled 1 107 to 300 computations (72.9% saved)

Precisions
Click to see histograms. Total time spent on operations: 494.0ms
ival-div: 128.0ms (25.9% of total)
ival-sub: 109.0ms (22.1% of total)
ival-mult: 63.0ms (12.8% of total)
ival-add: 51.0ms (10.3% of total)
ival-sqrt: 39.0ms (7.9% of total)
adjust: 36.0ms (7.3% of total)
ival-neg: 17.0ms (3.4% of total)
ival-log: 11.0ms (2.2% of total)
ival-if: 10.0ms (2% of total)
ival-fabs: 9.0ms (1.8% of total)
ival-exp: 5.0ms (1% of total)
ival-true: 5.0ms (1% of total)
exact: 4.0ms (0.8% of total)
ival->=: 3.0ms (0.6% of total)
ival-assert: 2.0ms (0.4% of total)

regimes1.3s (2.1%)

Memory
-47.7MiB live, 1 065.3MiB allocated
Counts
641 → 109
Calls

26 calls:

248.0ms
(fabs.f64 (-.f64 a b))
133.0ms
b
114.0ms
a
73.0ms
(neg.f64 (log.f64 (-.f64 (/.f64 #s(literal 1 binary64) x) #s(literal 1 binary64))))
65.0ms
(-.f64 (/.f64 (+.f64 x #s(literal 4 binary64)) y) (*.f64 (/.f64 x y) z))
Compiler

Compiled 927 to 820 computations (11.5% saved)

prune1.1s (1.8%)

Memory
-276.7MiB live, 1 307.5MiB allocated
Counts
16 021 → 306
Compiler

Compiled 24 440 to 10 775 computations (55.9% saved)

series910.0ms (1.5%)

Memory
16.0MiB live, 1 025.0MiB allocated
Counts
404 → 2 586
Calls

192 calls:

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

analyze893.0ms (1.5%)

Memory
22.5MiB live, 577.8MiB allocated
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
67.2%56.9%27.7%0.1%0%15.3%0%5
74.4%62.4%21.5%0.1%0%16%0%6
78.9%64.9%17.3%0.1%0%17.7%0%7
80.8%66.3%15.8%0.1%0%17.9%0%8
85.9%69.9%11.5%0.1%0%18.5%0%9
88%70.7%9.7%0.1%0%19.6%0%10
90%72.1%8%0.1%0%19.8%0%11
92.3%73.5%6.2%0.1%0%20.3%0%12
Compiler

Compiled 153 to 106 computations (30.7% saved)

bsearch802.0ms (1.4%)

Memory
76.3MiB live, 908.2MiB allocated
Algorithm
48×binary-search
left-value
Stop Event
44×narrow-enough
predicate-same
Samples
419.0ms3 632×0valid
31.0ms276×0invalid
9.0ms64×2valid
Compiler

Compiled 31 477 to 19 606 computations (37.7% saved)

Precisions
Click to see histograms. Total time spent on operations: 296.0ms
ival-mult: 117.0ms (39.6% of total)
ival-div: 52.0ms (17.6% of total)
ival-add: 40.0ms (13.5% of total)
ival-sub: 29.0ms (9.8% of total)
ival-sqrt: 13.0ms (4.4% of total)
ival-fabs: 11.0ms (3.7% of total)
ival-if: 8.0ms (2.7% of total)
ival-neg: 8.0ms (2.7% of total)
ival->=: 5.0ms (1.7% of total)
exact: 4.0ms (1.4% of total)
ival-true: 3.0ms (1% of total)
adjust: 2.0ms (0.7% of total)
ival-exp: 2.0ms (0.7% of total)
ival-assert: 2.0ms (0.7% of total)

start0.0ms (0%)

Memory
0.5MiB live, 0.5MiB allocated

end0.0ms (0%)

Memory
0.1MiB live, 0.1MiB allocated

Profiling

Loading profile data...