Herbie run

Date:Thursday, April 3rd, 2025
Commit:753370c2 on random-cleanup
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:828 857.7 MB

Time bar (total: 11.3min)

sample4.1min (36.5%)

Memory
3 443.9MiB live, 302 985.7MiB allocated; 1.2min collecting garbage
Samples
2.3min2 144 301×0valid
17.1s69 852×1valid
6.9s63 292×0invalid
1.3s6 016×2valid
887.0ms1 222×5exit
409.0ms1 839×1invalid
211.0ms401×4exit
200.0ms694×3valid
52.0ms25×1exit
0.0ms4valid
Precisions
Click to see histograms. Total time spent on operations: 1.5min
ival-mult!: 31.7s (35.7% of total)
ival-div!: 13.0s (14.6% of total)
ival-sub!: 9.3s (10.5% of total)
ival-add!: 8.6s (9.7% of total)
ival-log: 8.5s (9.6% of total)
ival-sqrt: 4.3s (4.8% of total)
adjust: 3.6s (4.1% of total)
ival-sin: 3.5s (3.9% of total)
ival-cos: 2.9s (3.3% of total)
ival-exp: 1.8s (2.1% of total)
ival-tan: 294.0ms (0.3% of total)
ival-sinh: 272.0ms (0.3% of total)
ival-cosh: 265.0ms (0.3% of total)
ival-fabs: 198.0ms (0.2% of total)
ival-acos: 189.0ms (0.2% of total)
ival-hypot: 159.0ms (0.2% of total)
ival-tanh: 89.0ms (0.1% of total)
const: 0.0ms (0% of total)
Bogosity

rewrite2.9min (26%)

Memory
4 208.7MiB live, 192 160.6MiB allocated; 45.8s collecting garbage
Stop Event
2 230×iter-limit
854×node-limit
69×unsound
12×saturated
Counts
126 091 → 226 326

regimes1.1min (9.3%)

Memory
-53.4MiB live, 87 160.3MiB allocated; 16.5s collecting garbage
Counts
33 664 → 4 891
Calls

512 calls:

10.6s
x
8.0s
y
6.1s
z
5.3s
t
2.3s
a
Compiler

Compiled 37 880 to 57 160 computations (-50.9% saved)

series48.9s (7.2%)

Memory
1 368.1MiB live, 66 753.3MiB allocated; 13.7s collecting garbage
Counts
18 942 → 107 149
Calls

8919 calls:

TimeVariablePointExpression
1.2s
x
@-inf
((* x (* (/ (pow (log x) 2) -1) (/ -1 (log x)))) x (* (/ (pow (log x) 2) -1) (/ -1 (log x))) (/ (pow (log x) 2) -1) (pow (log x) 2) (log x) 2 -1 (/ -1 (log x)) (/ (* (pow (log x) 3) x) (pow (log x) 2)) (* (pow (log x) 3) x) (pow (log x) 3) 3 (* (pow (pow (log x) 2) 3/2) (/ x (pow (log x) 2))) (pow (pow (log x) 2) 3/2) 3/2 (/ x (pow (log x) 2)) (* (pow (log x) 3) (/ x (exp (* (log (log x)) 2)))) (/ x (exp (* (log (log x)) 2))) (exp (* (log (log x)) 2)) (* (log (log x)) 2) (log (log x)) (* x (/ (pow (log x) 2) (* (pow (log x) 1/2) (pow (log x) 1/2)))) (/ (pow (log x) 2) (* (pow (log x) 1/2) (pow (log x) 1/2))) (* (pow (log x) 1/2) (pow (log x) 1/2)) (pow (log x) 1/2) 1/2)
273.0ms
z
@0
((+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (+ (+ (* (log t) (- a 1/2)) (log (+ y x))) (log z)) t) (+ (+ (* (log t) (- a 1/2)) (log (+ y x))) (log z)) (+ (* (log t) (- a 1/2)) (log (+ y x))) (log t) t (- a 1/2) a 1/2 (log (+ y x)) (+ y x) y x (log z) z (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (+ (+ (* (log t) (- a 1/2)) (neg (neg (log z)))) (log (+ y x))) t) (+ (+ (* (log t) (- a 1/2)) (neg (neg (log z)))) (log (+ y x))) (* (log t) a) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (log (* (* x z) (pow t (- a 1/2)))) t) (+ (* (log t) (- a 1/2)) (log (* z x))) (log (* z x)) (* z x) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (log (* (* (pow t (- a 1/2)) z) y)) t) (log (* (* (pow t (- a 1/2)) z) y)) (* (* (pow t (- a 1/2)) z) y) (* (pow t (- a 1/2)) z) (pow t (- a 1/2)) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (* (- (+ (* (* (neg (log t)) (/ (- a 1/2) t)) -1) (/ (log (* (+ y x) z)) t)) 1) t) (- (+ (* (* (neg (log t)) (/ (- a 1/2) t)) -1) (/ (log (* (+ y x) z)) t)) 1) (+ (* (* (neg (log t)) (/ (- a 1/2) t)) -1) (/ (log (* (+ y x) z)) t)) (* (neg (log t)) (/ (- a 1/2) t)) (neg (log t)) (/ (- a 1/2) t) -1 (/ (log (* (+ y x) z)) t) (log (* (+ y x) z)) (* (+ y x) z) 1)
244.0ms
y
@0
((* x (/ (* (log (/ x y)) (log (* y x))) (log (* y x)))) x (/ (* (log (/ x y)) (log (* y x))) (log (* y x))) (* (log (/ x y)) (log (* y x))) (log (/ x y)) (/ x y) y (log (* y x)) (* y x) (log (pow (/ x y) x)) (pow (/ x y) x) (+ (* (* (neg x) (log (neg x))) -1) (* (neg (neg (log (/ -1 y)))) x)) (* (neg x) (log (neg x))) (neg x) (log (neg x)) -1 (* (neg (neg (log (/ -1 y)))) x) (neg (neg (log (/ -1 y)))) (neg (log (/ -1 y))) (log (/ -1 y)) (/ -1 y) (* x (log (* (* (pow y -1/2) (pow x 1/2)) (* (pow y -1/2) (exp (* (log x) 1/2)))))) (log (* (* (pow y -1/2) (pow x 1/2)) (* (pow y -1/2) (exp (* (log x) 1/2))))) (* (* (pow y -1/2) (pow x 1/2)) (* (pow y -1/2) (exp (* (log x) 1/2)))) (* (pow y -1/2) (pow x 1/2)) (pow y -1/2) -1/2 (pow x 1/2) 1/2 (* (pow y -1/2) (exp (* (log x) 1/2))) (exp (* (log x) 1/2)) (* (log x) 1/2) (log x) (/ (* (+ (pow (log (neg x)) 3) (pow (log (/ -1 y)) 3)) x) (+ (* (log (neg x)) (log (* x y))) (pow (log (/ -1 y)) 2))) (* (+ (pow (log (neg x)) 3) (pow (log (/ -1 y)) 3)) x) (+ (pow (log (neg x)) 3) (pow (log (/ -1 y)) 3)) (pow (log (neg x)) 3) 3 (pow (log (/ -1 y)) 3) (+ (* (log (neg x)) (log (* x y))) (pow (log (/ -1 y)) 2)) (log (* x y)) (* x y) (pow (log (/ -1 y)) 2) 2)
143.0ms
z
@-inf
((+ x (/ (* y (+ (* (+ (* (+ (* (+ (* z 313060547623/100000000000) 55833770631/5000000000) z) t) z) a) z) b)) (+ (* (+ (* (+ (* (+ z 15234687407/1000000000) z) 314690115749/10000000000) z) 119400905721/10000000000) z) 607771387771/1000000000000))) x (/ (* y (+ (* (+ (* (+ (* (+ (* z 313060547623/100000000000) 55833770631/5000000000) z) t) z) a) z) b)) (+ (* (+ (* (+ (* (+ z 15234687407/1000000000) z) 314690115749/10000000000) z) 119400905721/10000000000) z) 607771387771/1000000000000)) (* y (+ (* (+ (* (+ (* (+ (* z 313060547623/100000000000) 55833770631/5000000000) z) t) z) a) z) b)) y (+ (* (+ (* (+ (* (+ (* z 313060547623/100000000000) 55833770631/5000000000) z) t) z) a) z) b) (* (+ (* (+ (* (+ (* z 313060547623/100000000000) 55833770631/5000000000) z) t) z) a) z) (+ (* (+ (* (+ (* z 313060547623/100000000000) 55833770631/5000000000) z) t) z) a) (* (+ (* (+ (* z 313060547623/100000000000) 55833770631/5000000000) z) t) z) (+ (* (+ (* z 313060547623/100000000000) 55833770631/5000000000) z) t) (* (+ (* z 313060547623/100000000000) 55833770631/5000000000) z) (+ (* z 313060547623/100000000000) 55833770631/5000000000) (* z 313060547623/100000000000) z 313060547623/100000000000 55833770631/5000000000 t a b (+ (* (+ (* (+ (* (+ z 15234687407/1000000000) z) 314690115749/10000000000) z) 119400905721/10000000000) z) 607771387771/1000000000000) (* (+ (* (+ (* (+ z 15234687407/1000000000) z) 314690115749/10000000000) z) 119400905721/10000000000) z) (+ (* (+ (* (+ z 15234687407/1000000000) z) 314690115749/10000000000) z) 119400905721/10000000000) (* (+ (* (+ z 15234687407/1000000000) z) 314690115749/10000000000) z) (+ (* (+ z 15234687407/1000000000) z) 314690115749/10000000000) (* (+ z 15234687407/1000000000) z) (+ z 15234687407/1000000000) 15234687407/1000000000 314690115749/10000000000 119400905721/10000000000 607771387771/1000000000000)
135.0ms
x
@-inf
((* (neg x) (log (/ y x))) (neg x) x (log (/ y x)) (/ y x) y (* x (- (log x) (log y))) (- (log x) (log y)) (log x) (log y) (+ (* (neg (log y)) x) (* (log x) x)) (neg (log y)) (* (log x) x) (* x (log (* (* (pow y -1/2) (pow x 1/2)) (* (pow y -1/2) (pow x 1/2))))) (log (* (* (pow y -1/2) (pow x 1/2)) (* (pow y -1/2) (pow x 1/2)))) (* (* (pow y -1/2) (pow x 1/2)) (* (pow y -1/2) (pow x 1/2))) (* (pow y -1/2) (pow x 1/2)) (pow y -1/2) -1/2 (pow x 1/2) 1/2 (/ (* (- (pow (log x) 3) (pow (log y) 3)) x) (+ (* (log x) (log (* x y))) (pow (log y) 2))) (* (- (pow (log x) 3) (pow (log y) 3)) x) (- (pow (log x) 3) (pow (log y) 3)) (pow (log x) 3) 3 (pow (log y) 3) (+ (* (log x) (log (* x y))) (pow (log y) 2)) (log (* x y)) (* x y) (pow (log y) 2) 2)

eval39.7s (5.8%)

Memory
-437.0MiB live, 59 221.9MiB allocated; 11.9s collecting garbage
Compiler

Compiled 9 489 328 to 1 002 106 computations (89.4% saved)

explain36.6s (5.4%)

Memory
-1 207.9MiB live, 46 009.3MiB allocated; 11.7s collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
log.f64#fsensitivity15852
/.f64#fo/n11960
sqrt.f64#foflow-rescue7500
-.f64#fcancellation5779
/.f64#fo/o5620
*.f64#fn*o5040
+.f64#fnan-rescue4610
-.f64#fnan-rescue4260
cos.f64#fsensitivity3551
+.f64#fcancellation3370
/.f64#fn/o3210
/.f64#fu/n2720
sin.f64#fsensitivity2310
*.f64#fn*u2250
/.f64#fn/u1510
cos.f64#foflow-rescue1280
/.f64#fu/u1070
tan.f64(tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))sensitivity940
log.f64#foflow-rescue820
log.f64#fuflow-rescue550
sqrt.f64#fuflow-rescue480
*.f64#fo*u340
tan.f64(tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))oflow-rescue310
(/.f64 x (*.f64 y #s(literal 2 binary64)))overflow31
sin.f64(sin.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))oflow-rescue310
(/.f64 x (*.f64 y #s(literal 2 binary64)))overflow31
exp.f64#fsensitivity305
Confusion
Predicted +Predicted -
+5967214
-176060923
Precision
0.772227255079591
Recall
0.9653777705872836
Confusion?
Predicted +Predicted MaybePredicted -
+59672212
-17601760906
Precision?
0.7705912729150529
Recall?
0.9657013428247856
Freqs
test
numberfreq
061137
16947
2715
349
412
53
61
Total Confusion?
Predicted +Predicted MaybePredicted -
+13400
-12132
Precision?
0.9781021897810219
Recall?
1.0
Samples
9.8s130 446×0valid
1.6s5 850×1valid
603.0ms1 328×2valid
28.0ms98×3valid
2.0ms4valid
Compiler

Compiled 24 442 to 8 402 computations (65.6% saved)

Precisions
Click to see histograms. Total time spent on operations: 5.6s
ival-mult!: 1.9s (34.2% of total)
ival-log: 869.0ms (15.6% of total)
ival-div!: 590.0ms (10.6% of total)
ival-add!: 539.0ms (9.7% of total)
ival-sub!: 476.0ms (8.5% of total)
adjust: 361.0ms (6.5% of total)
ival-sin: 246.0ms (4.4% of total)
ival-cos: 183.0ms (3.3% of total)
ival-sqrt: 168.0ms (3% of total)
ival-exp: 158.0ms (2.8% of total)
ival-cosh: 18.0ms (0.3% of total)
ival-tan: 15.0ms (0.3% of total)
ival-tanh: 15.0ms (0.3% of total)
ival-fabs: 12.0ms (0.2% of total)
ival-sinh: 10.0ms (0.2% of total)
ival-hypot: 9.0ms (0.2% of total)
ival-acos: 5.0ms (0.1% of total)

prune24.5s (3.6%)

Memory
-710.5MiB live, 32 808.7MiB allocated; 10.1s collecting garbage
Counts
254 577 → 12 769
Compiler

Compiled 802 168 to 442 208 computations (44.9% saved)

preprocess16.7s (2.5%)

Memory
-2 788.6MiB live, 14 591.9MiB allocated; 3.0s collecting garbage
Stop Event
174×node-limit
95×saturated
Compiler

Compiled 69 614 to 29 368 computations (57.8% saved)

analyze16.2s (2.4%)

Memory
421.6MiB live, 20 241.7MiB allocated; 5.7s collecting garbage
Algorithm
269×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%99.9%0.1%0%0%0%0
46.8%46.8%53.1%0.1%0%0%0%1
50.5%50.1%49.2%0.1%0%0.6%0%2
58.6%57%40.3%0.1%0%2.6%0%3
65.2%62.7%33.5%0.1%0%3.6%0%4
71.2%68.2%27.5%0.1%0%4.1%0%5
75.9%72.3%23%0.1%0%4.6%0%6
79.8%75.6%19.1%0.1%0%5.1%0%7
81.7%77%17.3%0.1%0%5.6%0%8
84.3%79.3%14.7%0.1%0%5.9%0%9
85.9%80.5%13.2%0.1%0%6.2%0%10
88.5%82.8%10.8%0.1%0%6.2%0%11
89.6%83.6%9.8%0.1%0%6.5%0%12
Compiler

Compiled 3 462 to 2 977 computations (14% saved)

derivations7.9s (1.2%)

Memory
-281.3MiB live, 6 441.0MiB allocated; 1.8s collecting garbage
Stop Event
49×done
25×fuel
Compiler

Compiled 12 741 to 2 235 computations (82.5% saved)

bsearch296.0ms (0%)

Memory
64.4MiB live, 460.9MiB allocated; 30ms collecting garbage
Algorithm
533×left-value
binary-search
Stop Event
narrow-enough
Compiler

Compiled 7 213 to 8 006 computations (-11% saved)

start47.0ms (0%)

Memory
-73.0MiB live, 17.0MiB allocated; 15ms collecting garbage

end2.0ms (0%)

Memory
5.7MiB live, 5.4MiB allocated; 0ms collecting garbage

Profiling

Loading profile data...