The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the LRA logic in the Single Query Track.
Page generated on 2021-07-18 17:29:05 +0000
Benchmarks: 1003 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | cvc5 | Vampire | cvc5 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 954 | 101816.41 | 101794.118 | 954 | 388 | 566 | 49 | 49 | 0 |
| 2019-Par4n | 0 | 932 | 110034.129 | 97682.999 | 932 | 384 | 548 | 71 | 71 | 0 |
| 2020-z3n | 0 | 927 | 136280.772 | 136181.732 | 927 | 385 | 542 | 76 | 76 | 0 |
| 2020-CVC4n | 0 | 824 | 254152.689 | 255456.875 | 824 | 340 | 484 | 179 | 179 | 0 |
| cvc5 | 0 | 823 | 206360.467 | 231750.256 | 823 | 346 | 477 | 180 | 180 | 0 |
| cvc5 - fixedn | 0 | 821 | 200915.211 | 233606.389 | 821 | 347 | 474 | 182 | 182 | 0 |
| UltimateEliminator+MathSAT | 0 | 743 | 342691.912 | 336234.283 | 743 | 284 | 459 | 260 | 254 | 0 |
| Vampire | 0 | 485 | 621019.305 | 622015.137 | 485 | 0 | 485 | 518 | 518 | 0 |
| Vampire - fixedn | 0 | 477 | 622642.05 | 621996.64 | 477 | 0 | 477 | 526 | 518 | 0 |
| iProver | 0 | 21 | 1187564.097 | 1180724.99 | 21 | 0 | 21 | 982 | 927 | 55 |
| SMTInterpol | 0 | 5 | 10675.712 | 8997.891 | 5 | 1 | 4 | 998 | 4 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 954 | 101820.11 | 101792.608 | 954 | 388 | 566 | 49 | 49 | 0 |
| 2019-Par4n | 0 | 944 | 118651.879 | 94801.014 | 944 | 388 | 556 | 59 | 59 | 0 |
| 2020-z3n | 0 | 927 | 136285.382 | 136179.942 | 927 | 385 | 542 | 76 | 76 | 0 |
| 2020-CVC4n | 0 | 824 | 254522.429 | 255448.545 | 824 | 340 | 484 | 179 | 179 | 0 |
| cvc5 | 0 | 823 | 231772.333 | 231742.926 | 823 | 346 | 477 | 180 | 180 | 0 |
| cvc5 - fixedn | 0 | 821 | 233580.078 | 233599.889 | 821 | 347 | 474 | 182 | 182 | 0 |
| UltimateEliminator+MathSAT | 0 | 744 | 342701.202 | 336206.983 | 744 | 284 | 460 | 259 | 253 | 0 |
| Vampire | 0 | 487 | 635765.185 | 620829.631 | 487 | 0 | 487 | 516 | 516 | 0 |
| Vampire - fixedn | 0 | 478 | 624703.32 | 620770.686 | 478 | 0 | 478 | 525 | 516 | 0 |
| iProver | 0 | 23 | 1188057.847 | 1179056.059 | 23 | 0 | 23 | 980 | 925 | 55 |
| SMTInterpol | 0 | 5 | 10675.712 | 8997.891 | 5 | 1 | 4 | 998 | 4 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 388 | 20399.482 | 20400.016 | 388 | 388 | 0 | 11 | 604 | 49 | 0 |
| 2019-Par4n | 0 | 388 | 30407.413 | 21834.492 | 388 | 388 | 0 | 11 | 604 | 59 | 0 |
| 2020-z3n | 0 | 385 | 26734.451 | 26731.458 | 385 | 385 | 0 | 14 | 604 | 76 | 0 |
| cvc5 - fixedn | 0 | 347 | 67204.782 | 67202.918 | 347 | 347 | 0 | 52 | 604 | 182 | 0 |
| cvc5 | 0 | 346 | 68075.456 | 68101.985 | 346 | 346 | 0 | 53 | 604 | 180 | 0 |
| 2020-CVC4n | 0 | 340 | 87208.34 | 87727.004 | 340 | 340 | 0 | 59 | 604 | 179 | 0 |
| UltimateEliminator+MathSAT | 0 | 284 | 143506.762 | 141336.395 | 284 | 284 | 0 | 115 | 604 | 253 | 0 |
| SMTInterpol | 0 | 1 | 9054.449 | 8189.949 | 1 | 1 | 0 | 398 | 604 | 4 | 0 |
| Vampire | 0 | 0 | 489600.39 | 478789.06 | 0 | 0 | 0 | 399 | 604 | 516 | 0 |
| iProver | 0 | 0 | 478800.0 | 478800.0 | 0 | 0 | 0 | 399 | 604 | 925 | 55 |
| Vampire - fixedn | 0 | 0 | 478800.0 | 478800.0 | 0 | 0 | 0 | 399 | 604 | 516 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 566 | 63420.628 | 63392.592 | 566 | 0 | 566 | 23 | 414 | 49 | 0 |
| 2019-Par4n | 0 | 556 | 70244.466 | 54966.522 | 556 | 0 | 556 | 33 | 414 | 59 | 0 |
| 2020-z3n | 0 | 542 | 91550.931 | 91448.485 | 542 | 0 | 542 | 47 | 414 | 76 | 0 |
| Vampire | 0 | 487 | 128164.795 | 124040.571 | 487 | 0 | 487 | 102 | 414 | 516 | 0 |
| 2020-CVC4n | 0 | 484 | 149314.089 | 149721.541 | 484 | 0 | 484 | 105 | 414 | 179 | 0 |
| Vampire - fixedn | 0 | 478 | 127903.32 | 123970.686 | 478 | 0 | 478 | 111 | 414 | 516 | 0 |
| cvc5 | 0 | 477 | 145696.877 | 145640.941 | 477 | 0 | 477 | 112 | 414 | 180 | 0 |
| cvc5 - fixedn | 0 | 474 | 148375.296 | 148396.971 | 474 | 0 | 474 | 115 | 414 | 182 | 0 |
| UltimateEliminator+MathSAT | 0 | 460 | 181194.44 | 176870.588 | 460 | 0 | 460 | 129 | 414 | 253 | 0 |
| iProver | 0 | 23 | 691257.847 | 682256.059 | 23 | 0 | 23 | 566 | 414 | 925 | 55 |
| SMTInterpol | 0 | 4 | 1584.811 | 793.698 | 4 | 0 | 4 | 585 | 414 | 4 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 861 | 4898.672 | 4205.903 | 861 | 360 | 501 | 142 | 142 | 0 |
| z3n | 0 | 821 | 5660.027 | 5658.78 | 821 | 363 | 458 | 182 | 182 | 0 |
| 2020-z3n | 0 | 796 | 6527.58 | 6501.054 | 796 | 354 | 442 | 207 | 207 | 0 |
| 2020-CVC4n | 0 | 727 | 6971.075 | 6965.102 | 727 | 299 | 428 | 276 | 276 | 0 |
| cvc5 | 0 | 723 | 6962.02 | 6961.783 | 723 | 296 | 427 | 280 | 280 | 0 |
| cvc5 - fixedn | 0 | 723 | 6962.209 | 6961.929 | 723 | 296 | 427 | 280 | 280 | 0 |
| UltimateEliminator+MathSAT | 0 | 621 | 15511.438 | 12212.261 | 621 | 256 | 365 | 382 | 376 | 0 |
| Vampire | 0 | 482 | 12874.302 | 12660.149 | 482 | 0 | 482 | 521 | 521 | 0 |
| Vampire - fixedn | 0 | 474 | 12883.191 | 12660.878 | 474 | 0 | 474 | 529 | 521 | 0 |
| iProver | 0 | 6 | 24188.612 | 24000.342 | 6 | 0 | 6 | 997 | 942 | 55 |
| SMTInterpol | 0 | 5 | 2606.202 | 1372.427 | 5 | 1 | 4 | 998 | 19 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.