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:2 632 749.8 MB

Time bar (total: 39.9min)

sample17.8min (44.5%)

Memory
17 301.5MiB live, 1 202 318.9MiB allocated; 6.9min collecting garbage
Samples
6.0min3 920 633×0valid
2.2min448 545×1valid
2.1min14 969×3exit
1.2min141 992×2valid
44.2s40 580×5exit
40.1s323 436×0invalid
18.8s4 566×4exit
12.6s15 343×3valid
7.8s50 083×0exit
7.6s29 455×1invalid
939.0ms6 624×1exit
633.0ms1 499×2invalid
105.0ms40×4valid
1.0ms1×2exit
Precisions
Click to see histograms. Total time spent on operations: 10.2min
ival-mult!: 2.0min (19.2% of total)
adjust: 59.7s (9.8% of total)
ival-pow: 45.8s (7.5% of total)
ival-exp: 45.7s (7.5% of total)
ival-div!: 42.7s (7% of total)
ival-log: 41.1s (6.7% of total)
ival-add!: 38.1s (6.2% of total)
ival-sub!: 33.0s (5.4% of total)
ival-pow2: 32.6s (5.4% of total)
ival-cos: 28.5s (4.7% of total)
ival-sin: 24.6s (4% of total)
ival-sqrt: 23.6s (3.9% of total)
ival-tan: 17.5s (2.9% of total)
ival-neg: 12.3s (2% of total)
ival-cosu: 7.2s (1.2% of total)
ival-sinu: 6.4s (1% of total)
ival-fabs: 4.3s (0.7% of total)
ival-hypot: 4.3s (0.7% of total)
ival-expm1: 3.3s (0.5% of total)
ival-asin: 2.5s (0.4% of total)
ival-fmax: 2.2s (0.4% of total)
ival-acos: 2.0s (0.3% of total)
ival-fmod: 1.9s (0.3% of total)
ival-sinh: 1.8s (0.3% of total)
ival-atan2: 1.7s (0.3% of total)
ival-log1p: 1.6s (0.3% of total)
ival-fmin: 1.3s (0.2% of total)
ival-atan: 1.1s (0.2% of total)
ival-<=: 1.0s (0.2% of total)
ival-cbrt: 724.0ms (0.1% of total)
ival-floor: 713.0ms (0.1% of total)
ival-and: 699.0ms (0.1% of total)
ival-<: 610.0ms (0.1% of total)
ival-acosh: 383.0ms (0.1% of total)
ival-asinh: 265.0ms (0% of total)
ival-cosh: 254.0ms (0% of total)
ival-tanu: 235.0ms (0% of total)
ival-atanh: 227.0ms (0% of total)
ival-if: 223.0ms (0% of total)
ival-log2: 222.0ms (0% of total)
ival-assert: 104.0ms (0% of total)
ival-tanh: 87.0ms (0% of total)
ival->=: 73.0ms (0% of total)
ival->: 51.0ms (0% of total)
ival-or: 14.0ms (0% of total)
ival-==: 3.0ms (0% of total)
const: 2.0ms (0% of total)
exact: 0.0ms (0% of total)
ival-pi: 0.0ms (0% of total)
Bogosity

rewrite7.6min (19.1%)

Memory
5 940.3MiB live, 405 432.2MiB allocated; 2.1min collecting garbage
Stop Event
2 541×iter-limit
1 983×saturated
1 721×node-limit
213×unsound
Counts
231 491 → 446 476

regimes2.6min (6.4%)

Memory
1 082.3MiB live, 200 091.6MiB allocated; 46.9s collecting garbage
Counts
75 362 → 8 270
Calls

1 238 calls:

15.4s
x
9.3s
y
7.9s
z
5.4s
a
5.3s
t
Compiler

Compiled 98 764 to 117 098 computations (-18.6% saved)

derivations2.4min (6.1%)

Memory
-1 663.7MiB live, 120 117.4MiB allocated; 31.7s collecting garbage
Stop Event
322×fuel
226×done
Compiler

Compiled 71 773 to 40 352 computations (43.8% saved)

series2.3min (5.9%)

Memory
7 263.8MiB live, 187 228.9MiB allocated; 44.7s collecting garbage
Counts
47 871 → 183 620
Calls

16359 calls:

TimeVariablePointExpression
1.3s
re
@-inf
((/ (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (+ (* (log base) (log base)) (* 0 0))) (* (log im) (/ 1 (log base))) (log im) im (/ 1 (log base)) 1 (log base) base (/ (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (+ (* (log base) (log base)) (* 0 0))) (* (log re) (/ 1 (log base))) (log re) re (/ (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (* (log base) (log base))) (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (* (log im) (log base)) (* (log base) (log base)) (* (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (/ 1 (* (log base) (log base)))) (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (* (log re) (log base)) (/ 1 (* (log base) (log base))) (/ (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (* (log base) (log base))) (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (* (neg (log (/ -1 im))) (log base)) (neg (log (/ -1 im))) (log (/ -1 im)) (/ -1 im) -1)
929.0ms
x
@0
((* (/ (sin (* x (* (PI) tau))) (* x (* (PI) tau))) (/ (sin (* x (PI))) (* x (PI)))) (/ (sin (* x (* (PI) tau))) (* x (* (PI) tau))) (sin (* x (* (PI) tau))) (* x (* (PI) tau)) x (* (PI) tau) (PI) tau (/ (sin (* x (PI))) (* x (PI))) (sin (* x (PI))) (* x (PI)) (* (/ (sin (* (* x (PI)) tau)) (* (* x (PI)) tau)) (/ (sin (* x (PI))) (* x (PI)))) 1 (* (/ (sin (* (* x (PI)) tau)) (* (* x (PI)) tau)) (/ (sin (* x (PI))) (* x (PI)))) (/ (sin (* (* x (PI)) tau)) (* (* x (PI)) tau)) (sin (* (* x (PI)) tau)) (* (* x (PI)) tau) (/ (sin (* x (PI))) (* x (PI))) (+ (* (* -1/6 (* x x)) (* (PI) (PI))) 1) (* -1/6 (* x x)) -1/6 (* x x) (* (PI) (PI)) (* (/ (sin (* (* x (PI)) tau)) (* (* x (PI)) tau)) (/ (sin (* x (PI))) (* x (PI)))) (* (sin (* (* tau x) (PI))) (/ (sin (* (PI) x)) (* (* (* (PI) (PI)) (* x x)) tau))) (sin (* (* tau x) (PI))) (* (* tau x) (PI)) (* tau x) (/ (sin (* (PI) x)) (* (* (* (PI) (PI)) (* x x)) tau)) (sin (* (PI) x)) (* (PI) x) (* (* (* (PI) (PI)) (* x x)) tau) (* (* (PI) (PI)) (* x x)) (/ (* (/ (sin (* (PI) x)) x) (sin (* (* tau x) (PI)))) (* (PI) (* (* tau x) (PI)))) (* (/ (sin (* (PI) x)) x) (sin (* (* tau x) (PI)))) (/ (sin (* (PI) x)) x) (* (PI) (* (* tau x) (PI))))
901.0ms
A
@-inf
((/ (neg (sqrt (* (* 2 (* (- (pow B 2) (* (* 4 A) C)) F)) (- (+ A C) (sqrt (+ (pow (- A C) 2) (pow B 2))))))) (- (pow B 2) (* (* 4 A) C))) (neg (sqrt (* (* 2 (* (- (pow B 2) (* (* 4 A) C)) F)) (- (+ A C) (sqrt (+ (pow (- A C) 2) (pow B 2))))))) (sqrt (* (* 2 (* (- (pow B 2) (* (* 4 A) C)) F)) (- (+ A C) (sqrt (+ (pow (- A C) 2) (pow B 2)))))) (* (* 2 (* (- (pow B 2) (* (* 4 A) C)) F)) (- (+ A C) (sqrt (+ (pow (- A C) 2) (pow B 2))))) (* 2 (* (- (pow B 2) (* (* 4 A) C)) F)) 2 (* (- (pow B 2) (* (* 4 A) C)) F) (- (pow B 2) (* (* 4 A) C)) (+ (* -4 (* A C)) (pow B 2)) -4 (* A C) A C (pow B 2) B F (- (+ A C) (sqrt (+ (pow (- A C) 2) (pow B 2)))) (- (+ A (* -1/2 (/ (pow B 2) C))) (* -1 A)) (+ (* -1/2 (/ (pow B 2) C)) (* 2 A)) -1/2 (/ (pow B 2) C) (* 2 A) (/ (neg (sqrt (* (* 2 (* (- (pow B 2) (* (* 4 A) C)) F)) (- (+ A C) (sqrt (+ (pow (- A C) 2) (pow B 2))))))) (- (pow B 2) (* (* 4 A) C))) (neg (sqrt (* (* 2 (* (- (pow B 2) (* (* 4 A) C)) F)) (- (+ A C) (sqrt (+ (pow (- A C) 2) (pow B 2))))))) (sqrt (* (* 2 (* (- (pow B 2) (* (* 4 A) C)) F)) (- (+ A C) (sqrt (+ (pow (- A C) 2) (pow B 2)))))) (* (* 2 (* (- (pow B 2) (* (* 4 A) C)) F)) (- (+ A C) (sqrt (+ (pow (- A C) 2) (pow B 2))))) (* 2 (* (- (pow B 2) (* (* 4 A) C)) F)) (* (- (pow B 2) (* (* 4 A) C)) F) (- (pow B 2) (* (* 4 A) C)) (* -4 (* A C)) (- (+ A C) (sqrt (+ (pow (- A C) 2) (pow B 2)))) (* -1 (* B (- (* -1 (/ (+ A C) B)) 1))) (+ A (+ B C)) (+ B C) (/ (neg (sqrt (* (* 2 (* (- (pow B 2) (* (* 4 A) C)) F)) (- (+ A C) (sqrt (+ (pow (- A C) 2) (pow B 2))))))) (- (pow B 2) (* (* 4 A) C))) (neg (sqrt (* (* 2 (* (- (pow B 2) (* (* 4 A) C)) F)) (- (+ A C) (sqrt (+ (pow (- A C) 2) (pow B 2))))))) (sqrt (* (* 2 (* (- (pow B 2) (* (* 4 A) C)) F)) (- (+ A C) (sqrt (+ (pow (- A C) 2) (pow B 2)))))) (* (* 2 (* (- (pow B 2) (* (* 4 A) C)) F)) (- (+ A C) (sqrt (+ (pow (- A C) 2) (pow B 2))))) (* (pow B 3) (+ (* -2 F) (* 2 (/ (* F (+ A C)) B)))) (pow B 3) 3 (+ (* -2 F) (* 2 (/ (* F (+ A C)) B))) (* -2 F) -2 (- (pow B 2) (* (* 4 A) C)) (* (* 4 A) C) (* 4 A) 4 (/ (neg (sqrt (* (* 2 (* (- (pow B 2) (* (* 4 A) C)) F)) (- (+ A C) (sqrt (+ (pow (- A C) 2) (pow B 2))))))) (- (pow B 2) (* (* 4 A) C))) (neg (sqrt (* (* 2 (* (- (pow B 2) (* (* 4 A) C)) F)) (- (+ A C) (sqrt (+ (pow (- A C) 2) (pow B 2))))))) (sqrt (* (* 2 (* (- (pow B 2) (* (* 4 A) C)) F)) (- (+ A C) (sqrt (+ (pow (- A C) 2) (pow B 2)))))) (* (* 2 (* (- (pow B 2) (* (* 4 A) C)) F)) (- (+ A C) (sqrt (+ (pow (- A C) 2) (pow B 2))))) (* 2 (* (- (pow B 2) (* (* 4 A) C)) F)) (* (- (pow B 2) (* (* 4 A) C)) F) (- (pow B 2) (* (* 4 A) C)) (- (+ A C) (sqrt (+ (pow (- A C) 2) (pow B 2)))) (* -1 (* B (- (* -1 (/ (+ A C) B)) 1))) -1 (* B (- (* -1 (/ (+ A C) B)) 1)) (- (* -1 (/ (+ A C) B)) 1) (* -1 (/ (+ A C) B)) (/ (+ A C) B) (+ A C) 1 (/ (neg (sqrt (* (* 2 (* (- (pow B 2) (* (* 4 A) C)) F)) (- (+ A C) (sqrt (+ (pow (- A C) 2) (pow B 2))))))) (- (pow B 2) (* (* 4 A) C))) (neg (sqrt (* (* 2 (* (- (pow B 2) (* (* 4 A) C)) F)) (- (+ A C) (sqrt (+ (pow (- A C) 2) (pow B 2))))))) (sqrt (* (* 2 (* (- (pow B 2) (* (* 4 A) C)) F)) (- (+ A C) (sqrt (+ (pow (- A C) 2) (pow B 2)))))) (* (* 2 (* (- (pow B 2) (* (* 4 A) C)) F)) (- (+ A C) (sqrt (+ (pow (- A C) 2) (pow B 2))))) (* 2 (* (- (pow B 2) (* (* 4 A) C)) F)) (* (- (pow B 2) (* (* 4 A) C)) F) (- (pow B 2) (* (* 4 A) C)) (* C (- (/ (pow B 2) C) (* 4 A))) (- (/ (pow B 2) C) (* 4 A)) (- (+ A C) (sqrt (+ (pow (- A C) 2) (pow B 2)))) (- (+ A (* -1/2 (/ (pow B 2) C))) (* -1 A)) (+ A (* -1/2 (/ (pow B 2) C))) (* -1/2 (/ (pow B 2) C)) (* -1 A))
861.0ms
c
@inf
((/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (+ (* (+ (* a (+ (* (/ (* (* (/ (pow c 4) (pow b 6)) 20) a) b) -1/4) (* (/ (* (* c c) c) (pow b 5)) -2))) (neg (/ (* c c) (* (* b b) b)))) a) (/ (neg c) b)) (+ (* a (+ (* (/ (* (* (/ (pow c 4) (pow b 6)) 20) a) b) -1/4) (* (/ (* (* c c) c) (pow b 5)) -2))) (neg (/ (* c c) (* (* b b) b)))) a (+ (* (/ (* (* (/ (pow c 4) (pow b 6)) 20) a) b) -1/4) (* (/ (* (* c c) c) (pow b 5)) -2)) (/ (* (* (/ (pow c 4) (pow b 6)) 20) a) b) (* (* (/ (pow c 4) (pow b 6)) 20) a) (* (/ (pow c 4) (pow b 6)) 20) (/ (pow c 4) (pow b 6)) (pow c 4) c 4 (pow b 6) b 6 20 -1/4 (* (/ (* (* c c) c) (pow b 5)) -2) (/ (* (* c c) c) (pow b 5)) (* (* c c) c) (* c c) (pow b 5) 5 -2 (neg (/ (* c c) (* (* b b) b))) (/ (* c c) (* (* b b) b)) (* (* b b) b) (* b b) (/ (neg c) b) (neg c) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (/ (+ (sqrt (+ (* (* -4 a) c) (* b b))) (neg b)) (+ a a)) (+ (sqrt (+ (* (* -4 a) c) (* b b))) (neg b)) (sqrt (+ (* (* -4 a) c) (* b b))) (+ (* (* -4 a) c) (* b b)) (* -4 a) -4 (neg b) (+ a a) (+ (/ (neg b) (+ a a)) (/ (sqrt (+ (* (* -4 a) c) (* b b))) (+ a a))) (/ (neg b) (+ a a)) (/ (sqrt (+ (* (* -4 a) c) (* b b))) (+ a a)) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (* (- (* (+ (* (* (* a a) (/ c (pow b 5))) -2) (neg (/ a (* (* b b) b)))) c) (/ 1 b)) c) (- (* (+ (* (* (* a a) (/ c (pow b 5))) -2) (neg (/ a (* (* b b) b)))) c) (/ 1 b)) (* (+ (* (* (* a a) (/ c (pow b 5))) -2) (neg (/ a (* (* b b) b)))) c) (+ (* (* (* a a) (/ c (pow b 5))) -2) (neg (/ a (* (* b b) b)))) (* (* a a) (/ c (pow b 5))) (* a a) (/ c (pow b 5)) (neg (/ a (* (* b b) b))) (/ a (* (* b b) b)) (/ 1 b) 1)
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))

preprocess2.0min (5%)

Memory
-4 184.5MiB live, 130 454.8MiB allocated; 37.7s collecting garbage
Stop Event
518×node-limit
29×saturated
3×iter-limit
1×unsound
Compiler

Compiled 528 452 to 377 962 computations (28.5% saved)

eval1.6min (4.1%)

Memory
1 400.7MiB live, 134 250.5MiB allocated; 38.9s collecting garbage
Compiler

Compiled 9 313 885 to 2 226 391 computations (76.1% saved)

analyze1.6min (4%)

Memory
263.1MiB live, 105 042.2MiB allocated; 39.2s collecting garbage
Algorithm
552×search
2×random
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%84.6%15.4%0%0%0%0
39.7%33.6%51.1%15.4%0%0%0%1
45.6%38.2%45.6%15.4%0%0.8%0%2
54.1%44.3%37.6%15.4%0%2.8%0%3
60.9%49.3%31.6%15.4%0%3.7%0%4
67.2%54.1%26.4%15.4%0%4.2%0%5
71.2%57%23.1%15.4%0%4.6%0%6
75.1%59.7%19.8%15.4%0%5.2%0%7
77.1%61%18.1%15.4%0%5.6%0%8
79.8%62.8%15.9%15.4%0%5.9%0%9
81.3%63.8%14.6%15.4%0%6.2%0%10
83.6%65.4%12.9%15.4%0%6.3%0%11
84.7%66.1%11.9%15.4%0%6.6%0%12
Compiler

Compiled 30 225 to 8 606 computations (71.5% saved)

prune1.1min (2.6%)

Memory
-2 111.3MiB live, 82 782.5MiB allocated; 28.0s collecting garbage
Counts
445 864 → 29 108
Compiler

Compiled 1 634 225 to 1 230 580 computations (24.7% saved)

bsearch56.1s (2.3%)

Memory
546.8MiB live, 64 919.4MiB allocated; 15.8s collecting garbage
Algorithm
2 747×binary-search
1 471×left-value
Stop Event
2 682×narrow-enough
63×predicate-same
2×predicate-failed
Samples
21.2s189 974×0valid
8.2s17 154×1valid
2.3s1 330×5exit
1.2s2 535×2valid
867.0ms7 614×0invalid
294.0ms337×3valid
113.0ms364×1invalid
105.0ms197×0exit
11.0ms41×2invalid
0.0ms1×1exit
Compiler

Compiled 1 083 684 to 1 026 989 computations (5.2% saved)

Precisions
Click to see histograms. Total time spent on operations: 23.9s
ival-mult!: 5.9s (24.5% of total)
ival-sin: 2.5s (10.5% of total)
ival-cos: 2.4s (10.2% of total)
ival-div!: 1.9s (7.9% of total)
ival-pow: 1.7s (7.2% of total)
ival-add!: 1.7s (7.2% of total)
adjust: 1.7s (7.2% of total)
ival-sub!: 1.6s (6.7% of total)
ival-pow2: 671.0ms (2.8% of total)
ival-exp: 629.0ms (2.6% of total)
ival-log: 615.0ms (2.6% of total)
ival-cosu: 412.0ms (1.7% of total)
ival-hypot: 348.0ms (1.5% of total)
ival-sqrt: 339.0ms (1.4% of total)
ival-sinu: 333.0ms (1.4% of total)
ival-atan2: 267.0ms (1.1% of total)
ival-neg: 265.0ms (1.1% of total)
ival-tan: 202.0ms (0.8% of total)
ival-fabs: 94.0ms (0.4% of total)
ival-acos: 65.0ms (0.3% of total)
ival-atan: 53.0ms (0.2% of total)
ival-fmax: 51.0ms (0.2% of total)
ival-log1p: 41.0ms (0.2% of total)
ival-fmin: 13.0ms (0.1% of total)
ival-expm1: 9.0ms (0% of total)
ival-cbrt: 9.0ms (0% of total)
ival-tanh: 8.0ms (0% of total)
ival-tanu: 7.0ms (0% of total)
ival->=: 7.0ms (0% of total)
ival-asin: 6.0ms (0% of total)
ival-if: 5.0ms (0% of total)
ival-cosh: 4.0ms (0% of total)
ival-fmod: 4.0ms (0% of total)
ival-sinh: 2.0ms (0% of total)
ival-pi: 0.0ms (0% of total)

start189.0ms (0%)

Memory
-106.6MiB live, 102.2MiB allocated; 162ms collecting garbage

end4.0ms (0%)

Memory
9.9MiB live, 9.1MiB allocated; 0ms collecting garbage

Profiling

Loading profile data...