Herbie run

Date:Monday, May 12th, 2025
Commit:2ad78556 on artem-rules-updates
Seed:2025132
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:21 933.0 MB

Time bar (total: 19.5s)

sample8.5s (43.6%)

Memory
233.2MiB live, 9 998.7MiB allocated; 5.0s collecting garbage
Samples
5.0s70 084×0valid
571.0ms4 210×2valid
131.0ms1 915×0invalid
1.0ms10×1valid
Precisions
Click to see histograms. Total time spent on operations: 3.4s
ival-mult!: 799.0ms (23.6% of total)
ival-sqrt: 772.0ms (22.8% of total)
ival-div!: 601.0ms (17.8% of total)
ival-sub!: 322.0ms (9.5% of total)
ival-neg: 302.0ms (8.9% of total)
ival-add!: 143.0ms (4.2% of total)
adjust: 127.0ms (3.8% of total)
ival-fabs: 117.0ms (3.5% of total)
ival-log: 104.0ms (3.1% of total)
ival-exp: 69.0ms (2% of total)
ival-if: 22.0ms (0.7% of total)
ival->=: 3.0ms (0.1% of total)
Bogosity

rewrite4.8s (24.4%)

Memory
83.6MiB live, 4 392.8MiB allocated; 1.0s collecting garbage
Stop Event
53×iter-limit
23×node-limit
12×saturated
10×unsound
Counts
2 967 → 4 636

preprocess1.4s (7.4%)

Memory
-201.6MiB live, 1 179.0MiB allocated; 386ms collecting garbage
Stop Event
8×node-limit
2×iter-limit
1×unsound
Compiler

Compiled 1 508 to 1 165 computations (22.7% saved)

series992.0ms (5.1%)

Memory
89.8MiB live, 1 426.4MiB allocated; 385ms collecting garbage
Counts
677 → 2 290
Calls

171 calls:

TimeVariablePointExpression
56.0ms
x
@0
((neg (log (- (/ 1 x) 1))) (log (- (/ 1 x) 1)) (- (/ 1 x) 1) (/ (+ (neg x) 1) x) (+ (neg x) 1) (neg x) x 1 (neg (log (- (/ 1 x) 1))) 0 (neg (log (- (/ 1 x) 1))) (log x) (neg (log (- (/ 1 x) 1))) (- (/ 1 x) 0) (/ 1 x) (neg (log (- (/ 1 x) 1))) (- x (neg (log x))) (neg (log x)))
44.0ms
x
@0
((neg (log (- (/ 1 x) 1))) (log (- (/ 1 x) 1)) (- (/ 1 x) 1) (/ (/ (- (* (neg x) (neg x)) 1) (- (neg x) 1)) x) (/ (- (* (neg x) (neg x)) 1) (- (neg x) 1)) (- (* (neg x) (neg x)) 1) (* (neg x) (neg x)) (neg x) x 1 (- (neg x) 1) (neg (log (- (/ 1 x) 1))) (/ 1 x) (neg (log (- (/ 1 x) 1))) (+ (log x) x) (log x) (neg (log (- (/ 1 x) 1))) (log (- (/ 1 x) 1)) (- (/ 1 x) 1) (/ (- (neg x) -1) x) (- (neg x) -1) -1 (log (/ 1 (- (/ 1 x) 1))) (/ 1 (- (/ 1 x) 1)) (- (/ 1 x) 1))
38.0ms
b
@0
((if (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (>= b 0) b 0 (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (neg b) (sqrt (- (* b b) (* (* 4 a) c))) (- (* b b) (* (* 4 a) c)) (* b b) (* (* 4 a) c) (* 4 a) 4 a c (* 2 a) 2 (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))
38.0ms
z
@0
((fabs (- (/ (+ x 4) y) (* (/ x y) z))) (- (/ (+ x 4) y) (* (/ x y) z)) (/ (+ x 4) y) (+ x 4) 4 y (* (/ x y) z) (/ x y) x z (fabs (/ (+ (* z x) (- -4 x)) y)) (/ (+ (* z x) (- -4 x)) y) (+ (* z x) (- -4 x)) (- -4 x) -4 (fabs (/ (+ (* z x) (- -4 x)) y)) (/ (+ (* z x) (- -4 x)) y) (+ (* z x) (- -4 x)) (* x z) (fabs (- (/ (+ x 4) y) (* (/ x y) z))) (- (/ (+ x 4) y) (* (/ x y) z)) (/ 1 (/ y (* (neg z) x))) 1 (/ y (* (neg z) x)) (* (neg z) x) (neg z) (fabs (+ (* (/ (- 1 z) y) x) (/ 4 y))) (+ (* (/ (- 1 z) y) x) (/ 4 y)) (/ (- 1 z) y) (/ (neg z) y) (/ 4 y))
28.0ms
a
@-inf
((if (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (>= b 0) b 0 (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (+ (* -1 (/ b a)) (/ c b)) -1 (/ b a) a (/ c b) c (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (* 2 c) 2 (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (neg b) (sqrt (- (* b b) (* (* 4 a) c))) (- (* b b) (* (* 4 a) c)) (* b b) (* (* 4 a) c) (* 4 a) 4 (if (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (sqrt (- (* b b) (* (* 4 a) c))) (* 2 a) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (if (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (sqrt (- (* b b) (* (* 4 a) c))) (+ b (* -2 (/ (* a c) b))) (* -2 (/ (* a c) b)) -2 (/ (* a c) b) (* a c) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (if (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (sqrt (- (* b b) (* (* 4 a) c))) (- (* b b) (* (* 4 a) c)) (pow b 2) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (if (>= b 0) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (/ (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (sqrt (- (* b b) (* (* 4 a) c))) (* -1 (* b (+ 1 (* -2 (/ (* a c) (pow b 2)))))) (* b (+ 1 (* -2 (/ (* a c) (pow b 2))))) (+ 1 (* -2 (/ (* a c) (pow b 2)))) 1 (* -2 (/ (* a c) (pow b 2))) (/ (* a c) (pow b 2)) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))

eval863.0ms (4.4%)

Memory
29.9MiB live, 1 186.9MiB allocated; 238ms collecting garbage
Compiler

Compiled 73 324 to 23 632 computations (67.8% saved)

derivations852.0ms (4.4%)

Memory
85.9MiB live, 887.6MiB allocated; 87ms collecting garbage
Stop Event
5×done
4×fuel
Compiler

Compiled 729 to 463 computations (36.5% saved)

regimes724.0ms (3.7%)

Memory
-93.3MiB live, 984.7MiB allocated; 288ms collecting garbage
Counts
373 → 88
Calls

23 calls:

101.0ms
(-.f64 (/.f64 #s(literal 1 binary64) x) #s(literal 1 binary64))
88.0ms
b
78.0ms
(-.f64 (/.f64 (+.f64 x #s(literal 4 binary64)) y) (*.f64 (/.f64 x y) z))
68.0ms
x
31.0ms
z
Compiler

Compiled 735 to 753 computations (-2.4% saved)

bsearch593.0ms (3%)

Memory
48.8MiB live, 809.0MiB allocated; 158ms collecting garbage
Algorithm
37×binary-search
4×left-value
Stop Event
33×narrow-enough
4×predicate-same
Samples
233.0ms2 688×0valid
39.0ms451×0invalid
8.0ms64×2valid
Compiler

Compiled 19 138 to 16 314 computations (14.8% saved)

Precisions
Click to see histograms. Total time spent on operations: 174.0ms
ival-mult!: 53.0ms (30.4% of total)
ival-div!: 35.0ms (20.1% of total)
ival-sqrt: 33.0ms (18.9% of total)
ival-sub!: 12.0ms (6.9% of total)
ival-if: 9.0ms (5.2% of total)
ival-neg: 9.0ms (5.2% of total)
ival->=: 7.0ms (4% of total)
ival-fabs: 7.0ms (4% of total)
ival-add!: 7.0ms (4% of total)
adjust: 2.0ms (1.1% of total)

analyze536.0ms (2.7%)

Memory
15.1MiB live, 565.3MiB allocated; 528ms collecting garbage
Algorithm
9×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%99.9%0.1%0%0%0%0
22.2%22.2%77.7%0.1%0%0%0%1
29.4%27.8%66.6%0.1%0%5.6%0%2
50%44.4%44.4%0.1%0%11.1%0%3
59.7%51.3%34.7%0.1%0%13.9%0%4
66.4%56.2%28.4%0.1%0%15.3%0%5
74%62.1%21.8%0.1%0%16%0%6
77.6%63.8%18.4%0.1%0%17.7%0%7
79.3%65%17%0.1%0%17.9%0%8
85%69.2%12.2%0.1%0%18.5%0%9
86.8%69.7%10.6%0.1%0%19.6%0%10
88.7%71.1%9.1%0.1%0%19.8%0%11
91.6%72.9%6.7%0.1%0%20.3%0%12
Compiler

Compiled 153 to 106 computations (30.7% saved)

prune237.0ms (1.2%)

Memory
80.1MiB live, 501.6MiB allocated; 39ms collecting garbage
Counts
4 586 → 226
Compiler

Compiled 8 767 to 6 972 computations (20.5% saved)

start0.0ms (0%)

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

end0.0ms (0%)

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

Profiling

Loading profile data...