Herbie run

Date:Thursday, May 22nd, 2025
Commit:089dffb0 on main
Seed:2025142
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:1 022 744.3 MB

Time bar (total: 14.3min)

sample4.8min (33.8%)

Memory
4 286.8MiB live, 350 546.5MiB allocated; 1.9min collecting garbage
Samples
2.8min2 144 318×0valid
20.5s69 630×1valid
8.4s64 753×0invalid
1.8s6 225×2valid
775.0ms1 204×5exit
406.0ms1 775×1invalid
303.0ms689×3valid
237.0ms378×4exit
2.0ms21×1exit
0.0ms2×4valid
Precisions
Click to see histograms. Total time spent on operations: 1.7min
ival-mult!: 36.8s (35.4% of total)
ival-div!: 14.9s (14.3% of total)
ival-sub!: 11.0s (10.6% of total)
ival-add!: 10.0s (9.6% of total)
ival-log: 9.0s (8.7% of total)
ival-sqrt: 5.7s (5.5% of total)
ival-sin: 4.9s (4.7% of total)
adjust: 4.6s (4.4% of total)
ival-cos: 3.5s (3.3% of total)
ival-exp: 2.4s (2.3% of total)
ival-tan: 264.0ms (0.3% of total)
ival-sinh: 241.0ms (0.2% of total)
ival-fabs: 231.0ms (0.2% of total)
ival-cosh: 218.0ms (0.2% of total)
ival-acos: 182.0ms (0.2% of total)
ival-hypot: 168.0ms (0.2% of total)
ival-tanh: 104.0ms (0.1% of total)
const: 0.0ms (0% of total)
Bogosity

rewrite3.4min (24.1%)

Memory
2 838.0MiB live, 217 833.8MiB allocated; 1.3min collecting garbage
Stop Event
2 245×iter-limit
873×node-limit
69×unsound
18×saturated
Counts
99 880 → 212 782

derivations1.2min (8.2%)

Memory
-573.4MiB live, 67 508.7MiB allocated; 17.9s collecting garbage
Stop Event
155×fuel
114×done
Compiler

Compiled 152 842 to 18 566 computations (87.9% saved)

regimes1.2min (8.2%)

Memory
-134.1MiB live, 93 584.4MiB allocated; 27.3s collecting garbage
Counts
29 029 → 4 723
Calls

512 calls:

9.2s
y
8.7s
x
6.6s
t
6.1s
z
4.3s
a
Compiler

Compiled 36 563 to 54 946 computations (-50.3% saved)

preprocess59.2s (6.9%)

Memory
-2 932.3MiB live, 65 803.1MiB allocated; 22.1s collecting garbage
Stop Event
237×node-limit
32×saturated
Compiler

Compiled 358 388 to 113 746 computations (68.3% saved)

series51.7s (6%)

Memory
4 724.7MiB live, 78 956.1MiB allocated; 16.0s collecting garbage
Counts
19 106 → 80 774
Calls

9078 calls:

TimeVariablePointExpression
370.0ms
a
@-inf
((+ (- (+ (+ x y) z) (* z (log t))) (* (- a 1/2) b)) (+ y (- (+ (* (- a 1/2) b) z) (* (log t) z))) y (- (+ (* (- a 1/2) b) z) (* (log t) z)) (+ (* (- a 1/2) b) z) (- a 1/2) a 1/2 b z (* (log t) z) (log t) t (+ (- (+ (+ x y) z) (* z (log t))) (* (- a 1/2) b)) (* b a) (+ (- (+ (+ x y) z) (* z (log t))) (* (- a 1/2) b)) (* (- 1 (log t)) z) (- 1 (log t)) 1 (+ (- (+ (+ x y) z) (* z (log t))) (* (- a 1/2) b)) (- (+ (+ (+ (* -1/2 b) z) y) x) (* (log t) z)) (+ (+ (+ (* -1/2 b) z) y) x) (+ (+ (* -1/2 b) z) y) (+ (* -1/2 b) z) -1/2 x (+ (/ (- (pow (+ (+ y x) z) 3) (pow (* (log t) z) 3)) (+ (* (+ (+ y x) z) (+ (+ y x) z)) (+ (* (* (log t) z) (* (log t) z)) (* (+ (+ y x) z) (* (log t) z))))) (* (- a 1/2) b)) (/ (- (pow (+ (+ y x) z) 3) (pow (* (log t) z) 3)) (+ (* (+ (+ y x) z) (+ (+ y x) z)) (+ (* (* (log t) z) (* (log t) z)) (* (+ (+ y x) z) (* (log t) z))))) (- (pow (+ (+ y x) z) 3) (pow (* (log t) z) 3)) (pow (+ (+ y x) z) 3) (+ (+ y x) z) (+ y x) 3 (pow (* (log t) z) 3) (+ (* (+ (+ y x) z) (+ (+ y x) z)) (+ (* (* (log t) z) (* (log t) z)) (* (+ (+ y x) z) (* (log t) z)))) (+ (* (* (log t) z) (* (log t) z)) (* (+ (+ y x) z) (* (log t) z))) (* (+ (+ y x) z) (* (log t) z)) (* (- a 1/2) b))
199.0ms
x
@-inf
((+ (* (log x) x) (* (neg (log y)) x)) (log x) x (* (neg (log y)) x) (neg (log y)) (log y) y (* x (- (log (neg x)) (log (neg y)))) (- (log (neg x)) (log (neg y))) (log (neg x)) (neg x) (log (neg y)) (neg y) (* (* (log (/ x y)) (log (* y x))) (/ x (log (* y x)))) (* (log (/ x y)) (log (* y x))) (log (/ x y)) (/ x y) (log (* y x)) (* y x) (/ x (log (* y x))) (/ (* (* (log (/ x y)) x) (* x (log (* x y)))) (* x (log (* x y)))) (* (* (log (/ x y)) x) (* x (log (* x y)))) (* (log (/ x y)) x) (* x (log (* x y))) (log (* x y)) (* x y) (* x (/ (- (* (* (log (* -1 y)) (neg (log (neg y)))) (log (neg x))) (* (log (* -1 y)) (* (log (neg x)) (neg (log (neg x)))))) (* (log (* -1 y)) (log (neg x))))) (/ (- (* (* (log (* -1 y)) (neg (log (neg y)))) (log (neg x))) (* (log (* -1 y)) (* (log (neg x)) (neg (log (neg x)))))) (* (log (* -1 y)) (log (neg x)))) (- (* (* (log (* -1 y)) (neg (log (neg y)))) (log (neg x))) (* (log (* -1 y)) (* (log (neg x)) (neg (log (neg x)))))) (* (* (log (* -1 y)) (neg (log (neg y)))) (log (neg x))) (* (log (* -1 y)) (neg (log (neg y)))) (log (* -1 y)) (* -1 y) -1 (neg (log (neg y))) (* (log (* -1 y)) (* (log (neg x)) (neg (log (neg x))))) (* (log (neg x)) (neg (log (neg x)))) (neg (log (neg x))) (* (log (* -1 y)) (log (neg x))))
182.0ms
y
@-inf
((* x (- (log x) (log y))) x (- (log x) (log y)) (log x) (log y) y (* (neg x) (log (/ y x))) (neg x) (log (/ y x)) (/ y x) (- (* (log (neg x)) x) (* (log (neg y)) x)) (* (log (neg x)) x) (log (neg x)) (* (log (neg y)) x) (log (neg y)) (neg y) (* x (/ (- (* (log (* (/ -1 y) -1)) (log (* (/ -1 y) -1))) (* (log x) (log x))) (- (log (* (/ -1 y) -1)) (log x)))) (/ (- (* (log (* (/ -1 y) -1)) (log (* (/ -1 y) -1))) (* (log x) (log x))) (- (log (* (/ -1 y) -1)) (log x))) (- (* (log (* (/ -1 y) -1)) (log (* (/ -1 y) -1))) (* (log x) (log x))) (* (log (* (/ -1 y) -1)) (log (* (/ -1 y) -1))) (log (* (/ -1 y) -1)) (* (/ -1 y) -1) (/ -1 y) -1 (* (log x) (log x)) (- (log (* (/ -1 y) -1)) (log x)) (/ (* (- (pow (log x) 3) (pow (log y) 3)) x) (+ (* (log y) (log (* y x))) (* (log x) (log x)))) (* (- (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 y) (log (* y x))) (* (log x) (log x))) (log (* y x)) (* y x))
182.0ms
z
@inf
((+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (+ (log (+ x y)) (log z)) t) (+ (log (+ x y)) (log z)) (log (+ x y)) (+ x y) x y (log z) z t (* (- a 1/2) (log t)) (- a 1/2) (* (- 1 (/ 1/2 a)) a) (- 1 (/ 1/2 a)) 1 (/ 1/2 a) 1/2 a (log t) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (neg t) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (+ (log (* z (+ y x))) (* -1/2 (log t))) t) (+ (log (* z (+ y x))) (* -1/2 (log t))) (log (* z (+ y x))) (* z (+ y x)) (+ y x) (* -1/2 (log t)) -1/2 (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (+ (log (+ x y)) (log z)) t) (+ (log (+ x y)) (log z)) (log (+ x y)) (+ x y) (* (- a 1/2) (log t)) (- a 1/2) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (* (+ (log t) (- (+ (* (/ (log t) a) -1/2) (/ (log (* z (+ y x))) a)) (/ t a))) a) (+ (log t) (- (+ (* (/ (log t) a) -1/2) (/ (log (* z (+ y x))) a)) (/ t a))) (- (+ (* (/ (log t) a) -1/2) (/ (log (* z (+ y x))) a)) (/ t a)) (+ (* (/ (log t) a) -1/2) (/ (log (* z (+ y x))) a)) (/ (log t) a) (/ (log (* z (+ y x))) a) (/ t a))
170.0ms
z
@inf
((- x (/ (log (+ (- 1 y) (* y (exp z)))) t)) x (/ (log (+ (- 1 y) (* y (exp z)))) t) (log (+ (- 1 y) (* y (exp z)))) (* (- (exp z) 1) y) (- (exp z) 1) z y t (- x (/ (log (+ (- 1 y) (* y (exp z)))) t)) (/ (log (+ (- 1 y) (* y (exp z)))) t) (log (+ (- 1 y) (* y (exp z)))) (* z y) (- x (/ (log (+ (- 1 y) (* y (exp z)))) t)) (/ (log (+ (- 1 y) (* y (exp z)))) t) (log (+ (- 1 y) (* y (exp z)))) (log (* (- (exp z) 1) y)) (- x (/ (log (+ (- 1 y) (* y (exp z)))) t)) (+ (* (- (* (/ (* (+ (neg (* y y)) y) z) t) -1/2) (/ y t)) z) x) (- (* (/ (* (+ (neg (* y y)) y) z) t) -1/2) (/ y t)) (* (/ (* (+ (neg (* y y)) y) z) t) -1/2) (/ (* (+ (neg (* y y)) y) z) t) (* (+ (neg (* y y)) y) z) (+ (neg (* y y)) y) (neg (* y y)) (* y y) -1/2 (/ y t) (- x (/ (- (log (- (* (- 1 y) (- 1 y)) (pow (* (exp z) y) 2))) (log (- (- 1 y) (* (exp z) y)))) t)) (/ (- (log (- (* (- 1 y) (- 1 y)) (pow (* (exp z) y) 2))) (log (- (- 1 y) (* (exp z) y)))) t) (- (log (- (* (- 1 y) (- 1 y)) (pow (* (exp z) y) 2))) (log (- (- 1 y) (* (exp z) y)))) (log (- (* (- 1 y) (- 1 y)) (pow (* (exp z) y) 2))) (- (* (- 1 y) (- 1 y)) (pow (* (exp z) y) 2)) (* (- 1 y) (- 1 y)) (- 1 y) 1 (pow (* (exp z) y) 2) (* (exp z) y) (exp z) 2 (log (- (- 1 y) (* (exp z) y))) (- (- 1 y) (* (exp z) y)))

eval39.3s (4.6%)

Memory
-46.9MiB live, 56 218.6MiB allocated; 17.0s collecting garbage
Compiler

Compiled 8 100 587 to 957 261 computations (88.2% saved)

bsearch27.6s (3.2%)

Memory
264.0MiB live, 37 076.2MiB allocated; 9.6s collecting garbage
Algorithm
1 682×binary-search
1 062×left-value
Stop Event
1 659×narrow-enough
23×predicate-same
Samples
13.9s135 706×0valid
995.0ms3 678×1valid
224.0ms2 749×0invalid
27.0ms105×1invalid
25.0ms151×2valid
3.0ms17×3valid
Compiler

Compiled 941 170 to 669 803 computations (28.8% saved)

Precisions
Click to see histograms. Total time spent on operations: 7.6s
ival-mult!: 3.2s (41.7% of total)
ival-sub!: 1.3s (17% of total)
ival-add!: 773.0ms (10.2% of total)
ival-div!: 599.0ms (7.9% of total)
ival-log: 479.0ms (6.3% of total)
ival-cos: 382.0ms (5% of total)
ival-exp: 304.0ms (4% of total)
ival-sin: 302.0ms (4% of total)
adjust: 171.0ms (2.3% of total)
ival-sqrt: 75.0ms (1% of total)
ival-fabs: 28.0ms (0.4% of total)
ival-tanh: 9.0ms (0.1% of total)
ival-cosh: 4.0ms (0.1% of total)
ival-sinh: 1.0ms (0% of total)

prune25.8s (3%)

Memory
-1 743.6MiB live, 33 071.3MiB allocated; 13.6s collecting garbage
Counts
206 190 → 12 420
Compiler

Compiled 791 926 to 430 821 computations (45.6% saved)

analyze16.4s (1.9%)

Memory
-41.9MiB live, 22 117.7MiB allocated; 5.4s 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)

start9.0ms (0%)

Memory
22.5MiB live, 22.4MiB allocated; 0ms collecting garbage

end2.0ms (0%)

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

Profiling

Loading profile data...