Herbie run

Date:Saturday, May 31st, 2025
Commit:a88f6b81 on fighting-unsoundness
Seed:2025151
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:202 430.3 MB

Time bar (total: 3.0min)

sample1.7min (55.4%)

Memory
1 387.6MiB live, 105 422.7MiB allocated; 38.8s collecting garbage
Samples
28.3s44 588×2valid
18.5s96 942×1valid
14.2s146 476×0invalid
10.9s6 013×5exit
7.6s86 054×0valid
2.8s3 580×3valid
388.0ms4 256×0exit
156.0ms1 137×1exit
153.0ms146×4exit
4.0ms4×4valid
2.0ms1×3exit
Precisions
Click to see histograms. Total time spent on operations: 1.1min
ival-tan: 13.6s (20% of total)
ival-pow: 10.8s (15.9% of total)
adjust: 8.6s (12.7% of total)
ival-cos: 4.5s (6.7% of total)
ival-log: 4.2s (6.2% of total)
ival-mult!: 3.8s (5.7% of total)
ival-sin: 3.4s (5% of total)
ival-div!: 3.3s (4.9% of total)
ival-exp: 2.4s (3.5% of total)
ival-expm1: 2.3s (3.5% of total)
ival-sub!: 2.1s (3.1% of total)
ival-add!: 1.9s (2.8% of total)
ival-fabs: 1.8s (2.7% of total)
ival-sqrt: 1.2s (1.7% of total)
ival-log1p: 1.1s (1.7% of total)
ival-<=: 583.0ms (0.9% of total)
ival-cbrt: 528.0ms (0.8% of total)
ival-<: 478.0ms (0.7% of total)
ival-atan: 443.0ms (0.7% of total)
ival-and: 334.0ms (0.5% of total)
ival-neg: 263.0ms (0.4% of total)
ival-fmin: 114.0ms (0.2% of total)
ival-assert: 63.0ms (0.1% of total)
ival->: 1.0ms (0% of total)
exact: 0.0ms (0% of total)
Bogosity

rewrite30.4s (16.9%)

Memory
853.0MiB live, 35 451.3MiB allocated; 6.1s collecting garbage
Stop Event
223×iter-limit
110×node-limit
Counts
2 565 → 160 552

eval22.6s (12.6%)

Memory
268.9MiB live, 28 884.8MiB allocated; 11.3s collecting garbage
Compiler

Compiled 1 833 415 to 563 491 computations (69.3% saved)

prune6.1s (3.4%)

Memory
-31.9MiB live, 8 430.5MiB allocated; 3.2s collecting garbage
Counts
150 580 → 1 836
Compiler

Compiled 58 756 to 48 764 computations (17% saved)

series5.8s (3.2%)

Memory
21.5MiB live, 8 123.0MiB allocated; 1.4s collecting garbage
Stop Event
110×iter-limit
Counts
2 565 → 9 354
Calls

510 calls:

TimeVariablePointExpression
105.0ms
eps
@inf
((log (/ (- 1 eps) (+ 1 eps))) (* eps (- (* (pow eps 2) (- (* (pow eps 2) (- (* -2/7 (pow eps 2)) 2/5)) 2/3)) 2)) eps (- (* (pow eps 2) (- (* (pow eps 2) (- (* -2/7 (pow eps 2)) 2/5)) 2/3)) 2) (* (pow eps 2) (- (* (pow eps 2) (- (* -2/7 (pow eps 2)) 2/5)) 2/3)) (pow eps 2) 2 (- (* (pow eps 2) (- (* -2/7 (pow eps 2)) 2/5)) 2/3) (* (pow eps 2) (- (* -2/7 (pow eps 2)) 2/5)) (- (* -2/7 (pow eps 2)) 2/5) (* -2/7 (pow eps 2)) -2/7 2/5 2/3 (log (/ (- 1 eps) (+ 1 eps))) (* -2 eps) -2 (log (/ 1 (/ (- eps -1) (- 1 eps)))) (/ 1 (/ (- eps -1) (- 1 eps))) 1 (/ (- eps -1) (- 1 eps)) (- eps -1) -1 (- 1 eps) (log (/ (- 1 eps) (+ 1 eps))) (/ (- 1 eps) (+ 1 eps)) (+ 1 (* eps (- (* eps (+ 2 (* -2 eps))) 2))) (* eps (- (* eps (+ 2 (* -2 eps))) 2)) (- (* eps (+ 2 (* -2 eps))) 2) (* eps (+ 2 (* -2 eps))) (+ 2 (* -2 eps)) (- (log (- 2 (+ eps eps))) (log (+ (* 2 eps) 2))) (log (- 2 (+ eps eps))) (- 2 (+ eps eps)) (+ eps eps) (log (+ (* 2 eps) 2)) (+ (* 2 eps) 2))
94.0ms
eps
@-inf
((log (/ (- 1 eps) (+ 1 eps))) (* eps (- (* (pow eps 2) (- (* (pow eps 2) (- (* -2/7 (pow eps 2)) 2/5)) 2/3)) 2)) eps (- (* (pow eps 2) (- (* (pow eps 2) (- (* -2/7 (pow eps 2)) 2/5)) 2/3)) 2) (* (pow eps 2) (- (* (pow eps 2) (- (* -2/7 (pow eps 2)) 2/5)) 2/3)) (pow eps 2) 2 (- (* (pow eps 2) (- (* -2/7 (pow eps 2)) 2/5)) 2/3) (* (pow eps 2) (- (* -2/7 (pow eps 2)) 2/5)) (- (* -2/7 (pow eps 2)) 2/5) (* -2/7 (pow eps 2)) -2/7 2/5 2/3 (log (/ (- 1 eps) (+ 1 eps))) (* -2 eps) -2 (log (/ 1 (/ (- eps -1) (- 1 eps)))) (/ 1 (/ (- eps -1) (- 1 eps))) 1 (/ (- eps -1) (- 1 eps)) (- eps -1) -1 (- 1 eps) (log (/ (- 1 eps) (+ 1 eps))) (/ (- 1 eps) (+ 1 eps)) (+ 1 (* eps (- (* eps (+ 2 (* -2 eps))) 2))) (* eps (- (* eps (+ 2 (* -2 eps))) 2)) (- (* eps (+ 2 (* -2 eps))) 2) (* eps (+ 2 (* -2 eps))) (+ 2 (* -2 eps)) (- (log (- 2 (+ eps eps))) (log (+ (* 2 eps) 2))) (log (- 2 (+ eps eps))) (- 2 (+ eps eps)) (+ eps eps) (log (+ (* 2 eps) 2)) (+ (* 2 eps) 2))
74.0ms
n
@-inf
((- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (/ (- (+ (* (log (- x -1)) n) (* (* (log (- x -1)) (log (- x -1))) 1/2)) (* (log x) (+ n (* (log x) 1/2)))) n) n) (/ (- (+ (* (log (- x -1)) n) (* (* (log (- x -1)) (log (- x -1))) 1/2)) (* (log x) (+ n (* (log x) 1/2)))) n) (- (+ (* (log (- x -1)) n) (* (* (log (- x -1)) (log (- x -1))) 1/2)) (* (log x) (+ n (* (log x) 1/2)))) (+ (* (log (- x -1)) n) (* (* (log (- x -1)) (log (- x -1))) 1/2)) (log (- x -1)) (- x -1) x -1 n (* (* (log (- x -1)) (log (- x -1))) 1/2) (* (log (- x -1)) (log (- x -1))) 1/2 (* (log x) (+ n (* (log x) 1/2))) (log x) (+ n (* (log x) 1/2)) (* (log x) 1/2) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (- (log (+ 1 x)) (log x)) n) (/ 1 (* n x)) 1 (* n x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ 1 (/ n (log (/ (- x -1) x)))) (/ n (log (/ (- x -1) x))) (log (/ (- x -1) x)) (/ (- x -1) x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (- (+ (log (+ 1 x)) (* 1/2 (/ (pow (log (+ 1 x)) 2) n))) (+ (log x) (* 1/2 (/ (pow (log x) 2) n)))) n) (- (+ (log (+ 1 x)) (* 1/2 (/ (pow (log (+ 1 x)) 2) n))) (+ (log x) (* 1/2 (/ (pow (log x) 2) n)))) (/ (+ 1 (* -1 (/ (log (/ 1 x)) n))) x) (+ 1 (* -1 (/ (log (/ 1 x)) n))) (* -1 (/ (log (/ 1 x)) n)) (/ (log (/ 1 x)) n) (log (/ 1 x)) (/ 1 x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (+ (* (* (log x) (/ (log x) n)) -1/2) (+ (* (/ (* (log (- x -1)) (log (- x -1))) n) 1/2) (log (/ (- x -1) x)))) n) (+ (* (* (log x) (/ (log x) n)) -1/2) (+ (* (/ (* (log (- x -1)) (log (- x -1))) n) 1/2) (log (/ (- x -1) x)))) (* (log x) (/ (log x) n)) (/ (log x) n) -1/2 (+ (* (/ (* (log (- x -1)) (log (- x -1))) n) 1/2) (log (/ (- x -1) x))) (/ (* (log (- x -1)) (log (- x -1))) n))
62.0ms
x
@-inf
((- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (* (/ x (/ -1 (log (/ x (- x -1))))) (/ 1 (* n x))) (/ x (/ -1 (log (/ x (- x -1))))) x (/ -1 (log (/ x (- x -1)))) -1 (log (/ x (- x -1))) (/ x (- x -1)) (- x -1) (/ 1 (* n x)) 1 (* n x) n (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (- (log (+ 1 x)) (log x)) n) (/ (/ 1 n) x) (/ 1 n) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (- (log (+ 1 x)) (log x)) n) (- (log (+ 1 x)) (log x)) (/ (- 1 (* 1/2 (/ 1 x))) x) (- 1 (* 1/2 (/ 1 x))) (* 1/2 (/ 1 x)) 1/2 (/ 1 x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (exp (* (log (/ n (log (/ (- x -1) x)))) -1)) (* (log (/ n (log (/ (- x -1) x)))) -1) (log (/ n (log (/ (- x -1) x)))) (/ n (log (/ (- x -1) x))) (log (/ (- x -1) x)) (/ (- x -1) x))
60.0ms
x
@0
((- (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))) (/ 1/2 (* (pow x 3) (pow (sqrt (/ 1 x)) 3))) 1/2 (* (pow x 3) (pow (sqrt (/ 1 x)) 3)) (pow x 3/2) x 3/2 (- (sqrt (/ 1 x)) (/ 1 (sqrt (+ x 1)))) (sqrt (/ 1 x)) (/ 1 x) 1 (- (sqrt (/ 1 x)) (/ 1 (sqrt (- x -1)))) (/ 1 (sqrt (- x -1))) (sqrt (- x -1)) (- x -1) -1 (* (/ (sqrt x) x) (- 1 (sqrt (/ x (- x -1))))) (/ (sqrt x) x) (sqrt x) (- 1 (sqrt (/ x (- x -1)))) (sqrt (/ x (- x -1))) (/ x (- x -1)) (- (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))) (/ 1/2 (* (pow x 3) (pow (sqrt (/ 1 x)) 3))) (* (pow x 3) (pow (sqrt (/ 1 x)) 3)) (pow (/ 1 (/ (sqrt x) x)) 3) (/ 1 (/ (sqrt x) x)) 3)

derivations4.6s (2.6%)

Memory
-223.2MiB live, 3 493.7MiB allocated; 680ms collecting garbage
Stop Event
23×fuel
5×done
Compiler

Compiled 2 375 to 1 570 computations (33.9% saved)

preprocess4.0s (2.2%)

Memory
104.7MiB live, 4 513.9MiB allocated; 1.1s collecting garbage
Stop Event
28×node-limit
Compiler

Compiled 5 851 to 4 619 computations (21.1% saved)

regimes3.1s (1.7%)

Memory
-114.7MiB live, 4 575.0MiB allocated; 792ms collecting garbage
Counts
4 026 → 292
Calls

43 calls:

975.0ms
x
242.0ms
eps
211.0ms
b
117.0ms
(-.f64 (tan.f64 (+.f64 x eps)) (tan.f64 x))
101.0ms
(-.f64 (sin.f64 (+.f64 x eps)) (sin.f64 x))
Compiler

Compiled 1 480 to 1 576 computations (-6.5% saved)

bsearch1.8s (1%)

Memory
73.9MiB live, 1 329.2MiB allocated; 798ms collecting garbage
Algorithm
97×binary-search
18×left-value
Stop Event
96×narrow-enough
1×predicate-same
Samples
511.0ms5 853×0valid
359.0ms1 155×0invalid
221.0ms1 196×1valid
150.0ms551×2valid
14.0ms207×0exit
Compiler

Compiled 23 910 to 24 824 computations (-3.8% saved)

Precisions
Click to see histograms. Total time spent on operations: 984.0ms
ival-div!: 346.0ms (35.2% of total)
ival-pow: 218.0ms (22.2% of total)
ival-mult!: 105.0ms (10.7% of total)
ival-neg: 102.0ms (10.4% of total)
ival-sqrt: 59.0ms (6% of total)
adjust: 51.0ms (5.2% of total)
ival-sub!: 39.0ms (4% of total)
ival-cos: 32.0ms (3.3% of total)
ival-add!: 19.0ms (1.9% of total)
ival-expm1: 8.0ms (0.8% of total)
ival-cbrt: 3.0ms (0.3% of total)
ival-exp: 2.0ms (0.2% of total)

analyze1.7s (0.9%)

Memory
33.4MiB live, 2 203.7MiB allocated; 578ms 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)

start1.0ms (0%)

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

end0.0ms (0%)

Memory
0.6MiB live, 0.5MiB allocated; 0ms collecting garbage

Profiling

Loading profile data...