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: | 1 388 015.8 MB |
Time bar (total: 18.2min)
| 2.8min | 2 144 767× | 0 | valid |
| 19.9s | 69 435× | 1 | valid |
| 11.7s | 64 058× | 0 | invalid |
| 1.5s | 6 039× | 2 | valid |
| 1.1s | 1 123× | 5 | exit |
| 492.0ms | 1 843× | 1 | invalid |
| 247.0ms | 621× | 3 | valid |
| 192.0ms | 367× | 4 | exit |
| 94.0ms | 28× | 1 | exit |
| 1.0ms | 2× | 4 | valid |
ival-mult!: 38.9s (34.6% of total)ival-sub!: 15.1s (13.4% of total)ival-add!: 11.9s (10.5% of total)ival-div!: 11.7s (10.4% of total)ival-log: 9.4s (8.3% of total)ival-sqrt: 9.1s (8.1% of total)adjust: 4.6s (4.1% of total)ival-sin: 4.2s (3.8% of total)ival-cos: 3.5s (3.1% of total)ival-exp: 2.3s (2% of total)ival-cosh: 537.0ms (0.5% of total)ival-fabs: 281.0ms (0.2% of total)ival-tan: 255.0ms (0.2% of total)ival-acos: 236.0ms (0.2% of total)ival-sinh: 191.0ms (0.2% of total)ival-hypot: 185.0ms (0.2% of total)ival-tanh: 130.0ms (0.1% of total)| 954× | saturated |
| 945× | iter-limit |
| 937× | node-limit |
Compiled 9 210 426 to 2 803 189 computations (69.6% saved)
| 941× | iter-limit |
9033 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 2.4s | y | @ | inf | ((+ (* x y) (* z t)) (* x y) x y (* z t) z t) |
| 985.0ms | y | @ | 0 | ((neg (+ (* (log (/ y x)) x) z)) (+ (* (log (/ y x)) x) z) (log (/ y x)) (/ y x) y x z (- (* x (log (/ x y))) z) (* -1 z) -1 (- (* x (log (/ x y))) z) (* x (log (/ x y))) (log (/ x y)) (/ x y) (- (* x (log (/ x y))) z) (* z (- (/ (* x (log (/ x y))) z) 1)) (- (/ (* x (log (/ x y))) z) 1) (/ (* x (log (/ x y))) z) 1 (- (* x (log (/ x y))) z) (* x (log (/ x y))) (log (/ x y)) (+ (log x) (* -1 (log y))) (log x) (* -1 (log y)) (log y)) |
| 691.0ms | t | @ | -inf | ((+ (* (/ (- z y) (- (- t z) -1)) a) x) (/ (- z y) (- (- t z) -1)) (- z y) (- z y) z y (- (- t z) -1) (- t z) t -1 a x (- x (/ (- y z) (/ (+ (- t z) 1) a))) (/ (- y z) (/ (+ (- t z) 1) a)) (/ (* a y) (+ 1 t)) (* y (/ a t)) (/ a t) (+ (* (/ (- z y) (- (- t z) -1)) a) x) (/ (- z y) (- (- t z) -1)) (/ (- z y) t) (- x (/ (- y z) (/ (+ (- t z) 1) a))) (/ (- y z) (/ (+ (- t z) 1) a)) (/ (* a (- y z)) (- 1 z)) (* (/ y (- 1 z)) a) (/ y (- 1 z)) (- 1 z) 1 (+ (* (- z y) (/ a (- (- t -1) z))) x) (- z y) (/ a (- (- t -1) z)) (- (- t -1) z) (- t -1)) |
| 680.0ms | x | @ | -inf | ((+ (* y (* z (/ (+ (* (+ (* (+ (* 313060547623/100000000000 z) 55833770631/5000000000) z) t) z) a) (+ (* (+ (* (+ (* (- z -15234687407/1000000000) z) 314690115749/10000000000) z) 119400905721/10000000000) z) 607771387771/1000000000000)))) (+ (* b (/ y (+ (* (+ (* (+ (* (- z -15234687407/1000000000) z) 314690115749/10000000000) z) 119400905721/10000000000) z) 607771387771/1000000000000))) x)) y (* z (/ (+ (* (+ (* (+ (* 313060547623/100000000000 z) 55833770631/5000000000) z) t) z) a) (+ (* (+ (* (+ (* (- z -15234687407/1000000000) z) 314690115749/10000000000) z) 119400905721/10000000000) z) 607771387771/1000000000000))) 313060547623/100000000000 (+ (* b (/ y (+ (* (+ (* (+ (* (- z -15234687407/1000000000) z) 314690115749/10000000000) z) 119400905721/10000000000) z) 607771387771/1000000000000))) x) b (/ y (+ (* (+ (* (+ (* (- z -15234687407/1000000000) z) 314690115749/10000000000) z) 119400905721/10000000000) z) 607771387771/1000000000000)) (+ (* (+ (* (+ (* (- z -15234687407/1000000000) z) 314690115749/10000000000) z) 119400905721/10000000000) z) 607771387771/1000000000000) (+ (* (+ (* (- z -15234687407/1000000000) z) 314690115749/10000000000) z) 119400905721/10000000000) (+ (* (- z -15234687407/1000000000) z) 314690115749/10000000000) (- z -15234687407/1000000000) z -15234687407/1000000000 314690115749/10000000000 119400905721/10000000000 607771387771/1000000000000 x (+ x (/ (* y (+ (* (+ (* (+ (* (+ (* z 313060547623/100000000000) 55833770631/5000000000) z) t) z) a) z) b)) (+ (* (+ (* (+ (* (+ z 15234687407/1000000000) z) 314690115749/10000000000) z) 119400905721/10000000000) z) 607771387771/1000000000000))) (/ (* y (+ (* (+ (* (+ (* (+ (* z 313060547623/100000000000) 55833770631/5000000000) z) t) z) a) z) b)) (+ (* (+ (* (+ (* (+ z 15234687407/1000000000) z) 314690115749/10000000000) z) 119400905721/10000000000) z) 607771387771/1000000000000)) (* 1000000000000/607771387771 (* b y)) 1000000000000/607771387771 (* b y) (+ x (/ (* y (+ (* (+ (* (+ (* (+ (* z 313060547623/100000000000) 55833770631/5000000000) z) t) z) a) z) b)) (+ (* (+ (* (+ (* (+ z 15234687407/1000000000) z) 314690115749/10000000000) z) 119400905721/10000000000) z) 607771387771/1000000000000))) (* (/ y (+ (* (+ (* (+ (* (- z -15234687407/1000000000) z) 314690115749/10000000000) z) 119400905721/10000000000) z) 607771387771/1000000000000)) b) (+ (* (/ (+ (* (+ (* (+ (* (+ (* z 313060547623/100000000000) 55833770631/5000000000) z) t) z) a) z) b) (+ (* (+ (* (+ (* (- z -15234687407/1000000000) z) 314690115749/10000000000) z) 119400905721/10000000000) z) 607771387771/1000000000000)) y) x) (/ (+ (* (+ (* (+ (* (+ (* z 313060547623/100000000000) 55833770631/5000000000) z) t) z) a) z) b) (+ (* (+ (* (+ (* (- z -15234687407/1000000000) z) 314690115749/10000000000) z) 119400905721/10000000000) z) 607771387771/1000000000000)) (+ (* (+ (* (+ (* (+ (* z 313060547623/100000000000) 55833770631/5000000000) z) t) z) a) z) b) (+ (* (+ (* (+ (* z 313060547623/100000000000) 55833770631/5000000000) z) t) z) a) (+ (* (+ (* z 313060547623/100000000000) 55833770631/5000000000) z) t) t a (+ x (/ (* y (+ (* (+ (* (+ (* (+ (* z 313060547623/100000000000) 55833770631/5000000000) z) t) z) a) z) b)) (+ (* (+ (* (+ (* (+ z 15234687407/1000000000) z) 314690115749/10000000000) z) 119400905721/10000000000) z) 607771387771/1000000000000))) (/ (* y (+ (* (+ (* (+ (* (+ (* z 313060547623/100000000000) 55833770631/5000000000) z) t) z) a) z) b)) (+ (* (+ (* (+ (* (+ z 15234687407/1000000000) z) 314690115749/10000000000) z) 119400905721/10000000000) z) 607771387771/1000000000000)) (+ (* -1 (/ (- (+ (* -55833770631/5000000000 y) (* -1 (/ (- (* t y) (+ (* -15234687407/1000000000 (- (* -55833770631/5000000000 y) (* -4769379582500641883561/100000000000000000000 y))) (* 98517059967927196814627/1000000000000000000000 y))) z))) (* -4769379582500641883561/100000000000000000000 y)) z)) (* 313060547623/100000000000 y)) -1 (/ (- (+ (* -55833770631/5000000000 y) (* -1 (/ (- (* t y) (+ (* -15234687407/1000000000 (- (* -55833770631/5000000000 y) (* -4769379582500641883561/100000000000000000000 y))) (* 98517059967927196814627/1000000000000000000000 y))) z))) (* -4769379582500641883561/100000000000000000000 y)) z) (- (+ (* -55833770631/5000000000 y) (* -1 (/ (- (* t y) (+ (* -15234687407/1000000000 (- (* -55833770631/5000000000 y) (* -4769379582500641883561/100000000000000000000 y))) (* 98517059967927196814627/1000000000000000000000 y))) z))) (* -4769379582500641883561/100000000000000000000 y)) (+ (* -55833770631/5000000000 y) (* -1 (/ (- (* t y) (+ (* -15234687407/1000000000 (- (* -55833770631/5000000000 y) (* -4769379582500641883561/100000000000000000000 y))) (* 98517059967927196814627/1000000000000000000000 y))) z))) -55833770631/5000000000 (* -1 (/ (- (* t y) (+ (* -15234687407/1000000000 (- (* -55833770631/5000000000 y) (* -4769379582500641883561/100000000000000000000 y))) (* 98517059967927196814627/1000000000000000000000 y))) z)) (/ (- (* t y) (+ (* -15234687407/1000000000 (- (* -55833770631/5000000000 y) (* -4769379582500641883561/100000000000000000000 y))) (* 98517059967927196814627/1000000000000000000000 y))) z) (- (* t y) (+ (* -15234687407/1000000000 (- (* -55833770631/5000000000 y) (* -4769379582500641883561/100000000000000000000 y))) (* 98517059967927196814627/1000000000000000000000 y))) (* t y) (+ (* -15234687407/1000000000 (- (* -55833770631/5000000000 y) (* -4769379582500641883561/100000000000000000000 y))) (* 98517059967927196814627/1000000000000000000000 y)) (- (* -55833770631/5000000000 y) (* -4769379582500641883561/100000000000000000000 y)) (* -55833770631/5000000000 y) (* -4769379582500641883561/100000000000000000000 y) -4769379582500641883561/100000000000000000000 (* 98517059967927196814627/1000000000000000000000 y) 98517059967927196814627/1000000000000000000000 (* 313060547623/100000000000 y)) |
| 596.0ms | z | @ | inf | ((- (+ (* (log t) (- a 1/2)) (log (+ x y))) (- t (log z))) (+ (* (log t) (- a 1/2)) (log (+ x y))) (log t) t (- a 1/2) a 1/2 (log (+ x y)) (+ x y) y (- t (log z)) (log z) z (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (neg t) (- (+ (* (log t) (- a 1/2)) (log (* z (+ y x)))) t) (+ (* (log t) (- a 1/2)) (log (* z (+ y x)))) (log (* z (+ y x))) (* z (+ y x)) (* x z) x (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (+ (log (+ x y)) (log z)) t) (+ (log (+ x y)) (log z)) (log (+ x y)) (log x) (* (- a 1/2) (log t)) (- a 1/2) -1/2 (- (log (+ x y)) (+ (* (- 1/2 a) (log t)) (- t (log z)))) (+ (* (- 1/2 a) (log t)) (- t (log z))) (- 1/2 a)) |
507 calls:
| 9.4s | x |
| 9.1s | y |
| 7.8s | z |
| 4.2s | t |
| 3.7s | a |
Compiled 31 268 to 53 227 computations (-70.2% saved)
| 254× | node-limit |
| 15× | saturated |
Compiled 143 996 to 120 464 computations (16.3% saved)
Compiled 425 975 to 376 964 computations (11.5% saved)
| 152× | fuel |
| 117× | done |
Compiled 26 349 to 17 122 computations (35% saved)
| 1 569× | binary-search |
| 864× | left-value |
| 1 532× | narrow-enough |
| 37× | predicate-same |
| 14.4s | 128 678× | 0 | valid |
| 833.0ms | 4 025× | 1 | valid |
| 378.0ms | 3 365× | 0 | invalid |
| 75.0ms | 445× | 1 | invalid |
| 31.0ms | 140× | 2 | valid |
| 1.0ms | 5× | 3 | valid |
Compiled 610 378 to 620 995 computations (-1.7% saved)
ival-mult!: 5.4s (55.5% of total)ival-sub!: 1.2s (12.6% of total)ival-add!: 729.0ms (7.5% of total)ival-log: 688.0ms (7.1% of total)ival-div!: 584.0ms (6% of total)ival-cos: 271.0ms (2.8% of total)ival-sqrt: 240.0ms (2.5% of total)adjust: 235.0ms (2.4% of total)ival-sin: 225.0ms (2.3% of total)ival-exp: 129.0ms (1.3% of total)ival-tanh: 9.0ms (0.1% of total)ival-sinh: 3.0ms (0% of total)| 269× | search |
| Probability | Valid | Unknown | Precondition | Infinite | Domain | Can't | Iter |
|---|---|---|---|---|---|---|---|
| 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 |
Compiled 3 462 to 2 977 computations (14% saved)
Loading profile data...