Herbie run

Date:Thursday, May 29th, 2025
Commit:3faf5b03 on fighting-unsoundness
Seed:2025149
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:37 811.3 MB

Time bar (total: 31.7s)

sample9.6s (30.2%)

Memory
280.0MiB live, 11 249.2MiB allocated; 5.2s collecting garbage
Samples
5.3s70 097×0valid
998.0ms4 198×2valid
193.0ms1 918×0invalid
1.0ms1valid
Precisions
Click to see histograms. Total time spent on operations: 3.7s
ival-sqrt: 878.0ms (23.8% of total)
ival-mult!: 757.0ms (20.5% of total)
ival-div!: 575.0ms (15.6% of total)
ival-fabs: 386.0ms (10.5% of total)
ival-sub!: 290.0ms (7.9% of total)
ival-neg: 266.0ms (7.2% of total)
ival-log: 144.0ms (3.9% of total)
ival-exp: 140.0ms (3.8% of total)
ival-add!: 135.0ms (3.7% of total)
adjust: 116.0ms (3.1% of total)
ival-if: 4.0ms (0.1% of total)
ival->=: 3.0ms (0.1% of total)
Bogosity

rewrite9.1s (28.6%)

Memory
-55.9MiB live, 10 092.8MiB allocated; 2.9s collecting garbage
Stop Event
34×saturated
33×node-limit
32×iter-limit
Counts
755 → 30 420

eval5.0s (15.7%)

Memory
-20.8MiB live, 7 019.9MiB allocated; 1.5s collecting garbage
Compiler

Compiled 379 476 to 112 030 computations (70.5% saved)

series1.7s (5.5%)

Memory
218.9MiB live, 2 487.1MiB allocated; 456ms collecting garbage
Stop Event
33×iter-limit
Counts
755 → 3 247
Calls

192 calls:

TimeVariablePointExpression
26.0ms
b
@-inf
((if (>= b 0) (/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a))) (>= b 0) b 0 (/ (* 2 c) (- (neg b) (sqrt (- (* b b) (* (* 4 a) c))))) (* 2 c) 2 c (- (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 (/ (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a)) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))) (* 2 a))
25.0ms
y
@inf
((fabs (/ (+ (* z x) (- -4 x)) y)) (/ (+ (* z x) (- -4 x)) y) (+ (* z x) (- -4 x)) (- -4 x) -4 x y (fabs (/ (+ (* z x) (- -4 x)) y)) (/ (+ (* z x) (- -4 x)) y) (+ (* z x) (- -4 x)) (* x z) z (fabs (- (/ (+ x 4) y) (* (/ x y) z))) (- (/ (+ x 4) y) (* (/ x y) z)) (* (/ (neg z) y) x) (/ (neg z) y) (neg z) (fabs (/ (- (* x z) (+ x 4)) y)) (/ (- (* x z) (+ x 4)) y) (- (* x z) (+ x 4)) (+ x 4) 4 (fabs (+ (* (/ (- z 1) y) x) (/ -4 y))) (+ (* (/ (- z 1) y) x) (/ -4 y)) (/ (- z 1) y) (/ z y) (/ -4 y))
24.0ms
x
@0
((log (/ x (- 1 x))) (/ x (- 1 x)) x (- 1 x) 1 (neg (log (- (/ 1 x) 1))) (/ -1 x) -1 (neg (log (- (/ 1 x) 1))) (log x) (neg (log (- (/ 1 x) 1))) (- x (* -1 (log x))) (* -1 (log x)) (neg (log (- (/ x (* x x)) 1))) (log (- (/ x (* x x)) 1)) (- (/ x (* x x)) 1) (/ x (* x x)) (* x x))
23.0ms
x
@inf
((neg (log (- (/ 1 x) 1))) (+ (log x) x) (log x) x (log (/ x (- 1 x))) (/ x (- 1 x)) (* x (+ 1 x)) (+ 1 x) 1)
22.0ms
c
@-inf
((if (>= b 0) (/ (+ (/ (sqrt (+ (* (* -4 c) a) (* b b))) a) (/ b a)) -2) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (>= b 0) b 0 (/ (+ (/ (sqrt (+ (* (* -4 c) a) (* b b))) a) (/ b a)) -2) (+ (/ (sqrt (+ (* (* -4 c) a) (* b b))) a) (/ b a)) (/ (sqrt (+ (* (* -4 c) a) (* b b))) a) (sqrt (+ (* (* -4 c) a) (* b b))) (+ (* (* -4 c) a) (* b b)) (* -4 c) -4 c a (* b b) (/ b a) -2 (/ (* 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)) (* (* 4 a) c) (* 4 a) 4 (if (>= b 0) (* (/ -1/2 a) (+ (sqrt (- (* b b) (* (* 4 a) c))) b)) (/ (+ c c) (- (sqrt (- (* b b) (* (* 4 a) c))) b))) (* (/ -1/2 a) (+ (sqrt (- (* b b) (* (* 4 a) c))) b)) (* -1/2 (/ (sqrt (neg (* 4 (* a c)))) a)) -1/2 (/ (sqrt (neg (* 4 (* a c)))) a) (sqrt (neg (* 4 (* a c)))) (neg (* 4 (* a c))) (* 4 (* a c)) (* a c) (/ (+ c c) (- (sqrt (- (* b b) (* (* 4 a) c))) b)) (+ c c) (- (sqrt (- (* b b) (* (* 4 a) c))) b) (sqrt (- (* b b) (* (* 4 a) c))) (- (* b b) (* (* 4 a) c)) (* (* c a) -4) (* c a) (if (>= b 0) (* (+ b (sqrt (+ (* (* c -4) a) (* b b)))) (/ -1/2 a)) (/ (+ c c) (- (sqrt (+ (* (* c -4) a) (* b b))) b))) (* (+ b (sqrt (+ (* (* c -4) a) (* b b)))) (/ -1/2 a)) (+ b (sqrt (+ (* (* c -4) a) (* b b)))) (sqrt (+ (* (* c -4) a) (* b b))) (* c (sqrt (* -4 (/ a c)))) (sqrt (* -4 (/ a c))) (* -4 (/ a c)) (/ a c) (/ -1/2 a) (/ (+ c c) (- (sqrt (+ (* (* c -4) a) (* b b))) b)) (- (sqrt (+ (* (* c -4) a) (* b b))) b) (if (>= b 0) (/ (- (neg b) (sqrt (+ (* (* -4 a) c) (* b b)))) (* 2 a)) (* (/ -2 (- b (sqrt (+ (* (* c a) -4) (* b b))))) c)) (/ (- (neg b) (sqrt (+ (* (* -4 a) c) (* b b)))) (* 2 a)) (- (neg b) (sqrt (+ (* (* -4 a) c) (* b b)))) (sqrt (+ (* (* -4 a) c) (* b b))) (+ (* (* -4 a) c) (* b b)) (* -4 a) (* 2 a) (* (/ -2 (- b (sqrt (+ (* (* c a) -4) (* b b))))) c) (/ -2 (- b (sqrt (+ (* (* c a) -4) (* b b))))) (- b (sqrt (+ (* (* c a) -4) (* b b)))) (sqrt (+ (* (* c a) -4) (* b b))) (+ (* (* c a) -4) (* b b)) (if (>= b 0) (/ (* (E) (* (+ b (sqrt (+ (* (* c -4) a) (* b b)))) (/ -1/2 a))) (E)) (/ (* 2 c) (+ (neg b) (sqrt (- (* b b) (* (* 4 a) c)))))) (/ (* (E) (* (+ b (sqrt (+ (* (* c -4) a) (* b b)))) (/ -1/2 a))) (E)) (* (E) (* (+ b (sqrt (+ (* (* c -4) a) (* b b)))) (/ -1/2 a))) (E) (* (+ b (sqrt (+ (* (* c -4) a) (* b b)))) (/ -1/2 a)) (+ b (sqrt (+ (* (* c -4) a) (* b b)))) (sqrt (+ (* (* c -4) a) (* b b))) (sqrt (* -4 (* a c))) (* -4 (* a c)))

preprocess1.6s (4.9%)

Memory
-196.9MiB live, 1 266.2MiB allocated; 1.0s collecting garbage
Stop Event
node-limit
iter-limit
Compiler

Compiled 1 664 to 1 262 computations (24.2% saved)

derivations1.5s (4.6%)

Memory
-2.5MiB live, 1 029.5MiB allocated; 194ms collecting garbage
Stop Event
done
fuel
Compiler

Compiled 919 to 580 computations (36.9% saved)

prune1.4s (4.5%)

Memory
205.1MiB live, 1 889.7MiB allocated; 1.1s collecting garbage
Counts
31 015 → 335
Compiler

Compiled 14 991 to 12 450 computations (17% saved)

regimes759.0ms (2.4%)

Memory
-36.2MiB live, 1 378.9MiB allocated; 168ms collecting garbage
Counts
800 → 115
Calls

26 calls:

193.0ms
b
60.0ms
x
52.0ms
a
49.0ms
c
35.0ms
(-.f64 (/.f64 #s(literal 1 binary64) x) #s(literal 1 binary64))
Compiler

Compiled 744 to 775 computations (-4.2% saved)

analyze657.0ms (2.1%)

Memory
-20.1MiB live, 762.8MiB allocated; 171ms collecting garbage
Algorithm
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)

bsearch485.0ms (1.5%)

Memory
26.8MiB live, 634.3MiB allocated; 121ms collecting garbage
Algorithm
52×binary-search
left-value
Stop Event
48×narrow-enough
predicate-same
Samples
192.0ms2 544×0valid
19.0ms246×0invalid
11.0ms96×2valid
Compiler

Compiled 24 535 to 22 070 computations (10% saved)

Precisions
Click to see histograms. Total time spent on operations: 136.0ms
ival-mult!: 41.0ms (30.2% of total)
ival-div!: 34.0ms (25% of total)
ival-sqrt: 14.0ms (10.3% of total)
ival-sub!: 10.0ms (7.4% of total)
ival->=: 9.0ms (6.6% of total)
ival-if: 8.0ms (5.9% of total)
ival-neg: 8.0ms (5.9% of total)
ival-add!: 6.0ms (4.4% of total)
adjust: 3.0ms (2.2% of total)
ival-fabs: 3.0ms (2.2% of total)

start0.0ms (0%)

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

end0.0ms (0%)

Memory
0.2MiB live, 0.1MiB allocated; 0ms collecting garbage

Profiling

Loading profile data...