Herbie run

Date:Wednesday, April 30th, 2025
Commit:77680327 on prove-soundness
Seed:2025120
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:2 447.6 MB

Time bar (total: 4.3s)

sample3.3s (76.2%)

Memory
114.4MiB live, 1 932.2MiB allocated; 2.8s collecting garbage
Samples
1.2s5 798×2valid
1.0s10 355×1valid
265.0ms8 615×0valid
Precisions
Click to see histograms. Total time spent on operations: 1.6s
adjust: 607.0ms (37% of total)
ival-add!: 542.0ms (33% of total)
ival-sub!: 431.0ms (26.3% of total)
ival-mult!: 61.0ms (3.7% of total)
Bogosity

rewrite599.0ms (13.8%)

Memory
-36.1MiB live, 240.1MiB allocated; 55ms collecting garbage
Stop Event
20×iter-limit
4×node-limit
3×unsound
2×saturated
Counts
143 → 404

preprocess277.0ms (6.4%)

Memory
-24.5MiB live, 155.2MiB allocated; 28ms collecting garbage
Stop Event
3×node-limit
Compiler

Compiled 267 to 242 computations (9.4% saved)

derivations57.0ms (1.3%)

Memory
10.8MiB live, 10.7MiB allocated; 0ms collecting garbage
Stop Event
3×done
Compiler

Compiled 55 to 39 computations (29.1% saved)

regimes41.0ms (0.9%)

Memory
-1.1MiB live, 46.1MiB allocated; 4ms collecting garbage
Counts
21 → 8
Calls

8 calls:

12.0ms
(+.f64 x #s(literal 1 binary64))
10.0ms
x
6.0ms
(-.f64 (*.f64 (+.f64 x #s(literal 1 binary64)) (+.f64 x #s(literal 1 binary64))) #s(literal 1 binary64))
6.0ms
(*.f64 (+.f64 x #s(literal 1 binary64)) (+.f64 x #s(literal 1 binary64)))
1.0ms
z
Compiler

Compiled 106 to 87 computations (17.9% saved)

eval27.0ms (0.6%)

Memory
32.1MiB live, 32.1MiB allocated; 0ms collecting garbage
Compiler

Compiled 2 530 to 1 138 computations (55% saved)

prune14.0ms (0.3%)

Memory
16.0MiB live, 16.0MiB allocated; 0ms collecting garbage
Counts
346 → 19
Compiler

Compiled 251 to 215 computations (14.3% saved)

series14.0ms (0.3%)

Memory
12.8MiB live, 12.8MiB allocated; 0ms collecting garbage
Counts
40 → 103
Calls

33 calls:

TimeVariablePointExpression
1.0ms
x
@-inf
((- (* (+ x 1) (+ x 1)) 1) (* (- x -2) x) (- x -2) x -2 (- (* (+ x 1) (+ x 1)) 1) (* (+ x 1) (+ x 1)) 1 (- (* (+ x 1) (+ x 1)) 1) (+ x x) (- (* (+ x 1) (+ x 1)) 1) (* x x) (+ (+ (* x x) x) (+ x 0)) (+ (* x x) x) (+ x 0) 0)
1.0ms
x
@0
((- (* (+ x 1) (+ x 1)) 1) (* (- x -2) x) (- x -2) x -2 (- (* (+ x 1) (+ x 1)) 1) (* (+ x 1) (+ x 1)) 1 (- (* (+ x 1) (+ x 1)) 1) (+ x x) (- (* (+ x 1) (+ x 1)) 1) (* x x) (+ (+ (* x x) x) (+ x 0)) (+ (* x x) x) (+ x 0) 0)
1.0ms
x
@inf
((- (* (+ x 1) (+ x 1)) 1) (* (- x -2) x) (- x -2) x -2 (- (* (+ x 1) (+ x 1)) 1) (* (+ x 1) (+ x 1)) 1 (- (* (+ x 1) (+ x 1)) 1) (+ x x) (- (* (+ x 1) (+ x 1)) 1) (* x x) (+ (+ (* x x) x) (+ x 0)) (+ (* x x) x) (+ x 0) 0)
1.0ms
x
@-inf
((- (* (+ x 1) (+ x 1)) 1) (* (+ x 1) (+ x 1)) (+ x 1) x 1)
1.0ms
x
@-inf
((- (+ (+ x y) z) (+ x (+ y z))) (+ (+ x y) z) (+ x y) x y z (+ x (+ y z)) (+ y z))

analyze1.0ms (0%)

Memory
1.9MiB live, 1.9MiB allocated; 0ms collecting garbage
Algorithm
3×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%99.9%0.1%0%0%0%0
100%99.9%0%0.1%0%0%0%1
Compiler

Compiled 31 to 23 computations (25.8% saved)

bsearch0.0ms (0%)

Memory
0.2MiB live, 0.2MiB allocated; 0ms collecting garbage
Algorithm
1×left-value
Compiler

Compiled 11 to 9 computations (18.2% saved)

start0.0ms (0%)

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

end0.0ms (0%)

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

Profiling

Loading profile data...