Herbie run

Date:Wednesday, May 14th, 2025
Commit:79007786 on artem-rules-updates
Seed:2025134
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:962 319.6 MB

Time bar (total: 14.9min)

sample5.0min (33.8%)

Memory
4 885.7MiB live, 347 800.4MiB allocated; 1.8min collecting garbage
Samples
2.8min2 144 630×0valid
25.0s69 513×1valid
8.6s64 025×0invalid
4.2s6 031×2valid
929.0ms1 224×5exit
465.0ms1 964×1invalid
404.0ms688×3valid
229.0ms405×4exit
3.0ms26×1exit
0.0ms2×4valid
Precisions
Click to see histograms. Total time spent on operations: 1.9min
ival-mult!: 42.0s (36.4% of total)
ival-add!: 15.0s (13% of total)
ival-div!: 13.0s (11.3% of total)
ival-log: 12.0s (10.4% of total)
ival-sub!: 11.6s (10.1% of total)
ival-sqrt: 5.8s (5.1% of total)
adjust: 4.6s (4% of total)
ival-sin: 4.5s (3.9% of total)
ival-cos: 3.0s (2.6% of total)
ival-exp: 2.0s (1.8% of total)
ival-tan: 319.0ms (0.3% of total)
ival-fabs: 274.0ms (0.2% of total)
ival-acos: 261.0ms (0.2% of total)
ival-cosh: 254.0ms (0.2% of total)
ival-hypot: 250.0ms (0.2% of total)
ival-sinh: 240.0ms (0.2% of total)
ival-tanh: 87.0ms (0.1% of total)
Bogosity

rewrite3.8min (25.5%)

Memory
1 516.4MiB live, 195 536.8MiB allocated; 1.2min collecting garbage
Stop Event
1 206×iter-limit
951×saturated
834×node-limit
95×unsound
Counts
91 944 → 180 766

derivations1.2min (8.3%)

Memory
-1 915.0MiB live, 62 852.7MiB allocated; 19.2s collecting garbage
Stop Event
135×done
134×fuel
Compiler

Compiled 29 073 to 18 094 computations (37.8% saved)

regimes1.1min (7.6%)

Memory
121.6MiB live, 87 073.1MiB allocated; 23.1s collecting garbage
Counts
29 061 → 4 627
Calls

511 calls:

11.5s
x
8.8s
y
7.4s
z
3.9s
t
2.8s
a
Compiler

Compiled 32 088 to 53 886 computations (-67.9% saved)

preprocess1.1min (7.1%)

Memory
-1 357.4MiB live, 67 152.0MiB allocated; 19.0s collecting garbage
Stop Event
255×node-limit
14×saturated
Compiler

Compiled 169 402 to 138 232 computations (18.4% saved)

series51.2s (5.7%)

Memory
4 097.5MiB live, 72 351.8MiB allocated; 14.6s collecting garbage
Counts
17 757 → 74 187
Calls

8988 calls:

TimeVariablePointExpression
795.0ms
z
@-inf
((+ (* (- x 1) (log y)) (- (* (log (- 1 y)) (- z 1)) t)) (- x 1) x 1 (log y) y (- (* (log (- 1 y)) (- z 1)) t) (- (neg (log (- 1 y))) t) (neg (log (- 1 y))) (log (- 1 y)) (- 1 y) t (- (+ (* (- x 1) (log y)) (* (- z 1) (log (- 1 y)))) t) (* (log (- 1 y)) z) (* (neg y) z) (neg y) z (- (+ (* (- x 1) (log y)) (* (- z 1) (log (- 1 y)))) t) (* (log (- 1 y)) z) (* (+ (* (* z y) -1/2) (neg z)) y) (+ (* (* z y) -1/2) (neg z)) (* z y) -1/2 (neg z) (+ (* (- x 1) (log y)) (- (* (log (- 1 y)) (- z 1)) t)) (- (* (log (- 1 y)) (- z 1)) t) (neg t) (- (+ (* (- x 1) (log y)) (* (- z 1) (log (- 1 y)))) t) (* (log (- 1 y)) z) (* (+ (* (+ (* (* z y) -1/3) (* -1/2 z)) y) (neg z)) y) (+ (* (+ (* (* z y) -1/3) (* -1/2 z)) y) (neg z)) (+ (* (* z y) -1/3) (* -1/2 z)) -1/3 (* -1/2 z))
782.0ms
y
@0
((/ (* (/ x z) y) (+ (* z z) z)) (* (/ x z) y) (/ x z) x z y (+ (* z z) z) (/ (* x y) (* (* z z) (+ z 1))) (* x y) (* (* z z) (+ z 1)) (* z z) (/ (* x y) (* (* z z) (+ z 1))) (* (* y x) (/ 1 (* z z))) (* y x) (/ 1 (* z z)) 1 (* y (/ x (* (+ (* z z) z) z))) (/ x (* (+ (* z z) z) z)) (* (+ (* z z) z) z) (/ (* x (/ y (- z -1))) (* z z)) (* x (/ y (- z -1))) (/ y (- z -1)) (- z -1) -1)
433.0ms
x
@-inf
((/ (* (sin x) (sinh y)) x) (* (sin x) (sinh y)) (sin x) x (sinh y) (* (+ (* (* y y) 1/6) 1) y) (+ (* (* y y) 1/6) 1) (* y y) y 1/6 1 (* (sin x) (/ (- (/ (exp y) 2) (/ (exp (neg y)) 2)) x)) (sin x) (/ (- (/ (exp y) 2) (/ (exp (neg y)) 2)) x) (- (/ (exp y) 2) (/ (exp (neg y)) 2)) (/ (* (sin x) (sinh y)) x) (* (sin x) (sinh y)) (sin x) (* (+ (* -1/6 (* x x)) 1) x) (+ (* -1/6 (* x x)) 1) (* (* x x) -1/6) (* x x) -1/6 (sinh y) (/ (* (sin x) (sinh y)) x) (* (* 2 (sinh y)) (+ (* (* -1/12 x) x) 1/2)) (* 2 (sinh y)) (* (+ (* 1/3 (* y y)) 2) y) (+ (* 1/3 (* y y)) 2) 1/3 2 (+ (* (* -1/12 x) x) 1/2) (* -1/12 x) -1/12 1/2 (/ (* (sin x) (sinh y)) x) (* (/ (sin x) x) y) (/ (sin x) x))
245.0ms
a
@inf
((+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (+ (log y) (- (+ (* (log t) (- a 1/2)) (log z)) t)) (log y) y (- (+ (* (log t) (- a 1/2)) (log z)) t) (+ (* (log t) (- a 1/2)) (log z)) (log t) t (- a 1/2) a 1/2 (log z) z (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (* (log t) a) (+ (* (- 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 (+ x y)) (log z)) t) (+ (log (+ x y)) (log z)) (log (+ x y)) (+ x y) (* (- a 1/2) (log t)) (- a 1/2) -1/2 (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (log (* (pow t (- a 1/2)) (* y z))) t) (log (* (pow t (- a 1/2)) (* y z))) (* (pow t (- a 1/2)) (* y z)) (pow t (- a 1/2)) (* y z))
240.0ms
b
@0
((+ (* (* -9 (* z y)) t) (+ (* (* b a) 27) (+ x x))) (* -9 (* z y)) -9 (* z y) z y t (+ (* (* b a) 27) (+ x x)) (* b a) b a 27 (+ x x) x (+ (- (* x 2) (* (* (* y 9) z) t)) (* (* a 27) b)) (+ (* (* b a) 27) (+ x x)) (* (* a b) 27) (* a b) (+ (- (* x 2) (* (* (* y 9) z) t)) (* (* a 27) b)) (+ (* (* 27 b) a) (+ x x)) (* 27 b) (+ (- (* x 2) (* (* (* y 9) z) t)) (* (* a 27) b)) (+ (* (* b a) 27) (+ x x)) (* (+ (* 27 b) (/ (+ x x) a)) a) (+ (* 27 b) (/ (+ x x) a)) (/ (+ x x) a) (+ (- (* x 2) (* (* (* y 9) z) t)) (* (* a 27) b)) (+ (* (* 27 a) b) (* -9 (* (* z y) t))) (* 27 a) (* -9 (* (* z y) t)) (* (* z y) t))

eval30.6s (3.4%)

Memory
1 004.3MiB live, 45 119.1MiB allocated; 11.2s collecting garbage
Compiler

Compiled 1 937 928 to 710 941 computations (63.3% saved)

bsearch27.0s (3%)

Memory
667.9MiB live, 34 848.6MiB allocated; 6.8s collecting garbage
Algorithm
1 684×binary-search
959×left-value
Stop Event
1 659×narrow-enough
24×predicate-same
1×predicate-failed
Samples
12.7s131 221×0valid
999.0ms3 874×1valid
364.0ms2 482×0invalid
26.0ms197×2valid
11.0ms52×1invalid
3.0ms20×3valid
Compiler

Compiled 616 616 to 625 965 computations (-1.5% saved)

Precisions
Click to see histograms. Total time spent on operations: 7.9s
ival-mult!: 3.8s (47.5% of total)
ival-sub!: 1.2s (14.7% of total)
ival-add!: 1.0s (13.2% of total)
ival-div!: 593.0ms (7.5% of total)
ival-log: 449.0ms (5.7% of total)
ival-sin: 284.0ms (3.6% of total)
adjust: 216.0ms (2.7% of total)
ival-cos: 197.0ms (2.5% of total)
ival-exp: 107.0ms (1.3% of total)
ival-sqrt: 96.0ms (1.2% of total)
ival-tanh: 8.0ms (0.1% of total)
ival-cosh: 4.0ms (0.1% of total)
ival-fabs: 2.0ms (0% of total)
ival-sinh: 2.0ms (0% of total)

analyze26.3s (2.9%)

Memory
-1 182.5MiB live, 22 895.4MiB allocated; 13.9s 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)

prune23.3s (2.6%)

Memory
-1 285.4MiB live, 26 664.4MiB allocated; 11.6s collecting garbage
Counts
171 719 → 11 405
Compiler

Compiled 422 149 to 376 248 computations (10.9% saved)

start9.0ms (0%)

Memory
21.0MiB live, 20.6MiB allocated; 0ms collecting garbage

end2.0ms (0%)

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

Profiling

Loading profile data...