Herbie run

Date:Sunday, March 30th, 2025
Commit:2100b191 on main
Seed:2025089
Parameters:256 points for 4 iterations
Flags:
reduce:regimesreduce:binary-searchreduce:branch-expressionsreduce:simplifysetup:simplifysetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:simplifygenerate:proofs
default
Memory:1 125 331.3 MB

Time bar (total: 14.5min)

sample4.7min (32.8%)

Memory
3 503.0MiB live, 365 944.2MiB allocated; 1.6min collecting garbage
Samples
2.6min2 144 602×0valid
18.4s69 602×1valid
11.6s63 744×0invalid
1.4s5 945×2valid
772.0ms1 186×5exit
331.0ms1 818×1invalid
216.0ms714×3valid
176.0ms353×4exit
3.0ms27×1exit
0.0ms4valid
Precisions
Click to see histograms. Total time spent on operations: 1.7min
ival-mult!: 35.8s (35.3% of total)
ival-add!: 14.3s (14.1% of total)
ival-div!: 12.4s (12.3% of total)
ival-sub!: 10.9s (10.8% of total)
ival-log: 8.4s (8.2% of total)
adjust: 4.7s (4.7% of total)
ival-sqrt: 4.6s (4.6% of total)
ival-sin: 3.7s (3.6% of total)
ival-cos: 3.1s (3.1% of total)
ival-exp: 1.9s (1.9% of total)
ival-cosh: 295.0ms (0.3% of total)
ival-fabs: 273.0ms (0.3% of total)
ival-acos: 241.0ms (0.2% of total)
ival-tan: 231.0ms (0.2% of total)
ival-sinh: 209.0ms (0.2% of total)
ival-hypot: 172.0ms (0.2% of total)
ival-tanh: 94.0ms (0.1% of total)
Bogosity

rewrite3.0min (20.6%)

Memory
3 151.3MiB live, 209 970.2MiB allocated; 47.0s collecting garbage
Stop Event
2 221×iter-limit
848×node-limit
68×unsound
13×saturated
Counts
125 612 → 227 284

preprocess1.2min (8.2%)

Memory
2 325.0MiB live, 81 829.9MiB allocated; 21.0s collecting garbage
Stop Event
538×iter-limit
341×node-limit
197×saturated
Compiler

Compiled 531 682 to 136 994 computations (74.2% saved)

derivations1.1min (7.7%)

Memory
-1 104.2MiB live, 63 165.8MiB allocated; 14.4s collecting garbage
Stop Event
148×fuel
121×done
Compiler

Compiled 162 808 to 19 045 computations (88.3% saved)

regimes59.6s (6.9%)

Memory
568.0MiB live, 96 353.7MiB allocated; 12.0s collecting garbage
Counts
34 144 → 5 134
Calls

512 calls:

9.2s
x
7.6s
y
5.9s
z
3.9s
t
2.3s
a
Compiler

Compiled 37 888 to 57 635 computations (-52.1% saved)

series49.4s (5.7%)

Memory
884.6MiB live, 79 436.2MiB allocated; 12.8s collecting garbage
Counts
18 626 → 106 986
Calls

8856 calls:

TimeVariablePointExpression
303.0ms
y
@-inf
((* x (/ (- 0 (pow (log (/ y x)) 3)) (+ 0 (+ (* (log (/ y x)) (log (/ y x))) (* 0 (log (/ y x))))))) x (/ (- 0 (pow (log (/ y x)) 3)) (+ 0 (+ (* (log (/ y x)) (log (/ y x))) (* 0 (log (/ y x)))))) (- 0 (pow (log (/ y x)) 3)) 0 (pow (log (/ y x)) 3) (log (/ y x)) (/ y x) y 3 (+ 0 (+ (* (log (/ y x)) (log (/ y x))) (* 0 (log (/ y x))))) (+ (* (log (/ y x)) (log (/ y x))) (* 0 (log (/ y x)))) (* 0 (log (/ y x))) (* x (- (log (neg x)) (log (neg y)))) (- (log (neg x)) (log (neg y))) (log (neg x)) (neg x) (log (neg y)) (neg y) (+ (* (* (neg x) (log (neg x))) -1) (* (neg (neg (log (/ -1 y)))) 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) (+ (* (exp (* (log (neg (log y))) 1)) x) (* (log x) x)) (exp (* (log (neg (log y))) 1)) (* (log (neg (log y))) 1) (log (neg (log y))) (neg (log y)) (log y) 1 (* (log x) x) (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) (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)
275.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) (/ (* (- (pow (log x) 2) (pow (log y) 2)) x) (log (* x y))) (* (- (pow (log x) 2) (pow (log y) 2)) x) (- (pow (log x) 2) (pow (log y) 2)) (pow (log x) 2) 2 (pow (log y) 2) (log (* x y)) (* x y) (/ (* (- (pow (log x) 3) (pow (log y) 3)) x) (+ (* (neg (log y)) (neg (log (* y x)))) (pow (log x) 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) (+ (* (neg (log y)) (neg (log (* y x)))) (pow (log x) 2)) (neg (log (* y x))) (log (* y x)) (* y x))
250.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) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (log (* (* y z) (pow t (/ (- (* a a) 1/4) (+ a 1/2))))) t) (log (* (* y z) (pow t (/ (- (* a a) 1/4) (+ a 1/2))))) (* (* y z) (pow t (/ (- (* a a) 1/4) (+ a 1/2)))) (* y z) (pow t (/ (- (* a a) 1/4) (+ a 1/2))) (/ (- (* a a) 1/4) (+ a 1/2)) (+ (* (- a 1/2) (log t)) (- (log (* z (+ y x))) t)) (- (log (* z (+ y x))) t) (log (* z (+ y x))) (* z (+ y x)) (+ y x) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (+ (log (* z (pow t (- a 1/2)))) (log y)) t) (+ (log (* z (pow t (- a 1/2)))) (log y)) (log (* z (pow t (- a 1/2)))) (* z (pow t (- a 1/2))) (pow t (- a 1/2)) (log y))
218.0ms
t
@-inf
((+ (- (+ (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) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (log (* (* y z) (pow t (/ (- (* a a) 1/4) (+ a 1/2))))) t) (log (* (* y z) (pow t (/ (- (* a a) 1/4) (+ a 1/2))))) (* (* y z) (pow t (/ (- (* a a) 1/4) (+ a 1/2)))) (* y z) (pow t (/ (- (* a a) 1/4) (+ a 1/2))) (/ (- (* a a) 1/4) (+ a 1/2)) (+ (* (- a 1/2) (log t)) (- (log (* z (+ y x))) t)) (- (log (* z (+ y x))) t) (log (* z (+ y x))) (* z (+ y x)) (+ y x) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (+ (log (* z (pow t (- a 1/2)))) (log y)) t) (+ (log (* z (pow t (- a 1/2)))) (log y)) (log (* z (pow t (- a 1/2)))) (* z (pow t (- a 1/2))) (pow t (- a 1/2)) (log y))
182.0ms
y
@-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)) (* b (/ y (+ (* (+ (* (+ (* (+ 15234687407/1000000000 z) z) 314690115749/10000000000) z) 119400905721/10000000000) z) 607771387771/1000000000000))) b (/ y (+ (* (+ (* (+ (* (+ 15234687407/1000000000 z) z) 314690115749/10000000000) z) 119400905721/10000000000) z) 607771387771/1000000000000)) y (+ (* (+ (* (+ (* (+ 15234687407/1000000000 z) z) 314690115749/10000000000) z) 119400905721/10000000000) z) 607771387771/1000000000000) (+ (* (+ (* (+ 15234687407/1000000000 z) z) 314690115749/10000000000) z) 119400905721/10000000000) (+ (* (+ 15234687407/1000000000 z) z) 314690115749/10000000000) 314690115749/10000000000 z 119400905721/10000000000 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))) (+ (* 313060547623/100000000000 y) x) (* 313060547623/100000000000 y) 313060547623/100000000000 (+ 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)) (+ (* (+ (* (+ (* (+ z 15234687407/1000000000) z) 314690115749/10000000000) z) 119400905721/10000000000) z) 607771387771/1000000000000)) (* y (+ (* (+ (* (+ (* (+ (* z 313060547623/100000000000) 55833770631/5000000000) z) t) z) a) z) b)) (+ (* (+ (* (+ (* (+ (* z 313060547623/100000000000) 55833770631/5000000000) z) t) z) a) z) b) (* a z) a (+ (* (+ (* (+ (* (+ 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))) (/ (* b y) (+ (* (+ (* (+ (* (+ 15234687407/1000000000 z) z) 314690115749/10000000000) z) 119400905721/10000000000) z) 607771387771/1000000000000)) (* b y) (+ (* (+ (* (+ (* (+ 15234687407/1000000000 z) z) 314690115749/10000000000) z) 119400905721/10000000000) z) 607771387771/1000000000000) (+ (* (+ (* (+ 15234687407/1000000000 z) z) 314690115749/10000000000) z) 119400905721/10000000000) (+ (* (+ 15234687407/1000000000 z) z) 314690115749/10000000000) (+ 15234687407/1000000000 z) (+ 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)) (+ (* (+ (* (+ (* (+ z 15234687407/1000000000) z) 314690115749/10000000000) z) 119400905721/10000000000) z) 607771387771/1000000000000)) (/ (* (* z y) (+ (* (+ (* (+ (* 313060547623/100000000000 z) 55833770631/5000000000) z) t) z) a)) (+ (* (+ (* (+ (* (+ 15234687407/1000000000 z) z) 314690115749/10000000000) z) 119400905721/10000000000) z) 607771387771/1000000000000)) (* (* z y) (+ (* (+ (* (+ (* 313060547623/100000000000 z) 55833770631/5000000000) z) t) z) a)) (* z y) (+ (* (+ (* (+ (* 313060547623/100000000000 z) 55833770631/5000000000) z) t) z) a) (+ (* (+ (* 313060547623/100000000000 z) 55833770631/5000000000) z) t) (* (+ (* 313060547623/100000000000 z) 55833770631/5000000000) z) (+ (* 313060547623/100000000000 z) 55833770631/5000000000) 55833770631/5000000000 (+ (* (+ (* (+ (* (+ 15234687407/1000000000 z) z) 314690115749/10000000000) z) 119400905721/10000000000) z) 607771387771/1000000000000) (+ (* (+ (* (+ 15234687407/1000000000 z) z) 314690115749/10000000000) z) 119400905721/10000000000))

eval42.7s (4.9%)

Memory
604.3MiB live, 68 808.2MiB allocated; 12.7s collecting garbage
Compiler

Compiled 9 801 758 to 1 011 060 computations (89.7% saved)

explain39.7s (4.6%)

Memory
494.2MiB live, 53 730.3MiB allocated; 13.7s collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
log.f64#fsensitivity15603
/.f64#fo/n11400
sqrt.f64#foflow-rescue7850
-.f64#fcancellation61913
/.f64#fo/o5640
*.f64#fn*o4870
+.f64#fnan-rescue4820
-.f64#fnan-rescue4650
cos.f64#fsensitivity3641
/.f64#fn/o3370
+.f64#fcancellation3103
/.f64#fu/n2890
*.f64#fn*u2170
sin.f64#fsensitivity1950
/.f64#fn/u1640
cos.f64#foflow-rescue1440
/.f64#fu/u1110
tan.f64(tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))sensitivity870
log.f64#foflow-rescue810
log.f64#fuflow-rescue610
sqrt.f64#fuflow-rescue410
sin.f64(sin.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))oflow-rescue390
(/.f64 x (*.f64 y #s(literal 2 binary64)))overflow39
tan.f64(tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))oflow-rescue390
(/.f64 x (*.f64 y #s(literal 2 binary64)))overflow39
*.f64#fo*u380
exp.f64#fsensitivity272
*.f64#fu*o20
Confusion
Predicted +Predicted -
+6088183
-167260921
Precision
0.7845360824742268
Recall
0.9708180513474725
Confusion?
Predicted +Predicted MaybePredicted -
+60885178
-16722160900
Precision?
0.7825584382224505
Recall?
0.9716153723489077
Freqs
test
numberfreq
061104
16974
2707
361
415
51
62
Total Confusion?
Predicted +Predicted MaybePredicted -
+13620
-02129
Precision?
0.9857142857142858
Recall?
1.0
Samples
13.5s130 340×0valid
1.7s5 990×1valid
512.0ms1 258×2valid
45.0ms138×3valid
1.0ms4valid
Compiler

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

Precisions
Click to see histograms. Total time spent on operations: 8.4s
ival-div!: 3.6s (43.2% of total)
ival-mult!: 1.7s (20.8% of total)
ival-log: 737.0ms (8.8% of total)
ival-sub!: 624.0ms (7.4% of total)
ival-add!: 495.0ms (5.9% of total)
adjust: 317.0ms (3.8% of total)
ival-sin: 315.0ms (3.7% of total)
ival-cos: 192.0ms (2.3% of total)
ival-sqrt: 182.0ms (2.2% of total)
ival-exp: 89.0ms (1.1% of total)
ival-tan: 17.0ms (0.2% of total)
ival-cosh: 13.0ms (0.2% of total)
ival-fabs: 12.0ms (0.1% of total)
ival-sinh: 11.0ms (0.1% of total)
ival-tanh: 9.0ms (0.1% of total)
ival-hypot: 9.0ms (0.1% of total)
ival-acos: 8.0ms (0.1% of total)
const: 0.0ms (0% of total)

prune29.9s (3.4%)

Memory
-1 052.9MiB live, 42 251.2MiB allocated; 15.0s collecting garbage
Counts
254 419 → 12 388
Compiler

Compiled 786 236 to 429 071 computations (45.4% saved)

bsearch27.0s (3.1%)

Memory
264.2MiB live, 41 315.5MiB allocated; 5.5s collecting garbage
Algorithm
1 875×binary-search
1 107×left-value
Stop Event
1 842×narrow-enough
33×predicate-same
Samples
12.8s147 585×0valid
1.0s4 739×1valid
179.0ms2 724×0invalid
21.0ms132×2valid
14.0ms24×3valid
9.0ms42×1invalid
Compiler

Compiled 1 044 815 to 749 449 computations (28.3% saved)

Precisions
Click to see histograms. Total time spent on operations: 8.2s
ival-mult!: 4.0s (49% of total)
ival-sub!: 1.1s (13.7% of total)
ival-add!: 676.0ms (8.3% of total)
ival-div!: 637.0ms (7.8% of total)
ival-log: 566.0ms (6.9% of total)
ival-sin: 369.0ms (4.5% of total)
adjust: 237.0ms (2.9% of total)
ival-cos: 232.0ms (2.8% of total)
ival-exp: 157.0ms (1.9% of total)
ival-sqrt: 107.0ms (1.3% of total)
ival-cosh: 43.0ms (0.5% of total)
ival-sinh: 16.0ms (0.2% of total)
ival-tanh: 7.0ms (0.1% of total)
ival-fabs: 5.0ms (0.1% of total)

analyze18.6s (2.1%)

Memory
234.6MiB live, 22 501.3MiB allocated; 7.5s 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)

start46.0ms (0%)

Memory
-89.8MiB live, 20.0MiB allocated; 40ms collecting garbage

end2.0ms (0%)

Memory
5.0MiB live, 4.9MiB allocated; 0ms collecting garbage

Profiling

Loading profile data...