Metrics for Herbie run

Date:	Friday, April 11th, 2025
Commit:	1485bc85 on chassis-platforms-cleanup
Seed:	2025101
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:	83 571.1 MB

sample38.8s (53.9%)

Memory

465.0MiB live, 42 023.7MiB allocated; 11.5s collecting garbage

Samples

11.5s	15 159×	5	exit
7.7s	39 631×	1	valid
6.7s	108 502×	0	valid
5.1s	16 987×	2	valid
485.0ms	3 900×	0	invalid
217.0ms	1 119×	1	exit
146.0ms	1 391×	0	exit

Precisions

Click to see histograms. Total time spent on operations: 24.6s

ival-exp: 3.8s (15.4% of total)

ival-pow: 3.6s (14.5% of total)

adjust: 3.0s (12.2% of total)

ival-cos: 2.4s (9.9% of total)

ival-log: 1.5s (6.3% of total)

ival-tan: 1.4s (5.7% of total)

ival-sinh: 1.4s (5.5% of total)

ival-sqrt: 1.3s (5.3% of total)

ival-mult!: 1.3s (5.2% of total)

ival-fmod: 1.0s (4.2% of total)

ival-acos: 750.0ms (3.1% of total)

ival-div!: 731.0ms (3% of total)

ival-sin: 713.0ms (2.9% of total)

ival-sub!: 420.0ms (1.7% of total)

ival-pow2: 402.0ms (1.6% of total)

ival-add!: 328.0ms (1.3% of total)

ival-neg: 219.0ms (0.9% of total)

ival-hypot: 170.0ms (0.7% of total)

ival-atan: 54.0ms (0.2% of total)

ival-<=: 52.0ms (0.2% of total)

ival-and: 34.0ms (0.1% of total)

ival-or: 15.0ms (0.1% of total)

ival-assert: 4.0ms (0% of total)

ival->: 2.0ms (0% of total)

ival-<: 2.0ms (0% of total)

Bogosity

rewrite10.4s (14.4%)

Memory

100.0MiB live, 10 623.3MiB allocated; 2.7s collecting garbage

Stop Event

187×	iter-limit
49×	node-limit
17×	unsound
4×	saturated

Counts

8 024 → 17 864

regimes4.9s (6.9%)

Memory

107.3MiB live, 7 489.4MiB allocated; 828ms collecting garbage

Counts

3 760 → 195

Calls

53 calls:

583.0ms	x
513.0ms	a
427.0ms	b
324.0ms	r
278.0ms	(/.f64 (sin.f64 b) (cos.f64 (+.f64 a b)))

Compiler

Compiled 1 801 to 2 083 computations (-15.7% saved)

derivations3.0s (4.1%)

Memory

-136.0MiB live, 2 653.9MiB allocated; 429ms collecting garbage

Stop Event

14×	fuel
6×	done

Compiler

Compiled 4 314 to 991 computations (77% saved)

eval2.9s (4.1%)

Memory: 228.8MiB live, 4 167.6MiB allocated; 1.5s collecting garbage
Compiler: Compiled 732 365 to 92 251 computations (87.4% saved)

series2.8s (3.8%)

Memory

179.0MiB live, 3 818.6MiB allocated; 1.2s collecting garbage

Counts

1 626 → 6 398

Calls

384 calls:

Time	Variable		Point	Expression
351.0ms	l	@	-inf	((* (exp (neg w)) (pow l (exp w))) (exp (neg w)) (neg w) w (pow l (exp w)) (/ 1 (pow l (neg (exp w)))) 1 (pow l (neg (exp w))) l (neg (exp w)) (exp w) (* (exp (neg w)) (pow l (exp w))) (* (exp (neg w)) (pow l (exp w))) (exp (neg w)) (- 1 w) (pow l (exp w)) (* (- (cosh w) (sinh w)) (pow l (exp w))) (- (cosh w) (sinh w)) (cosh w) (sinh w) (* (exp (neg w)) (pow l (exp w))) (+ (* (+ (* (+ (* (neg (log l)) l) (* l (+ (* 1/2 (* (+ (log l) 1) (log l))) 1/2))) w) (+ (* (log l) l) (neg l))) w) l) (+ (* (+ (* (neg (log l)) l) (* l (+ (* 1/2 (* (+ (log l) 1) (log l))) 1/2))) w) (+ (* (log l) l) (neg l))) (+ (* (neg (log l)) l) (* l (+ (* 1/2 (* (+ (log l) 1) (log l))) 1/2))) (neg (log l)) (log l) (* l (+ (* 1/2 (* (+ (log l) 1) (log l))) 1/2)) (+ (* 1/2 (* (+ (log l) 1) (log l))) 1/2) 1/2 (* (+ (log l) 1) (log l)) (+ (log l) 1) (+ (* (log l) l) (neg l)) (neg l))
98.0ms	x	@	0	((* (sqrt x) (sqrt (+ x x))) (sqrt x) x (sqrt (+ x x)) (+ x x) (sqrt (+ (* x x) (* x x))) (+ (* x x) (* x x)) 2 (sqrt (+ (* x x) (* x x))) (* (sqrt 2) x) (sqrt 2) (* (sqrt 2) (fabs x)) (fabs x) (sqrt (+ (* x x) (exp (* (log x) 2)))) (+ (* x x) (exp (* (log x) 2))) (* x x) (exp (* (log x) 2)) (* (log x) 2) (log x))
47.0ms	x	@	0	((+ x (- (+ (/ (tan y) (- 1 (* (tan y) (tan z)))) (/ (tan z) (- 1 (* (/ (sin y) (cos y)) (tan z))))) (tan a))) x (- (+ (/ (tan y) (- 1 (* (tan y) (tan z)))) (/ (tan z) (- 1 (* (/ (sin y) (cos y)) (tan z))))) (tan a)) (+ (/ (tan y) (- 1 (* (tan y) (tan z)))) (/ (tan z) (- 1 (* (/ (sin y) (cos y)) (tan z))))) (/ (tan y) (- 1 (* (tan y) (tan z)))) (tan y) y (- 1 (* (tan y) (tan z))) 1 (* (tan y) (tan z)) (tan z) z (/ (tan z) (- 1 (* (/ (sin y) (cos y)) (tan z)))) (- 1 (* (/ (sin y) (cos y)) (tan z))) (* (/ (sin y) (cos y)) (tan z)) (/ (sin y) (cos y)) (sin y) (cos y) (tan a) a (+ x (- (+ (/ (tan y) (- 1 (* (tan y) (tan z)))) (/ (tan z) (- 1 (* (tan y) (tan z))))) (tan a))) (- (+ (/ (tan y) (- 1 (* (tan y) (tan z)))) (/ (tan z) (- 1 (* (tan y) (tan z))))) (tan a)) (tan (+ z y)) (+ z y) (+ x (- (tan (+ z y)) (tan a))) (- (tan (+ z y)) (tan a)) (tan (+ z y)) (+ z y) (* z (+ (/ y z) 1)) (+ (/ y z) 1) (/ y z) (+ x (- (tan (+ y z)) (tan a))) (- (+ (+ (* (- 1 (neg (pow (tan y) 2))) z) (tan y)) x) (tan a)) (+ (+ (* (- 1 (neg (pow (tan y) 2))) z) (tan y)) x) (+ (* (- 1 (neg (pow (tan y) 2))) z) (tan y)) (- 1 (neg (pow (tan y) 2))) (neg (pow (tan y) 2)) (pow (tan y) 2) 2 (+ x (- (tan (/ (- (* y y) (* z z)) (/ (- (pow y 3) (pow z 3)) (+ (* y y) (+ (* z z) (* y z)))))) (tan a))) (- (tan (/ (- (* y y) (* z z)) (/ (- (pow y 3) (pow z 3)) (+ (* y y) (+ (* z z) (* y z)))))) (tan a)) (tan (/ (- (* y y) (* z z)) (/ (- (pow y 3) (pow z 3)) (+ (* y y) (+ (* z z) (* y z)))))) (/ (- (* y y) (* z z)) (/ (- (pow y 3) (pow z 3)) (+ (* y y) (+ (* z z) (* y z))))) (- (* y y) (* z z)) (* y y) (* z z) (/ (- (pow y 3) (pow z 3)) (+ (* y y) (+ (* z z) (* y z)))) (- (pow y 3) (pow z 3)) (pow y 3) 3 (pow z 3) (+ (* y y) (+ (* z z) (* y z))) (+ (* z z) (* y z)) (* y z))
41.0ms	x	@	inf	((/ (/ (+ (* (/ (* (* (PI) (PI)) (* (PI) (PI))) 16) (* (PI) (/ (PI) 4))) (pow (neg (pow (asin (+ -1 x)) 2)) 3)) (+ (/ (* (* (PI) (PI)) (* (PI) (PI))) 16) (- (pow (asin (- 1 x)) 4) (* (* (PI) (/ (PI) 4)) (neg (pow (asin (+ -1 x)) 2)))))) (+ (/ (PI) 2) (asin (- 1 x)))) (/ (+ (* (/ (* (* (PI) (PI)) (* (PI) (PI))) 16) (* (PI) (/ (PI) 4))) (pow (neg (pow (asin (+ -1 x)) 2)) 3)) (+ (/ (* (* (PI) (PI)) (* (PI) (PI))) 16) (- (pow (asin (- 1 x)) 4) (* (* (PI) (/ (PI) 4)) (neg (pow (asin (+ -1 x)) 2)))))) (+ (* (/ (* (* (PI) (PI)) (* (PI) (PI))) 16) (* (PI) (/ (PI) 4))) (pow (neg (pow (asin (+ -1 x)) 2)) 3)) (/ (* (* (PI) (PI)) (* (PI) (PI))) 16) (* (* (PI) (PI)) (* (PI) (PI))) (* (PI) (PI)) (PI) 16 (* (PI) (/ (PI) 4)) (/ (PI) 4) 4 (pow (neg (pow (asin (+ -1 x)) 2)) 3) (neg (pow (asin (+ -1 x)) 2)) (pow (asin (+ -1 x)) 2) (asin (+ -1 x)) (+ -1 x) -1 x 2 3 (+ (/ (* (* (PI) (PI)) (* (PI) (PI))) 16) (- (pow (asin (- 1 x)) 4) (* (* (PI) (/ (PI) 4)) (neg (pow (asin (+ -1 x)) 2))))) (- (pow (asin (- 1 x)) 4) (* (* (PI) (/ (PI) 4)) (neg (pow (asin (+ -1 x)) 2)))) (pow (asin (- 1 x)) 4) (asin (- 1 x)) (- 1 x) 1 (* (* (PI) (/ (PI) 4)) (neg (pow (asin (+ -1 x)) 2))) (+ (/ (PI) 2) (asin (- 1 x))) (/ (PI) 2) (- (/ (PI) 2) (asin (- 1 x))) (- (* 1/2 (PI)) (asin (- 1 x))) (* 1/2 (PI)) 1/2 (acos (- 1 x)) (- 1 x) (* (/ (- (/ 1 (* (* x x) x)) 1) (+ (+ (/ 1 (* x x)) 1) (/ 1 x))) x) (/ (- (/ 1 (* (* x x) x)) 1) (+ (+ (/ 1 (* x x)) 1) (/ 1 x))) (- (/ 1 (* (* x x) x)) 1) (/ 1 (* (* x x) x)) (* (* x x) x) (* x x) (+ (+ (/ 1 (* x x)) 1) (/ 1 x)) (+ (/ 1 (* x x)) 1) (/ 1 (* x x)) (/ 1 x) (/ (* (+ (/ (PI) -2) (asin (+ -1 x))) (acos (- 1 x))) (+ (/ (PI) -2) (asin (+ -1 x)))) (* (+ (/ (PI) -2) (asin (+ -1 x))) (acos (- 1 x))) (+ (/ (PI) -2) (asin (+ -1 x))) (/ (PI) -2) -2 (acos (- 1 x)) (- (/ (PI) 2) (* (pow (asin (- 1 x)) 1/2) (pow (asin (- 1 x)) 1/2))) (* (pow (asin (- 1 x)) 1/2) (pow (asin (- 1 x)) 1/2)) (pow (asin (- 1 x)) 1/2))
38.0ms	l	@	0	((* (exp (neg w)) (pow l (exp w))) (exp (neg w)) (neg w) w (pow l (exp w)) (/ 1 (pow l (neg (exp w)))) 1 (pow l (neg (exp w))) l (neg (exp w)) (exp w) (* (exp (neg w)) (pow l (exp w))) (* (exp (neg w)) (pow l (exp w))) (exp (neg w)) (- 1 w) (pow l (exp w)) (* (- (cosh w) (sinh w)) (pow l (exp w))) (- (cosh w) (sinh w)) (cosh w) (sinh w) (* (exp (neg w)) (pow l (exp w))) (+ (* (+ (* (+ (* (neg (log l)) l) (* l (+ (* 1/2 (* (+ (log l) 1) (log l))) 1/2))) w) (+ (* (log l) l) (neg l))) w) l) (+ (* (+ (* (neg (log l)) l) (* l (+ (* 1/2 (* (+ (log l) 1) (log l))) 1/2))) w) (+ (* (log l) l) (neg l))) (+ (* (neg (log l)) l) (* l (+ (* 1/2 (* (+ (log l) 1) (log l))) 1/2))) (neg (log l)) (log l) (* l (+ (* 1/2 (* (+ (log l) 1) (log l))) 1/2)) (+ (* 1/2 (* (+ (log l) 1) (log l))) 1/2) 1/2 (* (+ (log l) 1) (log l)) (+ (log l) 1) (+ (* (log l) l) (neg l)) (neg l))

analyze2.4s (3.3%)

Memory

109.5MiB live, 2 767.1MiB allocated; 1.2s collecting garbage

Algorithm

20×

Search

Probability	Valid	Unknown	Precondition	Infinite	Domain	Can't	Iter
0%	0%	73.7%	26.3%	0%	0%	0%	0
28.8%	21.3%	52.5%	26.3%	0%	0%	0%	1
44.1%	32.5%	41.2%	26.3%	0%	0%	0%	2
52.6%	38.7%	35%	26.3%	0%	0%	0%	3
61.9%	45.6%	28.1%	26.3%	0%	0%	0%	4
65.2%	47.5%	25.3%	26.3%	0%	0.9%	0%	5
66.8%	48.4%	24%	26.3%	0%	1.2%	0%	6
71.1%	51.1%	20.8%	26.3%	0%	1.9%	0%	7
72.1%	51.6%	20%	26.3%	0%	2.1%	0%	8
74.4%	53%	18.2%	26.3%	0%	2.5%	0%	9
75.8%	53.9%	17.2%	26.3%	0%	2.6%	0%	10
76.6%	54.3%	16.6%	26.3%	0%	2.8%	0%	11
77.3%	54.8%	16.1%	26.3%	0%	2.9%	0%	12

Compiler

Compiled 279 to 216 computations (22.6% saved)

preprocess2.4s (3.3%)

Memory

-122.9MiB live, 3 486.0MiB allocated; 474ms collecting garbage

Stop Event

15×	node-limit
5×	saturated

Compiler

Compiled 18 068 to 7 696 computations (57.4% saved)

explain2.2s (3.1%)

Memory

19.9MiB live, 3 078.8MiB allocated; 394ms collecting garbage

Explanations

Click to see full explanations table

Operator	Subexpression	Explanation	Count
`sqrt.f64`	`#f`	oflow-rescue	592	0
`cos.f64`	`#f`	sensitivity	532	2
`-.f64`	`#f`	cancellation	336	2
`sqrt.f64`	`#f`	uflow-rescue	273	0
`/.f64`	`#f`	n/o	258	0
`acos.f64`	`(acos.f64 (-.f64 #s(literal 1 binary64) x))`	sensitivity	254	1
`log.f64`	`(log.f64 (/.f64 (sinh.f64 x) x))`	sensitivity	253	0
`tan.f64`	`(tan.f64 (+.f64 y z))`	sensitivity	192	0
`pow.f64`	`(pow.f64 l (exp.f64 w))`	sensitivity	121	15
`*.f64`	`#f`	*nu**	40	0
`*.f64`	`#f`	*no**	27	0
`*.f64`	`#f`	*uo**	20	0
`-.f64`	`(-.f64 (.f64 a a) (.f64 b b))`	nan-rescue	20	0
↳	`(*.f64 a a)`	overflow	115
↳	`(*.f64 b b)`	overflow	20
`*.f64`	`(.f64 (pow.f64 c #s(literal 2 binary64)) (.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x))`	*ou**	17	0
↳	`(pow.f64 c #s(literal 2 binary64))`	overflow	65
↳	`(.f64 (.f64 x (pow.f64 s #s(literal 2 binary64))) x)`	underflow	71
↳	`(*.f64 x (pow.f64 s #s(literal 2 binary64)))`	underflow	65
↳	`(pow.f64 s #s(literal 2 binary64))`	underflow	72
`log.f64`	`(log.f64 (/.f64 (sinh.f64 x) x))`	oflow-rescue	2	0
↳	`(sinh.f64 x)`	overflow	2
↳	`(/.f64 (sinh.f64 x) x)`	overflow	2
`/.f64`	`(/.f64 (-.f64 x lo) (-.f64 hi lo))`	o/o	1	0
↳	`(-.f64 x lo)`	overflow	1
↳	`(-.f64 hi lo)`	overflow	256
`exp.f64`	`(exp.f64 (neg.f64 w))`	sensitivity	1	2
`tan.f64`	`(tan.f64 (+.f64 y z))`	cancellation	1	0

Confusion

	Predicted +	Predicted -
+	2129	264
-	736	1991

Precision

0.743106457242583

Recall

0.8896782281654827

Confusion?

	Predicted +	Predicted Maybe	Predicted -
+	2129	2	262
-	736	22	1969

Precision?

0.7376254759432329

Recall?

0.890513999164229

Freqs

test

number	freq
0	2255
1	2793
2	69
3	3

Total Confusion?

	Predicted +	Predicted Maybe	Predicted -
+	17	1	0
-	0	0	2

Precision?

1.0

Recall?

1.0

Samples

456.0ms	2 532×	1	valid
401.0ms	6 592×	0	valid
319.0ms	1 008×	2	valid
21.0ms	2×	3	valid
15.0ms	106×	1	exit

Compiler

Compiled 1 067 to 440 computations (58.8% saved)

Precisions

Click to see histograms. Total time spent on operations: 843.0ms

ival-tan: 103.0ms (12.2% of total)

ival-sqrt: 94.0ms (11.1% of total)

ival-cos: 83.0ms (9.8% of total)

adjust: 82.0ms (9.7% of total)

ival-log: 68.0ms (8.1% of total)

ival-sin: 60.0ms (7.1% of total)

ival-mult!: 58.0ms (6.9% of total)

ival-exp: 43.0ms (5.1% of total)

ival-fmod: 39.0ms (4.6% of total)

ival-sinh: 37.0ms (4.4% of total)

ival-acos: 35.0ms (4.1% of total)

ival-pow: 26.0ms (3.1% of total)

ival-div!: 25.0ms (3% of total)

ival-pow2: 23.0ms (2.7% of total)

ival-sub!: 21.0ms (2.5% of total)

ival-add!: 18.0ms (2.1% of total)

ival-hypot: 18.0ms (2.1% of total)

ival-neg: 6.0ms (0.7% of total)

ival-atan: 3.0ms (0.4% of total)

prune1.7s (2.4%)

Memory: -227.2MiB live, 2 664.2MiB allocated; 303ms collecting garbage
Counts: 20 349 → 1 396
Compiler: Compiled 73 982 to 38 352 computations (48.2% saved)

bsearch536.0ms (0.7%)

Memory

52.4MiB live, 796.9MiB allocated; 102ms collecting garbage

Algorithm

33×	binary-search
27×	left-value

Stop Event

29×	narrow-enough
4×	predicate-same

Samples

180.0ms	769×	1	valid
128.0ms	1 071×	0	valid
65.0ms	160×	2	valid

Compiler

Compiled 13 454 to 10 401 computations (22.7% saved)

Precisions

Click to see histograms. Total time spent on operations: 310.0ms

ival-exp: 72.0ms (23.3% of total)

ival-pow2: 45.0ms (14.5% of total)

ival-cos: 42.0ms (13.6% of total)

ival-mult!: 41.0ms (13.2% of total)

ival-fmod: 30.0ms (9.7% of total)

adjust: 21.0ms (6.8% of total)

ival-sin: 16.0ms (5.2% of total)

ival-pow: 12.0ms (3.9% of total)

ival-neg: 11.0ms (3.6% of total)

ival-sqrt: 8.0ms (2.6% of total)

ival-div!: 8.0ms (2.6% of total)

ival-add!: 4.0ms (1.3% of total)

start1.0ms (0%)

Memory: 1.5MiB live, 1.4MiB allocated; 0ms collecting garbage

end0.0ms (0%)

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

sample38.8s (53.9%)

rewrite10.4s (14.4%)

regimes4.9s (6.9%)

derivations3.0s (4.1%)

eval2.9s (4.1%)

series2.8s (3.8%)

analyze2.4s (3.3%)

preprocess2.4s (3.3%)

explain2.2s (3.1%)

prune1.7s (2.4%)

bsearch536.0ms (0.7%)

start1.0ms (0%)

end0.0ms (0%)

Profiling