Metrics for Herbie run

Date:	Wednesday, November 13th, 2024
Commit:	b0f482cc on pavel-concrete-values
Hostname:	nightly with Racket 8.10
Seed:	2024318
Parameters:	256 points for 4 iterations
Flags:	`localize:costslocalize:errorsreduce:regimesreduce:binary-searchreduce:branch-expressionssetup:simplifysetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:simplifygenerate:proofs` default

sample1.2min (23.6%)

Memory

743.0MiB live, 69 447.7MiB allocated

Samples

30.8s	285 585×	0	valid
12.7s	43 764×	1	valid
7.8s	16 990×	2	valid
823.0ms	4 270×	0	invalid
177.0ms	413×	3	valid
115.0ms	934×	0	exit
96.0ms	101×	4	exit
79.0ms	101×	3	exit
6.0ms	42×	1	exit

Precisions

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

ival-mult: 9.1s (23% of total)

ival-add: 3.8s (9.7% of total)

ival-sub: 3.5s (8.9% of total)

ival-pow: 3.4s (8.8% of total)

ival-div: 3.4s (8.7% of total)

const: 3.4s (8.7% of total)

adjust: 2.5s (6.3% of total)

ival-<=: 2.3s (5.9% of total)

ival-sin: 2.1s (5.3% of total)

ival-cos: 1.8s (4.6% of total)

ival-sqrt: 747.0ms (1.9% of total)

ival-exp: 483.0ms (1.2% of total)

exact: 466.0ms (1.2% of total)

ival-neg: 415.0ms (1.1% of total)

ival-and: 384.0ms (1% of total)

ival-pow2: 263.0ms (0.7% of total)

ival-==: 216.0ms (0.5% of total)

ival-tan: 199.0ms (0.5% of total)

ival-true: 157.0ms (0.4% of total)

ival-<: 152.0ms (0.4% of total)

ival-assert: 149.0ms (0.4% of total)

ival-expm1: 125.0ms (0.3% of total)

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

ival-log1p: 81.0ms (0.2% of total)

ival-pi: 62.0ms (0.2% of total)

ival-hypot: 17.0ms (0% of total)

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

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

Bogosity

simplify54.0s (17.7%)

Memory

1 193.9MiB live, 42 884.7MiB allocated

Algorithm

342×	egg-herbie

Stop Event

437×	iter limit
262×	node limit
93×	saturated

Counts

9 998 → 9 855

soundness45.6s (15%)

Memory

116.3MiB live, 25 058.3MiB allocated

Stop Event

276×	iter limit
182×	node limit
27×	fuel
15×	done
7×	saturated

Compiler

Compiled 45 366 to 13 582 computations (70.1% saved)

rewrite40.6s (13.3%)

Memory

-84.6MiB live, 34 914.3MiB allocated

Stop Event

294×	iter limit
146×	node limit
12×	saturated

Counts

1 888 → 90 574

localize23.5s (7.7%)

Memory

-857.4MiB live, 21 718.3MiB allocated

Samples

9.0s	29 513×	0	valid
4.4s	5 463×	1	valid
3.7s	2 840×	2	valid
428.0ms	154×	3	valid
89.0ms	269×	0	invalid
40.0ms	2×	4	valid
29.0ms	93×	0	exit
17.0ms	7×	5	exit
14.0ms	45×	1	exit
6.0ms	14×	2	exit

Compiler

Compiled 34 455 to 4 104 computations (88.1% saved)

Precisions

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

ival-mult: 3.4s (27.4% of total)

ival-add: 2.2s (17.8% of total)

ival-div: 1.7s (13.8% of total)

adjust: 1.2s (9.8% of total)

ival-pow: 902.0ms (7.2% of total)

ival-sub: 830.0ms (6.6% of total)

const: 750.0ms (6% of total)

ival-sin: 241.0ms (1.9% of total)

ival-atan: 213.0ms (1.7% of total)

ival-sqrt: 200.0ms (1.6% of total)

ival-cos: 193.0ms (1.5% of total)

ival-neg: 148.0ms (1.2% of total)

ival-exp: 140.0ms (1.1% of total)

ival-pow2: 90.0ms (0.7% of total)

exact: 61.0ms (0.5% of total)

ival-expm1: 41.0ms (0.3% of total)

ival-log1p: 38.0ms (0.3% of total)

ival-true: 35.0ms (0.3% of total)

ival-log: 19.0ms (0.2% of total)

ival-assert: 16.0ms (0.1% of total)

ival-tan: 6.0ms (0% of total)

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

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

eval20.5s (6.7%)

Memory: 81.0MiB live, 23 791.1MiB allocated
Compiler: Compiled 4 040 107 to 351 786 computations (91.3% saved)

preprocess11.2s (3.7%)

Memory

203.9MiB live, 8 762.7MiB allocated

Algorithm

42×	egg-herbie

Stop Event

82×	iter limit
54×	saturated
32×	node limit

Compiler

Compiled 59 947 to 9 052 computations (84.9% saved)

explain10.8s (3.5%)

Memory

-492.8MiB live, 11 123.1MiB allocated

Explanations

Click to see full explanations table

Operator	Subexpression	Explanation	Count
`-.f64`	`#f`	cancellation	1330	2
`+.f64`	`#f`	cancellation	355	92
`-.f64`	(-.f64 (*.f64 #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64) t) #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64))	oflow-left	219	0
`sqrt.f64`	`#f`	oflow-rescue	196	0
`log.f64`	`(log.f64 (+.f64 #s(literal 1 binary64) x))`	sensitivity	179	0
`/.f64`	`#f`	o/o	167	0
`/.f64`	`#f`	n/o	146	0
`pow.f64`	`(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)`	sensitivity	126	0
`-.f64`	`#f`	nan-rescue	93	0
`/.f64`	`#f`	u/n	91	0
`/.f64`	`#f`	n/u	53	0
`*.f64`	`#f`	*nu**	46	0
`/.f64`	`#f`	o/n	45	0
`+.f64`	`#f`	nan-rescue	42	0
`/.f64`	`#f`	u/u	40	0
`*.f64`	`#f`	*no**	26	0
`pow.f64`	`(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)`	oflow-rescue	20	0
↳	`(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)`	overflow	19
↳	`(/.f64 i n)`	overflow	20
↳	`(+.f64 #s(literal 1 binary64) (/.f64 i n))`	overflow	20
`sqrt.f64`	`#f`	uflow-rescue	16	0

Confusion

	Predicted +	Predicted -
+	3835	252
-	135	6530

Precision

0.9659949622166247

Recall

0.9383410814778567

Confusion?

	Predicted +	Predicted Maybe	Predicted -
+	3835	182	70
-	135	168	6362

Precision?

0.9298611111111111

Recall?

0.9828725226327379

Freqs

test

number	freq
0	6782
1	3519
2	407
3	44

Total Confusion?

	Predicted +	Predicted Maybe	Predicted -
+	31	1	0
-	2	0	8

Precision?

0.9411764705882353

Recall?

1.0

Samples

1.8s	16 384×	0	valid
1.2s	3 736×	1	valid
680.0ms	1 344×	2	valid
22.0ms	40×	3	valid

Compiler

Compiled 7 535 to 1 486 computations (80.3% saved)

Precisions

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

ival-mult: 550.0ms (21.7% of total)

adjust: 355.0ms (14% of total)

ival-add: 345.0ms (13.6% of total)

ival-div: 283.0ms (11.2% of total)

ival-sub: 180.0ms (7.1% of total)

ival-pow: 175.0ms (6.9% of total)

ival-cos: 116.0ms (4.6% of total)

ival-sin: 111.0ms (4.4% of total)

ival-sqrt: 110.0ms (4.3% of total)

const: 110.0ms (4.3% of total)

ival-exp: 63.0ms (2.5% of total)

ival-neg: 43.0ms (1.7% of total)

ival-pow2: 26.0ms (1% of total)

ival-true: 20.0ms (0.8% of total)

exact: 19.0ms (0.8% of total)

ival-assert: 9.0ms (0.4% of total)

ival-log1p: 5.0ms (0.2% of total)

ival-tan: 4.0ms (0.2% of total)

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

ival-expm1: 3.0ms (0.1% of total)

ival-pi: 2.0ms (0.1% of total)

regimes8.3s (2.7%)

Memory

-21.8MiB live, 8 263.0MiB allocated

Counts

5 511 → 602

Calls

96 calls:

966.0ms	x
417.0ms	(-.f64 #s(literal 1 binary64) (*.f64 x x))
340.0ms	(/.f64 (/.f64 #s(literal 2 binary64) t) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) t)))
338.0ms	(.f64 (cos.f64 x) (exp.f64 (.f64 #s(literal 10 binary64) (*.f64 x x))))
329.0ms	b

Compiler

Compiled 10 159 to 6 429 computations (36.7% saved)

prune6.2s (2%)

Memory: -83.0MiB live, 8 837.8MiB allocated
Counts: 97 227 → 2 088
Compiler: Compiled 149 045 to 65 348 computations (56.2% saved)

series4.6s (1.5%)

Memory

-95.4MiB live, 4 434.0MiB allocated

Counts

1 888 → 9 998

Calls

876 calls:

Time	Variable		Point	Expression
289.0ms	w	@	-inf	((- 3 (+ (* (* (* (* 1/8 (+ (* -2 v) 3)) w) (* r w)) (/ r (- 1 v))) 9/2)) (* 1/8 (+ (* -2 v) 3)) (+ (/ 2 (* r r)) (- 3 (+ (* (* (* (* 1/8 (+ (* -2 v) 3)) w) (* r w)) (/ r (- 1 v))) 9/2))) (/ 2 (* r r)) (- (- (+ 3 (/ 2 (* r r))) (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (- 1 v))) 9/2) (* (* -1/8 (* r r)) (/ (* (* (+ (* -2 v) 3) w) w) (- 1 v))) (* (* (* -1/4 (* r r)) w) w) (* (* -1/4 (* r r)) w) (- (- (+ 3 (/ 2 (* r r))) (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (- 1 v))) 9/2) (/ (/ 2 r) r) (/ 2 r) (- (- (+ 3 (/ 2 (* r r))) (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (- 1 v))) 9/2) (* (* -1/8 (* r r)) (/ (* (* (+ (* -2 v) 3) w) w) (- 1 v))) (* (* (* (- (/ 1/8 v) 1/4) w) w) (* r r)) (* (* (- (/ 1/8 v) 1/4) w) w) (* (* (/ w (- 1 v)) (* (+ (* -2 v) 3) w)) (* -1/8 r)) (- (- (+ 3 (/ 2 (* r r))) (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (- 1 v))) 9/2) (* (* (* (/ w (- 1 v)) (* (+ (* -2 v) 3) w)) (* -1/8 r)) r) (* (/ w (- 1 v)) (* (+ (* -2 v) 3) w)) (+ (* (* (* (* 1/8 (+ (* -2 v) 3)) w) (* r w)) (/ r (- 1 v))) 9/2) (* (* (* 1/8 (+ (* -2 v) 3)) w) (* r w)) (* (* 1/8 (+ (* -2 v) 3)) w) (* (- (/ 1/8 v) 1/4) w))
235.0ms	t	@	0	((* (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) 7/8) (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) 1/8)) (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) 7/8) (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) 1/8) (- (* 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 t) 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) (/ (sqrt (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)) (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -1/2)) (sqrt (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)) (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -1/2) (pow (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) 1/8) 8) (* (pow (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -1) -1/2) (sqrt (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000))) (pow (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -1) -1/2) (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -1))
137.0ms	t	@	inf	((* (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) 7/8) (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) 1/8)) (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) 7/8) (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) 1/8) (- (* 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 t) 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) (/ (sqrt (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)) (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -1/2)) (sqrt (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)) (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -1/2) (pow (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) 1/8) 8) (* (pow (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -1) -1/2) (sqrt (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000))) (pow (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -1) -1/2) (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -1))
134.0ms	t	@	-inf	((* (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) 7/8) (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) 1/8)) (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) 7/8) (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) 1/8) (- (* 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 t) 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) (/ (sqrt (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)) (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -1/2)) (sqrt (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)) (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -1/2) (pow (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) 1/8) 8) (* (pow (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -1) -1/2) (sqrt (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000))) (pow (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -1) -1/2) (pow (+ (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) -1))
92.0ms	x	@	-inf	((/ (- x (sin x)) (tan x)) (/ (* x x) (/ 1 (+ (* -23/360 (* x x)) 1/6))) (* x x) (/ 1 (+ (* -23/360 (* x x)) 1/6)) (/ (- x (sin x)) (tan x)) (/ (* x x) (/ 1 (+ (* -23/360 (* x x)) 1/6))) (/ 1 (+ (* -23/360 (* x x)) 1/6)) (/ x (/ 1 (+ (* -23/360 (* x x)) 1/6))) (/ (- x (sin x)) (tan x)) (* (/ x (/ 1 (+ (* -23/360 (* x x)) 1/6))) x) (/ 1 (+ (* -23/360 (* x x)) 1/6)) (* (* 1/6 (* x x)) x) (/ (- x (sin x)) (tan x)) (- x (sin x)) (* 1/6 (* x x)) (/ (- x (sin x)) (tan x)) (* (* (+ (* 529/129600 (pow x 4)) -1/36) x) (/ x (+ (* -23/360 (* x x)) -1/6))) (* (+ (* 529/129600 (pow x 4)) -1/36) x) (+ (* 529/129600 (pow x 4)) -1/36) (/ x (+ (* -23/360 (* x x)) -1/6)))

analyze4.2s (1.4%)

Memory

93.6MiB live, 4 263.2MiB allocated

Algorithm

43×	search
2×	random

Search

Probability	Valid	Unknown	Precondition	Infinite	Domain	Can't	Iter
0%	0%	54.5%	45.5%	0%	0%	0%	0
21.4%	11.7%	42.9%	45.5%	0%	0%	0%	1
37.4%	20.4%	34.1%	45.5%	0%	0%	0%	2
48.7%	26.2%	27.7%	45.5%	0%	0.6%	0%	3
57.7%	30.7%	22.6%	45.5%	0%	1.2%	0%	4
71.2%	37.7%	15.3%	45.5%	0%	1.6%	0%	5
72.9%	38.4%	14.3%	45.5%	0%	1.8%	0%	6
77.9%	40.7%	11.6%	45.5%	0%	2.2%	0%	7
81.5%	42.6%	9.7%	45.5%	0%	2.3%	0%	8
84.1%	43.8%	8.3%	45.5%	0%	2.5%	0%	9
86.2%	44.6%	7.2%	45.5%	0%	2.7%	0%	10
88.2%	45.6%	6.1%	45.5%	0%	2.8%	0%	11
89.1%	45.9%	5.6%	45.5%	0%	2.9%	0%	12

Compiler

Compiled 1 402 to 721 computations (48.6% saved)

bsearch3.3s (1.1%)

Memory

-73.4MiB live, 3 052.7MiB allocated

Algorithm

168×	binary-search
124×	left-value

Stop Event

156×	narrow-enough
12×	predicate-same

Samples

1.1s	10 046×	0	valid
244.0ms	923×	1	valid
133.0ms	403×	2	valid
93.0ms	901×	0	invalid
7.0ms	20×	3	valid
1.0ms	5×	0	exit

Compiler

Compiled 133 007 to 67 592 computations (49.2% saved)

Precisions

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

ival-mult: 435.0ms (35.4% of total)

ival-add: 200.0ms (16.3% of total)

ival-div: 169.0ms (13.7% of total)

ival-sub: 164.0ms (13.3% of total)

ival-pow: 109.0ms (8.9% of total)

adjust: 44.0ms (3.6% of total)

ival-neg: 33.0ms (2.7% of total)

ival-sqrt: 26.0ms (2.1% of total)

ival-exp: 19.0ms (1.5% of total)

ival-true: 10.0ms (0.8% of total)

exact: 10.0ms (0.8% of total)

ival-assert: 5.0ms (0.4% of total)

const: 3.0ms (0.2% of total)

ival-expm1: 2.0ms (0.2% of total)

ival-pi: 1.0ms (0.1% of total)

start2.0ms (0%)

Memory: 4.2MiB live, 4.2MiB allocated

end0.0ms (0%)

Memory: 0.6MiB live, 0.6MiB allocated

sample1.2min (23.6%)

simplify54.0s (17.7%)

soundness45.6s (15%)

rewrite40.6s (13.3%)

localize23.5s (7.7%)

eval20.5s (6.7%)

preprocess11.2s (3.7%)

explain10.8s (3.5%)

regimes8.3s (2.7%)

prune6.2s (2%)

series4.6s (1.5%)

analyze4.2s (1.4%)

bsearch3.3s (1.1%)

start2.0ms (0%)

end0.0ms (0%)

Profiling