This benchmark randomly takes forever to execute:
import stainless.lang._
import stainless.math.wrapping
object Test {
def safeAdd(x: Int, y: Int): Int = {
require(x >= 0 && y >= 0)
if wrapping(x + y) < 0 then 2147483647 else wrapping(x + y)
}.ensuring(v => v >= 0)
def sumNat(n: Int): Int = {
if n <= 0 then
0
else
safeAdd(sumNat(n - 1), n)
}.ensuring(v => v >= 0)
}[info] # JMH version: 1.37 21:39:01 [70/1802]
[info] # VM version: JDK 17.0.19, OpenJDK 64-Bit Server VM, 17.0.19+10-1-24.04.2-Ubuntu
[info] # VM invoker: /usr/lib/jvm/java-17-openjdk-amd64/bin/java
[info] # VM options: -XX:+PrintCommandLineFlags -Xms8G -Xmx8G
[info] # Blackhole mode: compiler (auto-detected, use -Djmh.blackhole.autoDetect=false to disable)
[info] # Warmup: 150 iterations, single-shot each
[info] # Measurement: 20 iterations, single-shot each
[info] # Timeout: 10 min per iteration
[info] # Threads: 1 thread
[info] # Benchmark mode: Single shot invocation time
[info] # Benchmark: bench.StainlessVerifyBenchmarks.sumnat
[info] # Run progress: 88.89% complete, ETA 00:05:04
[info] # Fork: 1 of 1
[info] -XX:CompileCommandFile=/tmp/jmh16406379732164420854compilecommand -XX:ConcGCThreads=16 -XX:G1ConcRefinementThreads=63 -XX:GCDr
ainStackTargetSize=64 -XX:InitialHeapSize=8589934592 -XX:MarkStackSize=4194304 -XX:MaxHeapSize=8589934592 -XX:MinHeapSize=8589934592
-XX:+PrintCommandLineFlags -XX:ReservedCodeCacheSize=251658240 -XX:+SegmentedCodeCache -XX:-THPStackMitigation -XX:+UnlockDiagnosticV
MOptions -XX:+UnlockExperimentalVMOptions -XX:+UseCompressedClassPointers -XX:+UseCompressedOops -XX:+UseG1GC
[info] # Warmup Iteration 1: 2873.736 ms/op
[info] # Warmup Iteration 2: 724.837 ms/op
[info] # Warmup Iteration 3: 687.767 ms/op
[info] # Warmup Iteration 4: 714.774 ms/op
[info] # Warmup Iteration 5: 617.537 ms/op
[info] # Warmup Iteration 6: 575.122 ms/op
[info] # Warmup Iteration 7: 552.685 ms/op
[info] # Warmup Iteration 8: 516.919 ms/op
[info] # Warmup Iteration 9: 518.927 ms/op
[info] # Warmup Iteration 10: 561.446 ms/op
[info] # Warmup Iteration 11: 531.179 ms/op
[info] # Warmup Iteration 12: 526.799 ms/op
[info] # Warmup Iteration 13: 510.283 ms/op
[info] # Warmup Iteration 14: 486.445 ms/op
[info] # Warmup Iteration 15: 514.173 ms/op
[info] # Warmup Iteration 16: 513.716 ms/op
[info] # Warmup Iteration 17: 514.954 ms/op
[info] # Warmup Iteration 18: 507.758 ms/op
[info] # Warmup Iteration 19: 508.607 ms/op
[info] # Warmup Iteration 20: 505.954 ms/op
[info] # Warmup Iteration 21: 487.222 ms/op
[info] # Warmup Iteration 22: 472.297 ms/op
[info] # Warmup Iteration 23: 487.540 ms/op
[info] # Warmup Iteration 24: 498.083 ms/op
[info] # Warmup Iteration 25: 464.409 ms/op
[info] # Warmup Iteration 26: 497.794 ms/op
[info] # Warmup Iteration 27: 473.420 ms/op
[info] # Warmup Iteration 28: 490.277 ms/op
[info] # Warmup Iteration 29: 504.183 ms/op
[info] # Warmup Iteration 30: 464.376 ms/op
[info] # Warmup Iteration 31: 470.950 ms/op
[info] # Warmup Iteration 32: 495.032 ms/op
[info] # Warmup Iteration 33: 494.734 ms/op
[info] # Warmup Iteration 34: 509.685 ms/op
[info] # Warmup Iteration 35: 472.280 ms/op
[info] # Warmup Iteration 36: 477.516 ms/op
[info] # Warmup Iteration 37: 477.354 ms/op
[info] # Warmup Iteration 38: 461.479 ms/op
[info] # Warmup Iteration 39: 451.367 ms/op
[info] # Warmup Iteration 40: 463.484 ms/op
[info] # Warmup Iteration 41: 466.221 ms/op
[info] # Warmup Iteration 42: 465.542 ms/op
[info] # Warmup Iteration 43: 494.241 ms/op
[info] # Warmup Iteration 44: 441.546 ms/op
[info] # Warmup Iteration 45: 97284.183 ms/op
[info] # Warmup Iteration 46: 460.705 ms/op
[info] # Warmup Iteration 47: 437.639 ms/op
[info] # Warmup Iteration 48: 476.750 ms/op
[info] # Warmup Iteration 49: 468.004 ms/op
[info] # Warmup Iteration 50: 466.253 ms/op
[info] # Warmup Iteration 51: 468.092 ms/op
[info] # Warmup Iteration 52: 488.991 ms/op
[info] # Warmup Iteration 53: 481.244 ms/op
[info] # Warmup Iteration 54: 459.122 ms/op
[info] # Warmup Iteration 55: 473.085 ms/op
[info] # Warmup Iteration 56: 469.700 ms/op
[info] # Warmup Iteration 57: 470.677 ms/op
[info] # Warmup Iteration 58: 455.173 ms/op
[info] # Warmup Iteration 59: 465.534 ms/op
[info] # Warmup Iteration 60: 466.951 ms/op
[info] # Warmup Iteration 61: 409725.999 ms/op
[info] # Warmup Iteration 62: 478.256 ms/op
[info] # Warmup Iteration 63: 467.704 ms/op
[info] # Warmup Iteration 64: 490.796 ms/op
[info] # Warmup Iteration 65: 475.197 ms/op
[info] # Warmup Iteration 66: 433.142 ms/op
[info] # Warmup Iteration 67: 456.869 ms/op
[info] # Warmup Iteration 68: 460.753 ms/op
[info] # Warmup Iteration 69: 454.673 ms/op
[info] # Warmup Iteration 70: 438.041 ms/op
[info] # Warmup Iteration 71: 431.964 ms/op
[info] # Warmup Iteration 72: 455.025 ms/op
[info] # Warmup Iteration 73: 431.728 ms/op
[info] # Warmup Iteration 74: 459.186 ms/op
[info] # Warmup Iteration 75: 432.997 ms/op
[info] # Warmup Iteration 76: 427.629 ms/op
[info] # Warmup Iteration 77: 457.082 ms/op
[info] # Warmup Iteration 78: 460.353 ms/op
[info] # Warmup Iteration 79: 467.694 ms/op
[info] # Warmup Iteration 80: 453.647 ms/op
[info] # Warmup Iteration 81: 453.673 ms/op
[info] # Warmup Iteration 82: 452.024 ms/op
[info] # Warmup Iteration 83: 455.451 ms/op
[info] # Warmup Iteration 84: 459.916 ms/op
[info] # Warmup Iteration 85: 436.827 ms/op
[info] # Warmup Iteration 86: 477.298 ms/op
[info] # Warmup Iteration 87: 458.223 ms/op
[info] # Warmup Iteration 88: 434.677 ms/op
[info] # Warmup Iteration 89: 447.431 ms/op
[info] # Warmup Iteration 90: 451.069 ms/op
[info] # Warmup Iteration 91: 430.800 ms/op
[info] # Warmup Iteration 92: 452.948 ms/op
[info] # Warmup Iteration 93: 452.016 ms/op
[info] # Warmup Iteration 94: 462.628 ms/op
[info] # Warmup Iteration 95: 430.445 ms/op
[info] # Warmup Iteration 96: 464.453 ms/op
[info] # Warmup Iteration 97: 132712.651 ms/op
[info] # Warmup Iteration 98: 443.603 ms/op
[info] # Warmup Iteration 99: 457.288 ms/op
[info] # Warmup Iteration 100: 452.323 ms/op
[info] # Warmup Iteration 101: 451.543 ms/op
Not sure yet why.
This benchmark randomly takes forever to execute:
Not sure yet why.