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:123 239.6 MB

Time bar (total: 2.3min)

sample1.6min (70.8%)

Memory
1 198.6MiB live, 87 688.4MiB allocated; 33.1s collecting garbage
Samples
28.1s44 910×2valid
16.2s147 082×0invalid
15.8s96 829×1valid
11.8s6 188×5exit
6.7s85 805×0valid
2.4s3 621×3valid
280.0ms4 065×0exit
219.0ms168×4exit
183.0ms1 044×1exit
3.0ms4valid
2.0ms3exit
1.0ms2exit
Precisions
Click to see histograms. Total time spent on operations: 1.1min
ival-tan: 13.1s (19.6% of total)
ival-pow: 12.2s (18.2% of total)
adjust: 7.0s (10.5% of total)
ival-mult!: 4.5s (6.8% of total)
ival-cos: 4.0s (6% of total)
ival-log: 3.6s (5.4% of total)
ival-sin: 3.4s (5.1% of total)
ival-div!: 2.9s (4.4% of total)
ival-expm1: 2.7s (4% of total)
ival-sub!: 2.5s (3.8% of total)
ival-exp: 2.1s (3.1% of total)
ival-fabs: 1.9s (2.9% of total)
ival-add!: 1.9s (2.8% of total)
ival-sqrt: 1.4s (2.1% of total)
ival-log1p: 1.2s (1.7% of total)
ival-<: 472.0ms (0.7% of total)
ival-atan: 403.0ms (0.6% of total)
ival-cbrt: 399.0ms (0.6% of total)
ival-<=: 350.0ms (0.5% of total)
ival-and: 323.0ms (0.5% of total)
ival-neg: 295.0ms (0.4% of total)
ival-fmin: 138.0ms (0.2% of total)
ival-assert: 64.0ms (0.1% of total)
ival->: 1.0ms (0% of total)
exact: 0.0ms (0% of total)
Bogosity

rewrite20.2s (14.5%)

Memory
122.5MiB live, 14 651.9MiB allocated; 3.5s collecting garbage
Stop Event
145×iter-limit
105×saturated
97×node-limit
unsound
Counts
9 315 → 23 177

derivations4.4s (3.2%)

Memory
-36.4MiB live, 3 202.8MiB allocated; 663ms collecting garbage
Stop Event
19×fuel
done
Compiler

Compiled 2 579 to 1 543 computations (40.2% saved)

preprocess4.0s (2.9%)

Memory
97.8MiB live, 3 754.6MiB allocated; 860ms collecting garbage
Stop Event
28×node-limit
Compiler

Compiled 6 285 to 4 794 computations (23.7% saved)

eval3.0s (2.1%)

Memory
404.0MiB live, 3 846.0MiB allocated; 715ms collecting garbage
Compiler

Compiled 267 934 to 104 598 computations (61% saved)

series2.7s (2%)

Memory
286.0MiB live, 3 255.7MiB allocated; 600ms collecting garbage
Counts
2 402 → 6 913
Calls

492 calls:

TimeVariablePointExpression
80.0ms
x
@inf
((- (cbrt (+ x 1)) (cbrt x)) (/ 1/3 (pow x 2/3)) 1/3 (pow x 2/3) x 2/3 (- (cbrt (+ x 1)) (cbrt x)) (cbrt (+ x 1)) 1 (cbrt x) (- (pow (- x -1) 1/3) (cbrt x)) (pow (- x -1) 1/3) (- x -1) -1 (- (cbrt (+ x 1)) (cbrt x)) (/ (+ (* (cbrt (pow x 4)) 1/3) (* -1/9 (cbrt x))) (* x x)) (+ (* (cbrt (pow x 4)) 1/3) (* -1/9 (cbrt x))) (cbrt (pow x 4)) (pow x 4) 4 (* -1/9 (cbrt x)) -1/9 (* x x) (- (cbrt (+ x 1)) (cbrt x)) (/ (+ (* -1/9 (cbrt x)) (+ (* (cbrt (pow x -5)) -10/243) (+ (* (cbrt (pow x 4)) 1/3) (/ 5/81 (pow x 2/3))))) (* x x)) (+ (* -1/9 (cbrt x)) (+ (* (cbrt (pow x -5)) -10/243) (+ (* (cbrt (pow x 4)) 1/3) (/ 5/81 (pow x 2/3))))) (+ (* (cbrt (pow x -5)) -10/243) (+ (* (cbrt (pow x 4)) 1/3) (/ 5/81 (pow x 2/3)))) (cbrt (pow x -5)) (pow x -5) -5 -10/243 (+ (* (cbrt (pow x 4)) 1/3) (/ 5/81 (pow x 2/3))) (/ 5/81 (pow x 2/3)) 5/81)
64.0ms
n
@0
((- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (log (/ (- x -1) x)) n) (log (/ (- x -1) x)) (/ (- x -1) x) (- x -1) x -1 n (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (neg (- (exp (/ (log x) n)) 1)) (- (exp (/ (log x) n)) 1) (/ (log x) n) (log x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (exp (neg (/ (neg (log x)) n))) (* n x)) (exp (neg (/ (neg (log x)) n))) (neg (/ (neg (log x)) n)) (/ (neg (log x)) n) (neg (log x)) (* n x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (+ x 1) 1 (/ 1 n) (pow x (/ 1 n)) (+ (/ (log x) n) 1) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (+ (* (exp (neg (/ (neg (log x)) n))) (/ (- (/ 1/2 (* n n)) (/ 1/2 n)) x)) (/ (exp (neg (/ (neg (log x)) n))) n)) x) (+ (* (exp (neg (/ (neg (log x)) n))) (/ (- (/ 1/2 (* n n)) (/ 1/2 n)) x)) (/ (exp (neg (/ (neg (log x)) n))) n)) (/ (- (/ 1/2 (* n n)) (/ 1/2 n)) x) (- (/ 1/2 (* n n)) (/ 1/2 n)) (/ 1/2 (* n n)) 1/2 (* n n) (/ 1/2 n) (/ (exp (neg (/ (neg (log x)) n))) n))
47.0ms
n
@-inf
((- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (neg (log (/ x (- x -1)))) n) (neg (log (/ x (- x -1)))) (log (/ x (- x -1))) (/ x (- x -1)) x (- x -1) -1 n (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (log (/ (- x -1) x)) n) (/ (/ 1 n) x) (/ 1 n) 1 (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (exp (neg (/ (neg (log x)) n))) (* n x)) (/ (+ (/ (log x) (* n x)) (/ 1 x)) n) (/ (log x) (* (* n n) x)) (log x) (* (* n n) x) (* n n) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (log (/ (- x -1) x)) n) (log (/ (- x -1) x)) (neg (/ (- (neg (/ (- (/ 1/3 x) 1/2) x)) 1) x)) (/ (- (neg (/ (- (/ 1/3 x) 1/2) x)) 1) x) (- (neg (/ (- (/ 1/3 x) 1/2) x)) 1) (neg (/ (- (/ 1/3 x) 1/2) x)) (/ (- (/ 1/3 x) 1/2) x) (- (/ 1/3 x) 1/2) (/ 1/3 x) 1/3 1/2 (- (pow (- x -1) (/ 1 n)) (pow x (/ 1 n))) (pow (- x -1) (/ 1 n)) (pow x (/ 1 n)) (- (/ (log x) n) -1) (/ (log x) n))
45.0ms
n
@-inf
((- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (log (/ (- x -1) x)) n) (log (/ (- x -1) x)) (/ (- x -1) x) (- x -1) x -1 n (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (neg (- (exp (/ (log x) n)) 1)) (- (exp (/ (log x) n)) 1) (/ (log x) n) (log x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (exp (neg (/ (neg (log x)) n))) (* n x)) (exp (neg (/ (neg (log x)) n))) (neg (/ (neg (log x)) n)) (/ (neg (log x)) n) (neg (log x)) (* n x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (+ x 1) 1 (/ 1 n) (pow x (/ 1 n)) (+ (/ (log x) n) 1) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (+ (* (exp (neg (/ (neg (log x)) n))) (/ (- (/ 1/2 (* n n)) (/ 1/2 n)) x)) (/ (exp (neg (/ (neg (log x)) n))) n)) x) (+ (* (exp (neg (/ (neg (log x)) n))) (/ (- (/ 1/2 (* n n)) (/ 1/2 n)) x)) (/ (exp (neg (/ (neg (log x)) n))) n)) (/ (- (/ 1/2 (* n n)) (/ 1/2 n)) x) (- (/ 1/2 (* n n)) (/ 1/2 n)) (/ 1/2 (* n n)) 1/2 (* n n) (/ 1/2 n) (/ (exp (neg (/ (neg (log x)) n))) n))
42.0ms
x
@-inf
((- (sqrt (+ x 1)) (sqrt x)) (/ (+ (* -1/8 (sqrt (/ 1 x))) (* 1/2 (sqrt x))) x) (/ (+ (* -1/8 (sqrt x)) (* 1/2 (sqrt (pow x 3)))) (pow x 2)) (+ (* -1/8 (sqrt x)) (* 1/2 (sqrt (pow x 3)))) (* (pow x 2) (+ (* -1/8 (sqrt (/ 1 (pow x 3)))) (* 1/2 (sqrt (/ 1 x))))) (pow x 2) x 2 (+ (* -1/8 (sqrt (/ 1 (pow x 3)))) (* 1/2 (sqrt (/ 1 x)))) -1/8 (sqrt (/ 1 (pow x 3))) (/ 1 (pow x 3)) 1 (pow x 3) 3 (* 1/2 (sqrt (/ 1 x))) 1/2 (sqrt (/ 1 x)) (/ 1 x) (- (sqrt (+ x 1)) (sqrt x)) (/ (+ (* -1/8 (sqrt (/ 1 x))) (+ (* -5/128 (sqrt (/ 1 (pow x 5)))) (+ (* 1/16 (sqrt (/ 1 (pow x 3)))) (* 1/2 (sqrt x))))) x) (+ (* -1/8 (sqrt (/ 1 (pow x 3)))) (+ (* 1/16 (sqrt (/ 1 (pow x 5)))) (* 1/2 (sqrt (/ 1 x))))) (/ (+ (* 1/16 (sqrt x)) (* x (+ (* -1/8 (sqrt x)) (* 1/2 (sqrt (pow x 3)))))) (pow x 3)) (+ (* 1/16 (sqrt x)) (* x (+ (* -1/8 (sqrt x)) (* 1/2 (sqrt (pow x 3)))))) 1/16 (sqrt x) (* x (+ (* -1/8 (sqrt x)) (* 1/2 (sqrt (pow x 3))))) (+ (* -1/8 (sqrt x)) (* 1/2 (sqrt (pow x 3)))) (* 1/2 (sqrt (pow x 3))) (sqrt (pow x 3)) (- (sqrt (+ x 1)) (sqrt x)) (/ (+ (* -1/8 (sqrt (/ 1 x))) (+ (* -5/128 (sqrt (/ 1 (pow x 5)))) (+ (* 1/16 (sqrt (/ 1 (pow x 3)))) (* 1/2 (sqrt x))))) x) (/ (+ (* -5/128 (sqrt x)) (* x (+ (* 1/16 (sqrt x)) (* x (+ (* -1/8 (sqrt x)) (* 1/2 (sqrt (pow x 3)))))))) (pow x 4)) (+ (* -5/128 (sqrt x)) (* x (+ (* 1/16 (sqrt x)) (* x (+ (* -1/8 (sqrt x)) (* 1/2 (sqrt (pow x 3)))))))) -5/128 (* x (+ (* 1/16 (sqrt x)) (* x (+ (* -1/8 (sqrt x)) (* 1/2 (sqrt (pow x 3))))))) (pow x 4) 4 (- (sqrt (+ x 1)) (sqrt x)) (/ (+ (* -1/8 (sqrt (/ 1 x))) (+ (* -5/128 (sqrt (/ 1 (pow x 5)))) (+ (* 1/16 (sqrt (/ 1 (pow x 3)))) (* 1/2 (sqrt x))))) x) (+ (* -1/8 (sqrt (/ 1 x))) (+ (* -5/128 (sqrt (/ 1 (pow x 5)))) (+ (* 1/16 (sqrt (/ 1 (pow x 3)))) (* 1/2 (sqrt x))))) (/ (+ (* -5/128 (sqrt x)) (* x (+ (* 1/16 (sqrt x)) (* x (+ (* -1/8 (sqrt x)) (* 1/2 (sqrt (pow x 3)))))))) (pow x 3)))

regimes1.9s (1.4%)

Memory
-36.1MiB live, 2 361.4MiB allocated; 392ms collecting garbage
Counts
2 115 → 278
Calls

43 calls:

569.0ms
x
151.0ms
eps
138.0ms
b
95.0ms
b_2
81.0ms
N
Compiler

Compiled 1 516 to 1 630 computations (-7.5% saved)

prune1.6s (1.1%)

Memory
-413.8MiB live, 2 001.9MiB allocated; 460ms collecting garbage
Counts
23 557 → 1 273
Compiler

Compiled 42 823 to 37 194 computations (13.1% saved)

analyze1.6s (1.1%)

Memory
177.7MiB live, 1 492.7MiB allocated; 353ms collecting garbage
Algorithm
28×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%61.1%38.9%0%0%0%0
7.4%4.5%56.6%38.9%0%0%0%1
22.3%13.6%47.5%38.9%0%0%0%2
40.2%23.5%34.9%38.9%0%2.7%0%3
53.4%31.1%27.2%38.9%0%2.8%0%4
63%36.3%21.3%38.9%0%3.6%0%5
65.9%37.5%19.4%38.9%0%4.2%0%6
70.4%38.8%16.3%38.9%0%6%0%7
73.6%40.2%14.4%38.9%0%6.5%0%8
76.3%40.9%12.7%38.9%0%7.5%0%9
78.4%41.4%11.4%38.9%0%8.3%0%10
81.1%42.4%9.9%38.9%0%8.8%0%11
82.3%42.7%9.2%38.9%0%9.3%0%12
Compiler

Compiled 483 to 337 computations (30.2% saved)

bsearch1.2s (0.8%)

Memory
39.0MiB live, 981.8MiB allocated; 147ms collecting garbage
Algorithm
92×binary-search
11×left-value
Stop Event
90×narrow-enough
predicate-same
Samples
365.0ms4 616×0valid
153.0ms482×2valid
113.0ms1 236×0invalid
96.0ms800×1valid
4.0ms46×0exit
1.0ms3valid
0.0ms1exit
Compiler

Compiled 22 108 to 23 017 computations (-4.1% saved)

Precisions
Click to see histograms. Total time spent on operations: 424.0ms
ival-mult!: 84.0ms (19.8% of total)
ival-pow: 83.0ms (19.6% of total)
ival-div!: 82.0ms (19.3% of total)
ival-sqrt: 42.0ms (9.9% of total)
adjust: 38.0ms (9% of total)
ival-neg: 32.0ms (7.5% of total)
ival-sub!: 26.0ms (6.1% of total)
ival-add!: 13.0ms (3.1% of total)
ival-cos: 10.0ms (2.4% of total)
ival-expm1: 7.0ms (1.7% of total)
ival-cbrt: 3.0ms (0.7% of total)
ival-log1p: 3.0ms (0.7% of total)
ival-log: 2.0ms (0.5% of total)

start1.0ms (0%)

Memory
2.1MiB live, 2.1MiB allocated; 0ms collecting garbage

end0.0ms (0%)

Memory
0.3MiB live, 0.3MiB allocated; 0ms collecting garbage

Profiling

Loading profile data...