Herbie run

Date:Wednesday, April 16th, 2025
Commit:5565a39e on main
Seed:2025106
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:999 626.3 MB

Time bar (total: 13.5min)

sample4.6min (34.3%)

Memory
4 357.6MiB live, 341 786.5MiB allocated; 1.7min collecting garbage
Samples
2.7min2 144 638×0valid
17.5s69 527×1valid
7.2s64 681×0invalid
1.3s5 999×2valid
719.0ms1 205×5exit
315.0ms1 705×1invalid
202.0ms382×4exit
182.0ms696×3valid
3.0ms26×1exit
1.0ms4valid
Precisions
Click to see histograms. Total time spent on operations: 1.6min
ival-mult!: 38.9s (40% of total)
ival-div!: 10.8s (11.1% of total)
ival-add!: 9.7s (10% of total)
ival-sub!: 9.6s (9.9% of total)
ival-log: 8.6s (8.8% of total)
adjust: 4.6s (4.8% of total)
ival-sqrt: 4.6s (4.7% of total)
ival-sin: 3.9s (4.1% of total)
ival-cos: 3.0s (3.1% of total)
ival-exp: 1.8s (1.9% of total)
ival-fabs: 287.0ms (0.3% of total)
ival-sinh: 280.0ms (0.3% of total)
ival-cosh: 266.0ms (0.3% of total)
ival-acos: 238.0ms (0.2% of total)
ival-hypot: 213.0ms (0.2% of total)
ival-tan: 212.0ms (0.2% of total)
ival-tanh: 108.0ms (0.1% of total)
Bogosity

rewrite3.1min (22.8%)

Memory
3 458.3MiB live, 202 414.9MiB allocated; 53.7s collecting garbage
Stop Event
2 241×iter-limit
853×node-limit
72×unsound
12×saturated
Counts
123 549 → 225 213

regimes1.1min (8.3%)

Memory
-77.7MiB live, 93 463.9MiB allocated; 23.1s collecting garbage
Counts
30 608 → 4 606
Calls

512 calls:

9.1s
x
8.2s
y
5.9s
z
5.4s
(+.f64 (*.f64 x y) (*.f64 z t))
4.0s
t
Compiler

Compiled 36 898 to 55 797 computations (-51.2% saved)

derivations1.0min (7.4%)

Memory
-865.9MiB live, 57 171.3MiB allocated; 12.3s collecting garbage
Stop Event
147×fuel
122×done
Compiler

Compiled 143 175 to 17 757 computations (87.6% saved)

series48.6s (6%)

Memory
3 967.4MiB live, 69 636.6MiB allocated; 13.3s collecting garbage
Counts
18 569 → 104 980
Calls

8925 calls:

TimeVariablePointExpression
826.0ms
a
@0
((+ (+ (+ x (* y z)) (* t a)) (* (* a z) b)) (+ (+ x (* y z)) (* t a)) (+ x (* y z)) x (* y z) y z (* t a) t a (* (* a z) b) (* a z) b)
740.0ms
x
@inf
((+ (* (log y) x) (- (* z (log (- 1 y))) t)) (log y) y x (- (* z (log (- 1 y))) t) (* z (log (- 1 y))) (* (+ (* (+ (* (+ (* -1/4 (* z y)) (* -1/3 z)) y) (* -1/2 z)) y) (neg z)) y) (+ (* (+ (* (+ (* -1/4 (* z y)) (* -1/3 z)) y) (* -1/2 z)) y) (neg z)) (+ (* (+ (* -1/4 (* z y)) (* -1/3 z)) y) (* -1/2 z)) (* (+ (* (+ (* 1/4 y) 1/3) y) 1/2) (neg z)) (+ (* (+ (* 1/4 y) 1/3) y) 1/2) (+ (* 1/4 y) 1/3) 1/4 1/3 1/2 (neg z) z t (- (+ (* x (log y)) (* z (log (- 1 y)))) t) (+ (* x (log y)) (* z (log (- 1 y)))) (+ (* (+ (* -1/2 (* z y)) (neg z)) y) (* (log y) x)) (* (+ (* -1/2 z) (/ (neg z) y)) (* y y)) (* (neg y) z) (neg y) (- (+ (* x (log y)) (* z (log (- 1 y)))) t) (+ (* x (log y)) (* z (log (- 1 y)))) (+ (* (+ (* -1/2 (* z y)) (neg z)) y) (* (log y) x)) (* (+ (* -1/2 z) (/ (neg z) y)) (* y y)) (+ (* -1/2 z) (/ (neg z) y)) (/ (neg z) y) (* y y) (- (+ (* x (log y)) (* z (log (- 1 y)))) t) (* (log y) x) (- (+ (* x (log y)) (* z (log (- 1 y)))) t) (+ (* x (log y)) (* z (log (- 1 y)))) (+ (* (neg y) z) (* (log y) x)) (* (+ (* (* x (/ (neg (log y)) y)) -1) (neg z)) y) (+ (* (* x (/ (neg (log y)) y)) -1) (neg z)) (* x (/ (neg (log y)) y)) (/ (neg (log y)) y) (neg (log y)) -1)
247.0ms
y
@-inf
((+ (* (log x) x) (* (neg x) (log y))) (log x) x (* (neg x) (log y)) (neg x) (log y) y (* x (- (log (neg x)) (log (neg y)))) (- (log (neg x)) (log (neg y))) (log (neg x)) (log (neg y)) (neg y) (+ (* (log (neg x)) x) (* (exp (* (log (log (/ -1 y))) 1)) x)) (* (exp (* (log (log (/ -1 y))) 1)) x) (exp (* (log (log (/ -1 y))) 1)) (* (log (log (/ -1 y))) 1) (log (log (/ -1 y))) (log (/ -1 y)) (/ -1 y) -1 1 (* x (- (/ (pow (log (neg x)) 2) (log (* x y))) (/ (pow (log (/ -1 y)) 2) (log (* x y))))) (- (/ (pow (log (neg x)) 2) (log (* x y))) (/ (pow (log (/ -1 y)) 2) (log (* x y)))) (/ (- (pow (log (neg x)) 2) (pow (log (neg y)) 2)) (+ (* (log (/ -1 x)) -1) (log (neg y)))) (- (pow (log (neg x)) 2) (pow (log (neg y)) 2)) (pow (log (neg x)) 2) 2 (pow (log (neg y)) 2) (+ (* (log (/ -1 x)) -1) (log (neg y))) (log (/ -1 x)) (/ -1 x) (* x (/ (- (* (pow (log x) 2) (log (* x y))) (* (log (* x y)) (pow (log y) 2))) (* (log (* x y)) (log (* x y))))) (/ (- (* (pow (log x) 2) (log (* x y))) (* (log (* x y)) (pow (log y) 2))) (* (log (* x y)) (log (* x y)))) (- (* (pow (log x) 2) (log (* x y))) (* (log (* x y)) (pow (log y) 2))) (* (pow (log x) 2) (log (* x y))) (pow (log x) 2) (log (* x y)) (* x y) (* (log (* x y)) (pow (log y) 2)) (pow (log y) 2) (* (log (* x y)) (log (* x y))))
211.0ms
x
@0
((* (neg x) (log (/ y x))) (neg x) x (log (/ y x)) (/ y x) y (* x (- (log x) (log y))) (- (log x) (log y)) (log x) (log y) (+ (* (log (neg x)) x) (* (neg (neg (log (/ -1 y)))) x)) (log (neg x)) (* (neg (neg (log (/ -1 y)))) x) (neg (neg (log (/ -1 y)))) (neg (log (/ -1 y))) (log (/ -1 y)) (/ -1 y) -1 (* x (- (/ (pow (log (neg x)) 2) (log (* x y))) (/ (pow (log (/ -1 y)) 2) (log (* x y))))) (- (/ (pow (log (neg x)) 2) (log (* x y))) (/ (pow (log (/ -1 y)) 2) (log (* x y)))) (/ (pow (log (neg x)) 2) (log (* x y))) (pow (log (neg x)) 2) 2 (log (* x y)) (* x y) (/ (pow (log (/ -1 y)) 2) (log (* x y))) (pow (log (/ -1 y)) 2) (/ (* (+ (pow (log (neg x)) 3) (pow (log (/ -1 y)) 3)) x) (+ (* (log (/ -1 y)) (neg (log (* y x)))) (pow (log (neg x)) 2))) (* (+ (pow (log (neg x)) 3) (pow (log (/ -1 y)) 3)) x) (+ (pow (log (neg x)) 3) (pow (log (/ -1 y)) 3)) (pow (log (neg x)) 3) 3 (pow (log (/ -1 y)) 3) (+ (* (log (/ -1 y)) (neg (log (* y x)))) (pow (log (neg x)) 2)) (neg (log (* y x))) (log (* y x)) (* y x))
205.0ms
x
@0
((- (* x (log (/ x y))) z) (* x (log (/ x y))) x (log (/ x y)) (/ x y) y z)

eval38.0s (4.7%)

Memory
266.3MiB live, 55 393.7MiB allocated; 14.3s collecting garbage
Compiler

Compiled 8 533 755 to 986 104 computations (88.4% saved)

explain36.0s (4.4%)

Memory
1 073.4MiB live, 52 466.0MiB allocated; 9.1s collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
log.f64#fsensitivity15710
/.f64#fo/n11710
sqrt.f64#foflow-rescue7350
-.f64#fcancellation5969
/.f64#fo/o5410
*.f64#fn*o5060
+.f64#fnan-rescue4980
-.f64#fnan-rescue4010
+.f64#fcancellation3770
cos.f64#fsensitivity3523
/.f64#fn/o3280
sin.f64#fsensitivity2300
/.f64#fu/n2250
*.f64#fn*u1720
/.f64#fn/u1560
cos.f64#foflow-rescue1170
tan.f64(tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))sensitivity1080
/.f64#fu/u1030
log.f64#foflow-rescue830
log.f64#fuflow-rescue590
sqrt.f64#fuflow-rescue430
exp.f64#fsensitivity285
sin.f64(sin.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))oflow-rescue250
(/.f64 x (*.f64 y #s(literal 2 binary64)))overflow25
tan.f64(tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))oflow-rescue250
(/.f64 x (*.f64 y #s(literal 2 binary64)))overflow25
*.f64#fo*u230
*.f64#fu*o50
Confusion
Predicted +Predicted -
+5887192
-172861057
Precision
0.7730794484569927
Recall
0.9684158578713604
Confusion?
Predicted +Predicted MaybePredicted -
+58871191
-17281561042
Precision?
0.7715895688638449
Recall?
0.9685803586116137
Freqs
test
numberfreq
061249
16842
2706
349
415
51
62
Total Confusion?
Predicted +Predicted MaybePredicted -
+13600
-20131
Precision?
0.9855072463768116
Recall?
1.0
Samples
10.4s130 332×0valid
1.7s1 328×2valid
1.6s5 970×1valid
62.0ms98×3valid
Compiler

Compiled 24 442 to 8 402 computations (65.6% saved)

Precisions
Click to see histograms. Total time spent on operations: 6.6s
ival-mult!: 2.4s (36.4% of total)
ival-log: 1.5s (22.2% of total)
ival-sub!: 539.0ms (8.2% of total)
ival-div!: 535.0ms (8.1% of total)
ival-add!: 441.0ms (6.7% of total)
adjust: 349.0ms (5.3% of total)
ival-sqrt: 229.0ms (3.5% of total)
ival-sin: 225.0ms (3.4% of total)
ival-cos: 211.0ms (3.2% of total)
ival-exp: 101.0ms (1.5% of total)
ival-hypot: 28.0ms (0.4% of total)
ival-tan: 17.0ms (0.3% of total)
ival-fabs: 16.0ms (0.2% of total)
ival-cosh: 13.0ms (0.2% of total)
ival-sinh: 10.0ms (0.2% of total)
ival-acos: 9.0ms (0.1% of total)
ival-tanh: 7.0ms (0.1% of total)

preprocess34.1s (4.2%)

Memory
-1 827.0MiB live, 41 420.5MiB allocated; 8.5s collecting garbage
Stop Event
174×node-limit
95×saturated
Compiler

Compiled 479 870 to 129 956 computations (72.9% saved)

bsearch25.7s (3.2%)

Memory
258.9MiB live, 34 032.5MiB allocated; 7.5s collecting garbage
Algorithm
1 637×binary-search
969×left-value
Stop Event
1 604×narrow-enough
33×predicate-same
Samples
12.8s132 619×0valid
943.0ms4 095×1valid
199.0ms2 510×0invalid
23.0ms92×1invalid
17.0ms132×2valid
3.0ms18×3valid
Compiler

Compiled 859 359 to 619 151 computations (28% saved)

Precisions
Click to see histograms. Total time spent on operations: 8.2s
ival-mult!: 3.3s (40.5% of total)
ival-sub!: 2.1s (25.3% of total)
ival-add!: 692.0ms (8.4% of total)
ival-div!: 538.0ms (6.6% of total)
ival-log: 389.0ms (4.7% of total)
ival-cos: 364.0ms (4.4% of total)
ival-sin: 309.0ms (3.8% of total)
adjust: 207.0ms (2.5% of total)
ival-exp: 145.0ms (1.8% of total)
ival-sqrt: 119.0ms (1.5% of total)
ival-tanh: 13.0ms (0.2% of total)
ival-fabs: 9.0ms (0.1% of total)
ival-sinh: 9.0ms (0.1% of total)
ival-cosh: 6.0ms (0.1% of total)

prune21.9s (2.7%)

Memory
-1 460.8MiB live, 30 132.6MiB allocated; 9.5s collecting garbage
Counts
221 572 → 12 374
Compiler

Compiled 783 911 to 426 024 computations (45.7% saved)

analyze16.4s (2%)

Memory
114.2MiB live, 21 683.4MiB allocated; 5.0s collecting garbage
Algorithm
269×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%99.9%0.1%0%0%0%0
46.8%46.8%53.1%0.1%0%0%0%1
50.5%50.1%49.2%0.1%0%0.6%0%2
58.6%57%40.3%0.1%0%2.6%0%3
65.2%62.7%33.5%0.1%0%3.6%0%4
71.2%68.2%27.5%0.1%0%4.1%0%5
75.9%72.3%23%0.1%0%4.6%0%6
79.8%75.6%19.1%0.1%0%5.1%0%7
81.7%77%17.3%0.1%0%5.6%0%8
84.3%79.3%14.7%0.1%0%5.9%0%9
85.9%80.5%13.2%0.1%0%6.2%0%10
88.5%82.8%10.8%0.1%0%6.2%0%11
89.6%83.6%9.8%0.1%0%6.5%0%12
Compiler

Compiled 3 462 to 2 977 computations (14% saved)

start9.0ms (0%)

Memory
-39.5MiB live, 19.3MiB allocated; 0ms collecting garbage

end2.0ms (0%)

Memory
5.3MiB live, 4.9MiB allocated; 0ms collecting garbage

Profiling

Loading profile data...