Herbie run

Date:Tuesday, April 15th, 2025
Commit:5565a39e on main
Seed:2025105
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:29 601.5 MB

Time bar (total: 24.4s)

sample8.9s (36.4%)

Memory
287.1MiB live, 9 558.8MiB allocated; 4.4s collecting garbage
Samples
5.1s70 190×0valid
700.0ms4 107×2valid
199.0ms2 005×0invalid
0.0ms1valid
Precisions
Click to see histograms. Total time spent on operations: 3.3s
ival-mult!: 792.0ms (24.1% of total)
ival-div!: 588.0ms (17.9% of total)
ival-sub!: 541.0ms (16.5% of total)
ival-sqrt: 470.0ms (14.3% of total)
ival-neg: 343.0ms (10.5% of total)
adjust: 141.0ms (4.3% of total)
ival-add!: 126.0ms (3.8% of total)
ival-fabs: 100.0ms (3% of total)
ival-log: 95.0ms (2.9% of total)
ival-exp: 78.0ms (2.4% of total)
ival-if: 4.0ms (0.1% of total)
ival->=: 3.0ms (0.1% of total)
Bogosity

rewrite5.5s (22.7%)

Memory
235.0MiB live, 6 271.3MiB allocated; 1.2s collecting garbage
Stop Event
78×iter-limit
27×node-limit
unsound
saturated
Counts
4 703 → 7 685

derivations2.0s (8%)

Memory
-4.8MiB live, 1 881.5MiB allocated; 402ms collecting garbage
Stop Event
done
fuel
Compiler

Compiled 5 417 to 680 computations (87.4% saved)

explain1.6s (6.4%)

Memory
-87.4MiB live, 2 170.6MiB allocated; 416ms collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
sqrt.f64#foflow-rescue2570
+.f64#fcancellation1160
-.f64#fcancellation1071
sqrt.f64#fuflow-rescue750
/.f64#fn/u310
-.f64#fnan-rescue180
/.f64#fu/n180
*.f64(*.f64 (/.f64 x y) z)n*o120
*.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 -
+28920
-2181777
Precision
0.5700197238658777
Recall
0.9352750809061489
Confusion?
Predicted +Predicted MaybePredicted -
+289020
-21811776
Precision?
0.5688976377952756
Recall?
0.9352750809061489
Freqs
test
numberfreq
01797
1383
2117
37
Total Confusion?
Predicted +Predicted MaybePredicted -
+500
-004
Precision?
1.0
Recall?
1.0
Samples
372.0ms3 702×0valid
144.0ms562×2valid
78.0ms286×1valid
20.0ms58×3valid
Compiler

Compiled 1 107 to 300 computations (72.9% saved)

Precisions
Click to see histograms. Total time spent on operations: 312.0ms
ival-div!: 60.0ms (19.2% of total)
adjust: 58.0ms (18.6% of total)
ival-mult!: 50.0ms (16% of total)
ival-sqrt: 37.0ms (11.9% of total)
ival-sub!: 32.0ms (10.3% of total)
ival-exp: 28.0ms (9% of total)
ival-neg: 12.0ms (3.8% of total)
ival-if: 10.0ms (3.2% of total)
ival-add!: 10.0ms (3.2% of total)
ival-fabs: 6.0ms (1.9% of total)
ival-log: 6.0ms (1.9% of total)
ival->=: 4.0ms (1.3% of total)

eval1.4s (5.6%)

Memory
-37.3MiB live, 2 458.9MiB allocated; 373ms collecting garbage
Compiler

Compiled 494 354 to 42 054 computations (91.5% saved)

series1.0s (4.3%)

Memory
187.2MiB live, 1 770.9MiB allocated; 228ms collecting garbage
Counts
738 → 3 965
Calls

183 calls:

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

regimes1.0s (4.2%)

Memory
89.3MiB live, 1 682.1MiB allocated; 264ms collecting garbage
Counts
748 → 136
Calls

26 calls:

167.0ms
b
155.0ms
a
108.0ms
x
90.0ms
c
69.0ms
(-.f64 #s(literal 1 binary64) (*.f64 x x))
Compiler

Compiled 1 126 to 981 computations (12.9% saved)

bsearch1.0s (4.1%)

Memory
-42.2MiB live, 1 225.2MiB allocated; 317ms collecting garbage
Algorithm
62×binary-search
left-value
Stop Event
50×narrow-enough
12×predicate-same
Samples
405.0ms4 496×0valid
73.0ms776×0invalid
10.0ms80×2valid
2.0ms32×1valid
Compiler

Compiled 42 735 to 25 766 computations (39.7% saved)

Precisions
Click to see histograms. Total time spent on operations: 269.0ms
ival-mult!: 103.0ms (38.3% of total)
ival-div!: 49.0ms (18.2% of total)
ival-sqrt: 27.0ms (10% of total)
ival-sub!: 20.0ms (7.4% of total)
ival-neg: 18.0ms (6.7% of total)
ival-if: 16.0ms (5.9% of total)
ival->=: 14.0ms (5.2% of total)
ival-add!: 11.0ms (4.1% of total)
ival-fabs: 7.0ms (2.6% of total)
adjust: 3.0ms (1.1% of total)
ival-exp: 2.0ms (0.7% of total)

preprocess925.0ms (3.8%)

Memory
-9.8MiB live, 1 064.2MiB allocated; 264ms collecting garbage
Stop Event
node-limit
saturated
Compiler

Compiled 12 704 to 2 526 computations (80.1% saved)

prune569.0ms (2.3%)

Memory
-112.6MiB live, 922.0MiB allocated; 111ms collecting garbage
Counts
8 903 → 294
Compiler

Compiled 22 953 to 11 331 computations (50.6% saved)

analyze527.0ms (2.2%)

Memory
-51.5MiB live, 594.5MiB allocated; 172ms 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
1.1MiB live, 1.1MiB allocated; 0ms collecting garbage

end0.0ms (0%)

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

Profiling

Loading profile data...