Herbie run

Date:Tuesday, April 22nd, 2025
Commit:735e0dad on main
Seed:2025112
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:942 002.7 MB

Time bar (total: 12.9min)

sample4.6min (35.2%)

Memory
1 879.9MiB live, 331 028.1MiB allocated; 1.6min collecting garbage
Samples
2.6min2 145 153×0valid
21.5s68 992×1valid
8.0s64 180×0invalid
1.8s6 035×2valid
925.0ms1 257×5exit
521.0ms1 780×1invalid
307.0ms680×3valid
172.0ms369×4exit
4.0ms28×1exit
1.0ms4×4valid
Precisions
Click to see histograms. Total time spent on operations: 1.6min
ival-mult!: 38.1s (40.1% of total)
ival-div!: 12.1s (12.7% of total)
ival-sub!: 9.2s (9.6% of total)
ival-add!: 8.7s (9.1% of total)
ival-log: 8.1s (8.5% of total)
ival-sqrt: 4.4s (4.7% of total)
adjust: 4.2s (4.4% of total)
ival-sin: 3.6s (3.8% of total)
ival-cos: 2.8s (2.9% of total)
ival-exp: 1.9s (2% of total)
ival-acos: 841.0ms (0.9% of total)
ival-cosh: 319.0ms (0.3% of total)
ival-tan: 228.0ms (0.2% of total)
ival-fabs: 195.0ms (0.2% of total)
ival-hypot: 194.0ms (0.2% of total)
ival-sinh: 164.0ms (0.2% of total)
ival-tanh: 101.0ms (0.1% of total)
const: 0.0ms (0% of total)
Bogosity

rewrite3.1min (23.6%)

Memory
4 966.9MiB live, 193 913.3MiB allocated; 53.7s collecting garbage
Stop Event
2 193×iter-limit
836×node-limit
71×unsound
14×saturated
Counts
121 027 → 219 970

derivations1.1min (8.4%)

Memory
-1 453.3MiB live, 61 436.7MiB allocated; 14.1s collecting garbage
Stop Event
146×fuel
123×done
Compiler

Compiled 30 236 to 18 409 computations (39.1% saved)

regimes1.0min (7.8%)

Memory
-310.9MiB live, 92 736.2MiB allocated; 15.8s collecting garbage
Counts
33 119 → 4 982
Calls

512 calls:

10.0s
y
8.8s
x
6.0s
z
4.0s
t
2.9s
a
Compiler

Compiled 32 516 to 55 347 computations (-70.2% saved)

series46.5s (6%)

Memory
2 627.7MiB live, 68 683.8MiB allocated; 11.1s collecting garbage
Counts
18 352 → 102 675
Calls

8823 calls:

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

preprocess42.7s (5.5%)

Memory
-900.3MiB live, 60 100.4MiB allocated; 11.2s collecting garbage
Stop Event
174×node-limit
95×saturated
Compiler

Compiled 143 911 to 115 687 computations (19.6% saved)

eval39.2s (5.1%)

Memory
-1 125.0MiB live, 49 476.1MiB allocated; 18.7s collecting garbage
Compiler

Compiled 2 879 992 to 954 971 computations (66.8% saved)

bsearch24.5s (3.2%)

Memory
314.5MiB live, 33 737.4MiB allocated; 5.5s collecting garbage
Algorithm
1 766×binary-search
1 156×left-value
Stop Event
1 728×narrow-enough
38×predicate-same
Samples
11.2s142 599×0valid
1.3s4 531×1valid
613.0ms2 494×0invalid
23.0ms127×2valid
12.0ms60×1invalid
1.0ms7×3valid
Compiler

Compiled 647 807 to 654 405 computations (-1% saved)

Precisions
Click to see histograms. Total time spent on operations: 7.2s
ival-mult!: 3.2s (44.7% of total)
ival-sub!: 1.1s (14.8% of total)
ival-add!: 733.0ms (10.2% of total)
ival-log: 652.0ms (9.1% of total)
ival-div!: 539.0ms (7.5% of total)
ival-sin: 281.0ms (3.9% of total)
ival-cos: 222.0ms (3.1% of total)
adjust: 200.0ms (2.8% of total)
ival-exp: 116.0ms (1.6% of total)
ival-sqrt: 100.0ms (1.4% of total)
ival-fabs: 35.0ms (0.5% of total)
ival-sinh: 21.0ms (0.3% of total)
ival-tanh: 13.0ms (0.2% of total)
ival-cosh: 8.0ms (0.1% of total)

analyze22.7s (2.9%)

Memory
104.1MiB live, 21 595.4MiB allocated; 12.2s 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)

prune18.0s (2.3%)

Memory
-981.6MiB live, 29 270.4MiB allocated; 4.4s collecting garbage
Counts
214 867 → 12 522
Compiler

Compiled 485 893 to 423 710 computations (12.8% saved)

start18.0ms (0%)

Memory
18.9MiB live, 18.7MiB allocated; 11ms collecting garbage

end2.0ms (0%)

Memory
6.5MiB live, 6.2MiB allocated; 0ms collecting garbage

Profiling

Loading profile data...